Архитектура и доступность
Новая модель Leanstral 1.5 входит в семейство Mistral Small 4 и предназначена для автоматического доказательства теорем и инженерии доказательств в системе Lean 4. Модель использует архитектуру Mixture-of-Experts (MoE) с общим объемом 119 миллиардов параметров, из которых активными являются только 6.5 миллиарда на каждый токен. Это обеспечивает высокую вычислительную эффективность при поддержке контекстного окна в 256 000 токенов.
Модель принимает мультимодальный ввод (текст и изображения) и выдает текстовый результат. Весы опубликованы под лицензией Apache 2.0, что позволяет свободное использование. Доступен бесплатный API-эндпоинт, а также локальная установка через vLLM.
Результаты на бенчмарках
Leanstral 1.5 демонстрирует выдающиеся результаты в области формальной верификации. Модель достигла 100% точности на датасете miniF2F и решила 587 задач из 672 в PutnamBench. По сравнению с предыдущей версией (Leanstral-2603), модель значительно улучшила показатели на алгебраических бенчмарках FATE-H и FATE-X.
| Бенчмарк | Результат Leanstral 1.5 | Примечание |
|---|---|---|
| miniF2F (val + test) | 100% | Полное насыщение датасета |
| PutnamBench | 587 / 672 | Решено 87.3% задач |
| FATE-H | 87% | Новый state-of-the-art |
| FATE-X | 34% | Новый state-of-the-art |
| FLTEval (pass@1) | 28.9 | Рост с 21.9 |
| FLTEval (pass@8) | 43.2 | Превосходит Opus 4.6 (39.6) |
Экономическая эффективность и масштабирование
Ключевое преимущество Leanstral 1.5 — радикальное снижение стоимости вычислений. Решение одной задачи PutnamBench обходится примерно в $4. Для сравнения, аналогичная задача с использованием Seed-Prover 1.5 в высоком режиме настройки требует бюджета в 10 дней работы GPU H20, что оценивается в $300 и более. Модель Aleph Prover обходится в $54–68 за задачу.
Производительность модели сильно зависит от бюджета токенов на попытку (test-time scaling). При увеличении лимита токенов с 50k до 4M количество решенных задач в PutnamBench возрастает с 44 до 587. Это позволяет гибко балансировать между скоростью и точностью в зависимости от сложности задачи.
Практическое применение: от математики к поиску багов
Хотя модель обучалась преимущественно на математических данных, она успешно применяется для верификации программного кода. В ходе тестирования Leanstral 1.5 доказал временную сложность O(log n) для реализации дерева AVL, используя структурную индукцию и монаду TimeM. Процесс занял 2.7 миллиона токенов и 22 сжатия контекста.
Также модель использовалась для поиска багов в открытых репозиториях. С помощью автоматизированного пайплайна Aeneas, переводящего Rust в Lean, модель проверила 57 репозиториев. Она выявила 47 нарушенных свойств и 11 реальных багов, пять из которых ранее не были зафиксированы в GitHub. Один из найденных багов приводил к переполнению при вводе максимального значения U64 в функции zigzag decoding, вызывая сбои в режиме отладки и скрытую порчу данных в релизной сборке.
Как начать работу
Для быстрого старта рекомендуется использовать CLI Mistral Vibe. Пользователям необходимо активировать раздел 'Labs models' в аккаунте, установить Vibe и добавить Lean-агент. Для локального развертывания требуется vLLM версии 0.24.0 или новее. Модель поддерживает вызовы инструментов (tool calling) в стиле OpenAI, что позволяет интегрировать её с компиляторами и языковыми серверами Lean.
Бенчмарки
| Бенчмарк | Leanstral 1.5 | Opus 4.6 |
|---|---|---|
| FLTEval pass@1 | 28.9% | 39.6% |
| FLTEval pass@8 | 43.2% | 39.6% |
Жирным — лучший результат в строке. Источник цифр — официальная публикация.
Источник: MarkTechPost ↗