16 марта Mistral представила Leanstral — специализированную модель с разреженной архитектурой «смесь экспертов» (MoE), спроектированную для написания и верификации формальных математических доказательств в языке Lean 4. В рамках собственного бенчмарка FLTEval модель продемонстрировала преимущество над Claude Sonnet 4.6 на 2,6 балла, при этом стоимость выполнения запроса оказалась примерно в 15 раз ниже.
Контекст разработки и формальная верификация
Релиз Leanstral продиктован проблемами безопасности современного «vibe coding», где генеративные модели пишут код без должной проверки. Согласно исследованиям, в выборке кода, созданного ИИ, было обнаружено 69 уязвимостей. Mistral позиционирует Leanstral как инструмент для формальной верификации, позволяющий гарантировать, что программный код соответствует заданной спецификации еще до внедрения в продакшн. Это принципиально отличается от классического модульного тестирования или статического анализа.
Формальная верификация — это построение математического доказательства корректности кода. Если доказательство не проходит, значит, код содержит ошибку, а не просто «вероятно ошибочен». В этом процессе ключевую роль играет Lean 4, который одновременно является полноценным языком функционального программирования и ассистентом доказательств. Популярность Lean 4 в академической среде резко возросла благодаря таким проектам, как формализация Великой теоремы Ферма (FLT) в Имперском колледже Лондона.
Архитектура и обучение
Именно репозиторий проекта FLT стал источником данных для обучения Leanstral. В отличие от стандартного подхода, где модели тренируются на изолированных задачах из математических олимпиад, разработчики из Mistral использовали реальные пул-реквесты, содержащие сложные зависимости, импортированные определения и специфическую структуру проекта.
Архитектурно Leanstral представляет собой модель с общим количеством параметров 120 млрд, где на каждый токен активируются только 6 млрд параметров из 128 экспертных модулей. Такая стратегия маршрутизации (аналогичная семейству Mixtral) обеспечивает высокую скорость и экономичность инференса по сравнению с плотными моделями аналогичного размера.
Результаты бенчмарков и возможности интеграции
Для оценки работы модели был представлен бенчмарк FLTEval, измеряющий частоту генерации правильного доказательства за N попыток (pass@N) с учетом стоимости вычислений. По данным Mistral, Leanstral (pass@2) обходит Claude Sonnet, при этом для тех, кому требуется максимальная точность, по-прежнему лидирует Claude Opus, хотя и с гораздо более высоким ценником ($1650 за 39,6 операции против $290 у Leanstral).
Важным дополнением стала поддержка протокола MCP через lean-lsp-mcp. Интеграция с локально запущенным языковым сервером Lean 4 позволяет модели получать обратную связь о текущем состоянии доказательства в реальном времени, вместо того чтобы пытаться угадать результат. Кроме того, модель способна переводить доказательства из экосистемы Rocq (ранее известной как Coq) в Lean 4, что облегчает миграцию для исследовательских групп.
Варианты использования
Mistral предлагает три пути взаимодействия с технологией:
1. Интерфейс Vibe: Максимально простой способ работы через CLI или веб-интерфейс без настройки API-ключей.
2. Labs API: Доступ к эндпоинту labs-leanstral-2603, который в данный период обратной связи функционирует бесплатно.
3. Self-hosted Weights: Веса модели опубликованы под лицензией Apache 2.0. Несмотря на то, что это не «карманная» модель и для её запуска требуются серьезные вычислительные мощности (GPU-память), это обеспечивает полный контроль над инфраструктурой и поведением ИИ.
Хотя результаты бенчмарков впечатляют, стоит учитывать, что они базируются на внутренних данных Mistral. Однако открытость FLTEval позволяет любому специалисту провести независимую проверку. Основной вопрос для будущего использования Leanstral заключается в том, насколько эффективно модель справится со спецификой формальной верификации программного обеспечения, которая отличается от чистой математики, представленной в репозитории проекта FLT.
