🌟 Mistral AI обновила модель Leanstral Leanstral 1.5 - новая версия ранее выпущенной модели для формальной верификации в языке Lean 4. Задача подобных моделей помогать составлять и проверять доказательства, которые компилятор Lean принимает как корректные.

Lean 4 - это система интерактивного доказательства теорем, которая позволяет записывать математические утверждения и проверять их строго формально, а также описывать свойства программного кода.

Обновление не затронуло изменение архитектуры, количество параметров и окно контекста, под капотом также MoE на 119 млрд общих и 6,5 млрд активных параметров, 256 тысяч токенов контекст и мультимодальность на входе. Версия 1.5 прошла техэтапное обучение в 2-х средах: одна отрабатывает доказательство теорем в диалоге с компилятором Lean, другая учит модель действовать как программист в реальных репозиториях. 🟡Тесты Апдейт полностью насыщает бенчмарк miniF2F, набирая 100% на проверочной и тестовой выборках, решает 587 из 672 задач PutnamBench и показывает лучшие на сегодня результаты на наборах FATE-H и FATE-X.

К слову, на PutnamBench, Leanstral 1.5 опережает систему Seed-Prover 1.5 на 7 задач при затратах около 4 долларов на задачу (против 300+ долларов у соперника).

В тесте по кодингу на 57 репозиториях, система с участием Leanstral выявила 47 нарушенных свойств, из которых 11 оказались реальными ошибками, а 5 ранее не были известны. 📌Лицензирование: Apache 2.0 License 🟡Блогпост 🟡Модель 🟡Demo @ai_machinelearning_big_data #AI #ML #LLM #LEAN #LeanStral #MistralAI