ИИтог

Leanstral 1.5: свободный доступ к формальной верификации

моделиРедакция ИИтогHacker News🔥78Рейтинг ИИтог · значимость 74 · 223 баллов · 20/ч · 55 коммент.

Mistral выпустила Leanstral 1.5, новую модель с 119B параметров (6B активных) под лицензией Apache-2.0, специализированную на формальной верификации и доказательстве теорем на языке Lean 4. На стандартных тестах модель достигает рекордных результатов: полностью решает miniF2F (100%), справляется с 587 из 672 задач PutnamBench, достигает 87% на FATE-H (абстрактная алгебра уровня магистратуры) и 34% на FATE-X (уровень PhD).

Модель обучалась в три этапа: предварительная подготовка, supervised fine-tuning и усиленное обучение (RL) с методом CISPO. Ключевой инновацией стало обучение в двух средах: в многошаговой среде модель получает теорему и должна её доказать, получая обратную связь от компилятора Lean при каждой итерации; в среде кодового агента модель работает как разработчик с полным доступом к файловой системе, может запускать bash-команды и использовать языковой сервер Lean в реальном времени, позволяя решать сложные задачи через несколько итераций и контекстные сжатия.

При применении к коду Leanstral показала практическую ценность: автоматизированный конвейер обнаружил 5 ранее неизвестных багов в открытом исходном коде, включая критическую ошибку переполнения в функции распаковки zigzag-декодирования varint в библиотеке datrs. Модель демонстрирует сильное масштабирование по тестовому времени: при увеличении бюджета токенов с 50 тысяч до 4 миллионов на одну задачу, решаемость PutnamBench растёт плавно с 44 до 587 задач. На коде (бенчмарк FLTEval) Leanstral превосходит GPT-4o при стоимости в 7 раз ниже.

Модель полностью открыта (лицензия Apache-2.0, веса на Hugging Face) и доступна через свободное API в составе Mistral Vibe. Стоимость применения существенно ниже конкурентов: около $4 за задачу вместо $300+ для других высокопроизводительных систем.

Ключевые факты

  • Leanstral 1.5 решает все 100% задач из miniF2F и 587/672 из PutnamBench, установив новый рекорд в формальной верификации
  • Обучена в двух RL-окружениях: многошаговое доказательство теорем с компилятором Lean и полный рабочий процесс кодового агента (edit, bash, LSP)
  • Находит реальные баги: обнаружила 5 ранее неизвестных ошибок в открытом коде (переполнения, логические ошибки в криптографии и структурах данных)
  • Показывает сильное масштабирование тестового времени: на PutnamBench решаемость растёт с 44 задач (50k токенов) до 587 (4M токенов)
  • Полностью открыта (Apache-2.0), доступна на Hugging Face и через свободное API; работает в 7 раз дешевле GPT-4o с лучшим качеством на коде

Почему это важно

Формальная верификация долгое время оставалась нишей, доступной только крупным исследовательским группам. Leanstral 1.5 впервые делает её практической и бесплатно доступной. Открытие багов, которые пропускают обычное тестирование и фаззинг, показывает, что ИИ может работать как инструмент обеспечения качества критичного кода. Применение к реальным проектам (57 репозиториев) с реальными найденными ошибками доказывает выход за рамки теоретических бенчмарков.

Кому это важно

Разработчикам критичного ПО (криптография, системное ПО, компиляторы, базы данных), исследователям в области формальных методов, авторам библиотек, которые хотят гарантировать корректность. Математикам и студентам, решающим задачи доказательства (олимпиадные, конкурентные). Компаниям, где баги обходятся дорого (финансовые системы, безопасность, авиаэлектроника).

Как это применить

Используйте Mistral Vibe с установленными Leanstral 1.5 и расширением Lean LSP MCP. Загрузите API-ключ Mistral. На простые задачи дайте модели теорему, на сложные, предоставьте репозиторий и попросите найти ошибки в реализации. Модель работает автономно: генерирует файлы, запускает Lean, интерпретирует ошибки компилятора. Для поиска багов в Rust-коде используйте конвейер: транслируйте через Aeneas в Lean, генерируйте свойства корректности, пусть модель их доказывает. Если доказательство не находит, ищет контрпримеры.

Можно ли доверять

Модель обучена строго: все доказательства проверяются компилятором Lean автоматически, ошибки видны сразу. На стандартных бенчмарках результаты воспроизводятся. Найденные баги (зигзаг-переполнение в varinteger) проверены вручную и подтверждены. Если модель что-то доказала в Lean, это математическая истина; если не доказала, это не гарантирует отсутствия доказательства.

Риски и подводные камни

Модель обучена в основном на математике, результаты на коде хороши, но вторичны. Сложные задачи требуют больших бюджетов токенов (AVL-trees заняли 2.7M токенов). Не заменяет рецензирование кода. Mistral Vibe пока в бета, API может меняться. Формальная верификация требует явного уточнения требуемых свойств, не помогает с нечётким определением требований. Доступ через API зависит от работоспособности сервиса Mistral.

«Конвейер Leanstral обнаружил его автоматически, демонстрируя, что формальная верификация уже может применяться к реальному коду и находить баги, которые пропускают традиционные методы.»

— Mistral AI