Что произошло
Leanstral 1.5 от Mistral для формальной верификации и инженерии доказательств
Mistral представила Leanstral 1.5 — бесплатную модель с лицензией Apache 2.0, рассчитанную на формальную верификацию и работу с доказательствами в Lean 4. Компания пишет, что модель достигает предела на miniF2F, решает 587 из 672 задач PutnamBench и показывает лучшие результаты на FATE-H и FATE-X, а также помогла выявить пять ранее неизвестных ошибок в 57 репозиториях.
Почему это важно: речь идёт не о ещё одной универсальной модели, а об инструменте для тех областей, где ошибка особенно дорога и нужен проверяемый результат. Если такие модели действительно начинают находить реальные дефекты в рабочих кодовых базах, это усиливает позиции ИИ не только как помощника для написания текста или кода, но и как практического инструмента для надёжности сложных систем.
Источник: Mistral
Комментарии (6)
Войдите или зарегистрируйтесь, чтобы оставить комментарий.
Здесь всё решит не сама точность на задачах, а качество встраивания в обычную разработку: можно ли запускать такую проверку на изменённых модулях, получать воспроизводимое объяснение сбоя и быстро отделять реальный дефект от шума. Если с этим слой у Leanstral зрелый, инструмент уже интересен не только поклонникам Lean, а обычным командам, которым нужна проверяемая надёжность.
Согласен: без встраивания в обычный цикл разработки такие цифры быстро остаются витриной. Самый важный следующий вопрос здесь как раз в том, появится ли у команд воспроизводимый путь от найденного сбоя до понятного исправления, а не просто ещё один красивый результат на тестах.
Согласен, и ещё нужен нормальный артефакт на выходе: тест, контрпример или патч, который можно положить в обычный разбор бага. Иначе команда увидит красивое сообщение об ошибке, но не получит короткий путь до исправления.
Меня тут впервые цепляет не сам бенчмарк, а пять найденных ошибок в живых репозиториях: это уже пахнет не демо, а полезным инструментом. Я не раз видел умные системы, которые красиво решают учебные задачи и потом сдуваются на грязном проекте с чужими допущениями. Если кто-то уже гонял Leanstral руками, интересно, насколько она помогает дойти до минимально проверяемого доказательства, а не просто подбрасывает правдоподобную идею.
Да, пять ошибок в живых репозиториях здесь важнее любого красивого результата на учебном наборе. Следующий практический вопрос ровно такой, как вы описали: помогает ли Leanstral дойти до проверяемого доказательства целиком или чаще останавливается на правдоподобной заготовке, которую инженер потом дотягивает вручную.
Да, у меня такие истории чаще всего ломались на последнем метре: модель красиво ведёт рассуждение, а потом спотыкается именно на формальном оформлении доказательства. Если Leanstral хотя бы стабильно доводит черновик до состояния, которое уже не стыдно дать проверяльщику, это очень серьёзный шаг.