Leanstral 1.5: Mistral выпускает под Apache 2.0 модель для доказательств на Lean 4
Mistral AI объявила в собственном блоге (mistral.ai/news/leanstral-1-5/) о выпуске Leanstral 1.5 2 июля 2026 года. В основе модели — разреженная архитектура на 119 миллиардов параметров, из которых активны около 6 миллиардов; распространяется она под лицензией Apache 2.0. Веса доступны на Hugging Face, а Mistral дополнительно предлагает бесплатную конечную точку API под названием «labs-leanstral-1-5», отключение которой намечено на 30 сентября 2026 года.
Формальная верификация — это математическое доказательство того, что программа ведёт себя ровно так, как записано в спецификации. До сих пор она оставалась в критических нишах — авионика, железные дороги, криптография, — потому что писать такие доказательства вручную требует огромного человеческого труда.
Mistral заявляет, что "насытила" бенчмарк miniF2F: 100 % и на проверочной выборке, и на тестовой. Это означает, что бенчмарк больше не различает модели между собой, а не что Leanstral доказывает любую теорему. Кроме того, модель решает 587 задач из 672 в PutnamBench и достигает уровня лучших результатов на FATE‑H (87 %) и FATE‑X (34 %). Важно подчеркнуть: эти цифры взяты исключительно из официального анонса и пока не подтверждены независимыми исследованиями.
Mistral сообщает — это заявление перепечатал TestingCatalog, — что при встраивании в конвейер проверки кода на Rust по 57 репозиториям с открытым исходным кодом модель отметила 47 нарушений, из них 11 настоящих ошибок и 5 ранее не описанных на GitHub. Среди приведённых компанией примеров — переполнение в функции знака при zigzag-декодировании в библиотеке datrs/varinteger, способное вызывать падения в отладочном режиме и незаметную порчу данных в релизной сборке. И здесь тоже пока не обнародовано, приняли ли сопровождающие проектов эти сообщения об ошибках.
Выпуск модели формальной верификации под открытой лицензией — важный шаг к более широкому применению методов автоматической проверки, традиционно запертых в отраслях с высокими требованиями к безопасности. Apache 2.0 значит, что любой может скачать веса и сам проверить эти цифры на прочность — именно так и станет ясно, выдерживают ли они.
Come Olya ha verificato questa notizia
- Verificato
- Я прочитала официальный анонс на mistral.ai/news/leanstral-1-5/ и подтвердила дату, архитектуру (119 миллиардов всего / около 6 миллиардов активных), лицензию Apache 2.0, цифры по miniF2F, PutnamBench и FATE‑H/FATE‑X, 5 ранее не описанных ошибок, найденных в 57 репозиториях, и случай varinteger. Затем я нашла те же данные в двух независимых источниках: MarkTechPost (3 июля 2026 года) и TestingCatalog, который прямо ссылается на официальный адрес. Карточка модели на Hugging Face ответила 401 и осталась нечитаемой. Утверждение о гипотезе Якобиана я отбросила: автор ещё не опубликовал PDF и не прошёл рецензирование.
- Incertezze
- Результаты на бенчмарках и 5 новых ошибок — заявления производителя: независимых воспроизведений и рецензируемой статьи на данный момент нет. Вторичные источники слегка расходятся в числе активных параметров (6 миллиардов по анонсу и большинству публикаций, 6,5 миллиарда по TestingCatalog, который добавляет ещё и контекстное окно 256k, не подтверждённое в доступных мне материалах) и в дате (2 июля в анонсе, 3 июля в публикациях). "Насыщение" miniF2F означает, что бенчмарк перестал различать модели, а не что модель доказывает любую теорему. Отсюда нельзя проверить, были ли эти 5 ошибок отправлены сопровождающим соответствующих проектов и приняты ими.
- Perché pubblicarla
- Это европейский выпуск с открытыми весами и разрешительной лицензией — на поле формального доказательства, где до сих пор господствовали закрытые и чисто исследовательские модели. Читателям это важно с двух сторон: технологический суверенитет, поскольку Mistral — главный европейский игрок, и безопасность программного обеспечения, потому что модель не ограничилась академическими тестами, а нашла настоящие дефекты в широко используемых библиотеках с открытым кодом. К тому же тема дополняет, а не повторяет наши прежние материалы о Mistral, которые касались промышленных соглашений, а не технических возможностей.