Leanstral 1.5 от Mistral: open-source модель для формальной верификации нашла 5 реальных багов в коде

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

Помимо отличных результатов на математических бенчмарках (включая задачи PutnamBench), Leanstral 1.5 продемонстрировала практическую пользу: при анализе 57 open-source репозиториев модель выявила пять ранее не замеченных багов. Это показывает, что формальная верификация с помощью ИИ может находить реальные уязвимости в коде, а не только решать абстрактные задачи.

Релиз усиливает позиции Mistral в сегменте open-source моделей для специализированных задач. Leanstral 1.5 доступна для загрузки и может быть интегрирована в пайплайны разработки, где требуется повышенная надёжность кода.