⚡⚡ Leanstral — первый open-source агент от Mistral для Lean 4: математические доказательства и верификация кода
Leanstral — это специализированный AI-агент, созданный для работы с Lean 4 (язык программирования и интерактивный доказыватель теорем). Если раньше формальная верификация сложных математических объектов или свойств Rust-кода требовала участия экспертов и дорогих проприетарных моделей, то теперь это доступно в open-source под лицензией Apache 2.0.
В основе лежит архитектура MoE (Mixture of Experts) на 119B параметров, где на каждый токен активируются всего 6.5B параметров (4 эксперта из 128). Это делает модель невероятно эффективной: на бенчмарке FLTEval (оценка эффективности формального доказательства теорем) Leanstral с результатом 26.3 (pass@2) обходит Claude 3.5 Sonnet на 2.6 пункта, при этом стоимость запуска в 15 РАЗ НИЖЕ ($36 против $549).
Модель поддерживает контекст в 256k токенов, что позволяет скармливать ей целиком крупные репозитории или научные работы. Кроме текста, Leanstral понимает изображения и умеет работать в режиме мультиагента через Mistral Vibe. По сравнению с предыдущим поколением Mistral Small, скорость генерации выросла на 40%, а пропускная способность — в 3 раза.
Запустить модель локально можно через vLLM или интегрировать прямо в рабочий процесс через uv pip install mistral-vibe --upgrade и команду /leanstall внутри интерфейса Vibe. Это мощный инструмент для тех, кто хочет гарантировать корректность своего кода не просто тестами, а математическим доказательством.
#AI #Mistral #Lean4 #OpenSource #MoE #FormalVerification
