Mistral выпустила Leanstral 1.5, бесплатную модель с лицензией Apache-2.0, имеющую 6B активных параметров и предназначенную для формальной верификации и автоматического доказательства теорем.

  • Достижение предела на бенчмарке miniF2F и решение 587 из 672 задач PutnamBench.
  • Достижение результатов уровня state-of-the-art на FATE-H (87%) и FATE-X (34%).
  • Обучение проводилось через mid-training, supervised fine-tuning и reinforcement learning с использованием CISPO.
  • Обнаружено 5 ранее неизвестных багов в 57 протестированных репозиториях во время agentic proof engineering.

Этот релиз позволяет разработчикам проверять корректность их программного обеспечения и спецификаций кода через формальную proof engineering.