Mistral ИИ выпустила Leanstral 1.5 — модель для формальной верификации на языке Lean 4 под открытой лицензией Apache 2.0. Модель показала 100% точность на бенчмарке miniF2F, который включает задачи от школьного уровня до олимпиадного. На PutnamBench, содержащем 672 задачи из престижного математического конкурса, Leanstral 1.5 решила 587. На алгебраических бенчмарках FATE-H и FATE-X, охватывающих задачи уровня магистратуры и докторантуры в теории групп и колец, модель показала лучшие результаты среди открытых: 87% и 34% соответственно. Среди закрытых моделей её превосходит только Aleph Prover.
Leanstral 1.5 обучалась в три этапа: промежуточное обучение (mid-training), контролируемая донастройка и обучение с подкреплением. Несмотря на основную направленность на математику, модель также справляется с верификацией кода. В практическом тестировании Leanstral 1.5 просканировала 57 открытых репозиториев и обнаружила пять ранее неизвестных ошибок, в том числе переполнение в Rust-библиотеке varinteger. Это демонстрирует практическую пользу модели для повышения надёжности программного обеспечения.
| Бенчмарк | Результат Leanstral 1.5 | Примечание |
|---|---|---|
| miniF2F | 100% | Задачи от школьного уровня до олимпиадного |
| PutnamBench | 587/672 (87,4%) | Лучший среди открытых; превзойдён только Aleph Prover |
| FATE-H | 87% | Лучший среди открытых; задачи уровня магистратуры |
| FATE-X | 34% | Лучший среди открытых; задачи уровня докторантуры |
Формальная верификация — это процесс математического доказательства корректности программ и теорем. Традиционно она требует высокой квалификации, но модели вроде Leanstral 1.5 могут автоматизировать часть работы. Открытая лицензия и бесплатный API делают технологию доступной для исследователей и разработчиков. Leanstral 1.5 уже доступна для загрузки на Hugging Face и через API Mistral.
Модель набрала 100% на бенчмарке miniF2F (олимпиадные задачи по математике).
Тем не менее, Leanstral 1.5 — узкоспециализированная модель: её сила именно в формальной верификации, а не в общих задачах. Для сравнения, закрытая Aleph Prover показывает более высокие результаты на PutnamBench. Открытость модели позволяет сообществу дорабатывать её и адаптировать под свои нужды. Выход Leanstral 1.5 — ещё один шаг к интеграции ИИ в формальные методы доказательства.
