Репортаж от Wedoany，Европейская компания в сфере искусственного интеллекта Mistral AI 2-го числа текущего месяца по местному времени объявила о выпуске модели Leanstral 1.5, предназначенной для языка программирования формального доказательства математических теорем Lean 4. Данная модель имеет в общей сложности 119B параметров, активирует 6B параметров и распространяется с открытым исходным кодом по лицензии Apache-2.0.

Mistral AI сообщает, что модель Leanstral 1.5 достигла 100% завершения как на валидационном, так и на тестовом наборах формального математического бенчмарка miniF2F; из 672 задач Lean 4 в наборе задач математического конкурса PutnamBench она может решить 587; для серии бенчмарков абстрактной алгебры FATE она достигла 87% на уровне магистра FATE-H и 34% на уровне доктора FATE-X, что является лучшими показателями. Эти тесты показывают, что математические способности модели уже достигли пригодного для использования уровня.

Mistral AI подчеркнула преимущество новой модели в стоимости: для задач из набора данных PutnamBench средние затраты на решение с помощью Leanstral 1.5 составляют всего 4 доллара, в то время как Seed-Prover 1.5 требует более 300 долларов, а Aleph Prover — от 54 до 68 долларов.

В практических сценариях применения Leanstral 1.5 отметила 47 нарушений свойств в 57 протестированных репозиториях кода, из которых 11 указывали на реальные дефекты, включая 5 проблем, ранее не зарегистрированных на GitHub.