Mistral выпустил Leanstral 1.5: решает 587 из 672 задач PutnamBench и находит баги в Rust

Mistral AI открыла Leanstral 1.5 под лицензией Apache 2.0 и сразу запустила бесплатный API-эндпоинт. Модель заточена под формальную верификацию кода и математических доказательств в Lean 4.

Что такое Leanstral 1.5 и зачем он нужен

Lean 4 - это proof assistant: система, которая механически проверяет каждый логический шаг. В ней можно выразить как абстрактные математические объекты (перфектоидные пространства), так и свойства реального кода на Rust.

Leanstral 1.5 обновляет предыдущую версию Leanstral-2603 и входит в семейство Mistral Small 4.

Архитектура: MoE с 128 экспертами

Модель построена по схеме mixture-of-experts (MoE). Каждый токен направляется к небольшому числу специализированных подсетей, а не ко всей модели целиком - это держит вычислительную нагрузку низкой при большой суммарной ёмкости.

Параметры:

• 119B параметров всего
• 6.5B активируются на каждый токен
• 128 экспертов, 4 активных на токен
• Контекстное окно - 256k токенов
• Принимает текст и изображения, выдаёт текст

Как обучали: три стадии и два RL-окружения

Обучение проходило в три этапа: mid-training, supervised fine-tuning, затем reinforcement learning с алгоритмом CISPO.

Для RL использовали два окружения. В первом модель получает формулировку теоремы, отправляет доказательство, читает фидбек компилятора Lean и итерирует до успеха или исчерпания бюджета. Во втором - работает напрямую с файловой системой: редактирует файлы, запускает bash-команды, использует Lean language server для получения целей, ошибок и типов в реальном времени.

Долгие задачи модель решает через context compaction - сжатие ранних частей контекста, чтобы задача вписалась в окно. Корректность проверяет форк SafeVerify от Mistral.

Бенчмарки

miniF2F - насыщение: 100% на validation и test сетах.

PutnamBench - 587 из 672 задач, что на 7 задач больше, чем у Seed-Prover 1.5 high. При этом Leanstral обходится примерно в $4 за задачу, тогда как Mistral оценивает стоимость Seed-Prover high-режима в $300 и выше (бюджет - 10 H20-дней на задачу).

FATE-H / FATE-X (алгебра) - новый state-of-the-art: 87% и 34% соответственно.

FLTEval (реальные pull request-ы в репозиторий доказательства теоремы Ферма):

• pass@1 вырос с 21.9 до 28.9
• pass@8 вырос с 31.9 до 43.2

На FLTEval Leanstral превосходит Opus 4.6 (39.6) при стоимости в семь раз ниже.

Масштабирование при инференсе

Чем больше токенов выделяешь на попытку, тем больше задач PutnamBench модель решает. По данным Mistral:

• 50k токенов - 44 задачи
• 200k - 244
• 1M - 493
• 4M - 587

Это test-time scaling в действии: без переобучения, просто бюджет на рассуждение.

Реальные кейсы: AVL-деревья и баги в Rust

Mistral документирует два практических случая.

Первый - доказательство O(log n) временной сложности для реальной реализации AVL-дерева. Модель использовала структурную индукцию и монадическое отслеживание времени через TimeM monad. Задача заняла более 2.7 млн токенов и 22 compaction-а. Итог - доказанная граница около 48 шагов на единицу высоты плюс константа.

Второй - автоматический поиск багов в open-source коде. Пайплайн: Aeneas переводит Rust-код в Lean, Leanstral выводит пользовательские намерения и генерирует свойства корректности, затем пытается доказать каждое свойство (4 попытки) и его отрицание (ещё 4).

Через 57 репозиториев: 47 нарушенных свойств, 11 настоящих багов, 5 из которых ранее не были зафиксированы на GitHub.

Один из найденных багов - в функции знака для zigzag-декодирования в datrs/varinteger. На входе Std.U64.MAX выражение (value + 1) переполнялось, вызывая краш в debug-режиме и тихое повреждение данных в release.

Как запустить

Простейший путь - Mistral Vibe, CLI-агент Mistral. Leanstral работает на бесплатном плане: включи «Labs models» в настройках аккаунта, создай API-ключ, установи Vibe и добавь Lean-агент.

Для self-hosting: vLLM версии 0.24.0 или новее. Сервер совместим с OpenAI-клиентом. Параметр reasoning_effort ставь в high для сложных задач и none для скорости.

Модель поддерживает OpenAI-style tool calling. Можно подключить функцию lean_run_code для компиляции фрагментов. Mistral также рекомендует сервер lean-lsp-mcp для плотной интеграции с Lean.

Веса доступны на Hugging Face.

Что это значит

Если ты работаешь с Rust или другими языками, где важна корректность, Leanstral даёт конкретный инструмент: автоматически строить свойства корректности и проверять их формально. Пять реальных багов в публичных репозиториях, о которых никто не знал, - это не абстрактный результат.

Для тех, кто занимается формальной верификацией или математикой в Lean 4, появился бесплатный агент с открытыми весами, который при достаточном токен-бюджете обходит коммерческие решения по соотношению результат/цена.

Источник: MarkTechPost, 3 июля 2025 - читать оригинал