Французская компания Mistral AI представила Leanstral — открытого ИИ-агента, который не только пишет код, но и способен формально доказать его корректность. По сути, это инструмент, работающий вместе с системой формальных доказательств Lean 4 и помогающий в так называемой «инженерии доказательств» — строгой проверке математических рассуждений и программных спецификаций.
В компании сделали ставку на новый подход: будущее не за просто «умными» моделями, а за агентами, которые могут обосновать каждый свой шаг и гарантировать соответствие требованиям. Leanstral стал первым серьёзным шагом в этом направлении.
Модель основана на архитектуре Mixture of Experts (MoE), оптимизированной под задачи доказательства. Она задействует лишь часть своих параметров (около 6 млрд активных), выбирая нужные экспертные модули под конкретную задачу. Это позволяет сочетать высокую производительность с эффективностью. При этом Lean выступает как надёжный верификатор, благодаря чему Leanstral может одновременно генерировать и проверять множество вариантов решений.
Для оценки возможностей разработчики использовали бенчмарк FLTEval, который проверяет завершение формальных доказательств и корректность введения новых математических понятий.
Результаты показали, что даже сильные открытые модели уступают: например, Qwen3.5 (397B-A17B) достигает 25,4 балла за 4 попытки, тогда как Leanstral с 120 млрд параметров (и всего 6 млрд активных) выдаёт 26,3 уже за 2 попытки и доходит до 29,3 за 4.
Особенно примечательно сравнение с моделями Claude. Leanstral оказался не только конкурентоспособным, но и значительно более дешёвым: при стоимости около $36 (pass@2) он набирает 26,3 балла, обгоняя Claude Sonnet 4.6, который стоит $549 и показывает 23,7. Впрочем, более продвинутый Claude Opus 4.6 пока остаётся лидером с результатом 39,6 балла.
В компании сделали ставку на новый подход: будущее не за просто «умными» моделями, а за агентами, которые могут обосновать каждый свой шаг и гарантировать соответствие требованиям. Leanstral стал первым серьёзным шагом в этом направлении.
Модель основана на архитектуре Mixture of Experts (MoE), оптимизированной под задачи доказательства. Она задействует лишь часть своих параметров (около 6 млрд активных), выбирая нужные экспертные модули под конкретную задачу. Это позволяет сочетать высокую производительность с эффективностью. При этом Lean выступает как надёжный верификатор, благодаря чему Leanstral может одновременно генерировать и проверять множество вариантов решений.
Для оценки возможностей разработчики использовали бенчмарк FLTEval, который проверяет завершение формальных доказательств и корректность введения новых математических понятий.
Результаты показали, что даже сильные открытые модели уступают: например, Qwen3.5 (397B-A17B) достигает 25,4 балла за 4 попытки, тогда как Leanstral с 120 млрд параметров (и всего 6 млрд активных) выдаёт 26,3 уже за 2 попытки и доходит до 29,3 за 4.
Особенно примечательно сравнение с моделями Claude. Leanstral оказался не только конкурентоспособным, но и значительно более дешёвым: при стоимости около $36 (pass@2) он набирает 26,3 балла, обгоняя Claude Sonnet 4.6, который стоит $549 и показывает 23,7. Впрочем, более продвинутый Claude Opus 4.6 пока остаётся лидером с результатом 39,6 балла.
