Mistral выпускает Leanstral 1.5: открытая модель формальной верификации для Lean 4
Mistral
Mistral выпустила Leanstral 1.5 — MoE-модель с 119B суммарных и 6B активных параметров, специализированную на формальном математическом доказательстве в Lean 4, под лицензией Apache-2.0. Модель полностью насыщает miniF2F (100%), решает 587/672 задач PutnamBench и устанавливает новый SOTA на FATE-H (87%) и FATE-X (34%). В практическом тестировании на 57 репозиториях с открытым исходным кодом модель обнаружила ранее неизвестные ошибки, в том числе целочисленное переполнение в широко используемой функции зигзаг-декодирования.
Почему это важно
Первая открытая модель, одновременно насыщающая miniF2F и демонстрирующая реальное обнаружение ошибок в масштабе; лицензия Apache-2.0 позволяет напрямую развёртывать её в коммерческих пайплайнах программной безопасности.
Важность: 4/5
SOTA на всех протестированных бенчмарках формального рассуждения; первая открытая модель, насыщающая miniF2F и находящая реальные ошибки в production-коде