Leanstral 1.5: карточка модели Mistral для формальных доказательств в Lean 4

Leanstral 1.5 — специализированная модель для работы с формальными доказательствами в Lean 4. Она помогает переводить математические утверждения в формальный язык, искать шаги доказательства и исправлять ошибки в репозитории. Сравнивать её с обычным чат-ботом по красоте объяснения бессмысленно: ценность появляется, когда результат принимает компилятор Lean и он воспроизводится в заданной версии проекта.

Архитектура и контекст

В документации указано 119 млрд общих параметров и около 6,5 млрд активных на запрос. Это разреженная схема: вычисляются не все параметры одновременно. Контекст достигает 256 тысяч токенов, максимальный выход — 128 тысяч. Большой лимит полезен для репозитория с импортами и вспомогательными леммами, но не гарантирует, что модель выберет актуальную версию библиотеки.

Какие задачи ей подходят

Практический сценарий — завершить доказательство с пропущенным шагом, найти несовместимый импорт или предложить формализацию текстовой гипотезы. Модель также может участвовать в агентном цикле: написать код, запустить Lean, прочитать ошибку и сделать следующую попытку. Финальным критерием остаётся успешная проверка инструментом, а не уверенность ответа.

Почему это не «математический оракул»

Компиляция подтверждает корректность формального выражения относительно аксиом и библиотек, но не гарантирует, что формализация точно отражает исходную человеческую задачу. Можно безупречно доказать не то утверждение. Поэтому специалист проверяет соответствие между текстом, формальной постановкой и выбранными допущениями.

Лицензия и доступ

Leanstral 1.5 опубликована с открытыми весами под Apache 2.0 и доступна как исследовательская модель. Документация Mistral указывает бесплатный доступ к API, но лабораторный статус означает необходимость следить за сроками поддержки. Для проекта важнее скачать точную версию и сохранить окружение, чем полагаться на постоянство публичного endpoint.

Как тестировать в репозитории

Зафиксируйте версию Lean, mathlib и список импортов. Выберите десять завершённых доказательств и временно скройте несколько шагов. Модель должна восстановить их без изменения формулировки теоремы. Затем добавьте реальные незавершённые задачи и считайте число компиляционных циклов, время и долю ручных правок. Не включайте в оценку примеры, которые могли входить в обучение, если происхождение неизвестно.

Безопасная агентная петля

Запускайте модель в отдельной ветке и ограниченном контейнере. Разрешите изменять только файлы эксперимента. После каждой попытки сохраняйте diff и вывод Lean. Агент не должен автоматически принимать новые аксиомы, отключать проверки или менять формулировку цели ради зелёной сборки. Эти действия являются изменением задачи, а не решением.

Где модель может дать реальную пользу

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

Связанные материалы

Организацию повторяемых экспериментов мы разобрали в гайде по исследовательскому воркбенчу. Перед запуском агента пригодится чек-лист проверки прав.

FAQ

Может ли Leanstral доказать любую теорему?

Нет. Она предлагает и проверяет шаги в пределах доступных библиотек, контекста и вычислительного бюджета.

Нужен ли специалист по Lean?

Да. Без него легко принять корректно скомпилированную, но неверно поставленную формализацию.

Что сохранять после эксперимента?

Версии Lean и библиотек, исходный запрос, diff, журналы компиляции и финальный проверенный файл.

Когда отказаться от использования

Если проект не собирается воспроизводимо без модели, сначала исправьте окружение. Leanstral не должна маскировать конфликт зависимостей или отсутствие тестов. Откажитесь от автоматического цикла, когда агент регулярно меняет формулировку теоремы, добавляет недопустимые аксиомы или создаёт слишком большой diff для проверки человеком. В учебной работе заранее определите, какие подсказки разрешены: готовое доказательство может лишить упражнение смысла. В исследовательском проекте каждое принятое изменение должно проходить обычное рецензирование, даже если Lean подтвердил синтаксическую корректность и типы.

Повторный прогон выполняйте в чистом окружении, чтобы случайный локальный кэш не создавал ложное ощущение воспроизводимости.

Как читать заявленные результаты

Бенчмарки формальных доказательств полезнее обычных голосований, потому что решения можно проверить компилятором. Но высокий pass@k означает, что модели разрешили несколько попыток; это не то же самое, что правильный ответ с первого запуска. Для планирования ресурсов сохраняйте распределение: сколько задач решено сразу, сколько потребовало восьми попыток и где понадобилась ручная правка.

Критерий принятия в команду

Модель оправдана, если уменьшает время до проверенного коммита, а не просто генерирует больше текста Lean. Сравните неделю работы без помощника и с ним на одинаковых типах задач. Учитывайте время чтения diff, число бесполезных циклов и случаи, когда модель изменила постановку. Если выигрыш держится только на знакомых учебных примерах, область применения нужно сузить. Для production важны повторяемая сборка и понятная ответственность за формализацию.

Отдельно отмечайте задачи, где специалисту пришлось переписать постановку до запуска модели. Это время относится к процессу и не должно исчезать из итоговой оценки эффективности.