Команда Leanstral выпустила модель версии 1.5 для формальной верификации кода и математических доказательств. Она работает на Lean 4. Модель имеет 119 миллиардов параметров, но активны из них только 6 миллиардов — это даёт высокую производительность при скромных вычислительных затратах. Leanstral 1.5 распространяется по свободной лицензии Apache-2.0.
Модель обучалась в три этапа: дообучение на промежуточных данных, supervised fine-tuning и reinforcement learning с алгоритмом CISPO. В процессе она работала в двух окружениях. В многопопыточном (multiturn) она получает теорему и пытается её доказать или опровергнуть, получая обратную связь от компилятора Lean. В режиме code agent модель сама редактирует файлы, запускает команды bash и использует Lean Language Server для анализа типов и ошибок в реальном времени.
Результаты на бенчмарках впечатляют. Leanstral насыщает тест miniF2F, набирая 100% на валидации и тесте. На PutnamBench модель решает 587 задач из 672. На FATE-H и FATE-X она показывает новый state-of-the-art: 87% и 34% соответственно. При этом стоимость решения одной задачи на PutnamBench — около 4 долларов, что резко контрастирует с $300 у Seed-Prover 1.5 и $54–68 у Aleph Prover.
Leanstral 1.5 отлично масштабируется по времени: при увеличении токенового бюджета на попытку с 25k до 4M количество решённых задач на PutnamBench плавно растёт с 44 до 587. Модель не сдаётся на длинных доказательствах — пример с AVL-деревом потребовал 2,7 миллиона токенов и 22 итерации уплотнения (compactions). В итоге Leanstral доказал, что вставка и удаление в AVL-дереве действительно работают за O(log n).
Помимо математики, модель нашла применение в верификации кода. Leanstral вместе с инструментом Aeneas, который переводит код из Rust в Lean, проверил 57 репозиториев. Модель выявила 47 нарушенных свойств, 11 из которых оказались реальными багами, причём 5 ранее не были зафиксированы на GitHub. Среди них — ошибка переполнения в функции sign для zigzag-декодинга библиотеки datrs/varinteger. На входе Std.U64.MAX выражение (value + 1) переполнялось, вызывая краш в debug-режиме и молчаливое повреждение данных в release.
Исходные коды и веса модели доступны на Huggingface, также работает бесплатный API под именем leanstral-1-5. Для старта рекомендуется использовать инструмент Mistral Vibe и опционально установить Lean LSP MCP.