❗️Leanstral 1.5: формальная верификация для всех — новая модель Mistral с открытым кодом

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

Обучение проходило в три этапа: mid-training, supervised fine-tuning и reinforcement learning с методом CISPO. Модель работает в двух средах: многопользовательской (многократные попытки доказательства с обратной связью от Lean-компилятора) и агентной (работа с файловой системой, bash-командами и Lean Language Server для долгосрочных задач). На PutnamBench модель демонстрирует сильное масштабирование по времени тестирования: от 44 решённых задач при бюджете 50k токенов до 587 при 4M токенов — при стоимости около $4 за задачу против $300+ у Seed-Prover 1.5.

Практическое значение: Leanstral 1.5 применима для верификации сложных свойств кода (например, временной сложности AVL-деревьев) и поиска ошибок в реальных проектах. Модель доступна на Hugging Face и через бесплатный API. Также открыт бенчмарк FLTEval на основе реальных pull request из репозитория Великой теоремы Ферма.

#AI #OpenCode #FormalVerification #MistralAI #Lean4