Согласно мониторингу 1M AI News, команда Meituan LongCat открыла исходный код LongCat-Flash-Prover — модель MoE с 560 миллиардами параметров, специализирующуюся на математических задачах в языке формализованного доказательства теорем Lean4. Веса модели выпущены по лицензии MIT и уже доступны на GitHub, Hugging Face и ModelScope.
Модель разбивает формализованное рассуждение на три независимые способности: автоматическую формализацию (преобразование математических задач на естественном языке в формальные утверждения Lean4), генерацию эскиза (создание каркаса доказательства в стиле леммы) и генерацию полного доказательства. Все три способности реализуются через интеграцию инструментов агента с интерактивным подтверждением в реальном времени с компилятором Lean4.
В области обучения команда предложила гибридную экспертную итерационную рамку для генерации данных при холодном запуске, а на этапе обучения с подкреплением внедрила алгоритм HisPO для стабилизации долгосрочного обучения модели MoE, а также добавила механизмы проверки теоретической согласованности и легитимности для предотвращения reward hacking.
Тестирование показало, что LongCat-Flash-Prover установил новые рекорды в автоматической формализации и доказательстве теорем среди моделей с открытыми весами. На MiniF2F-Test достигнута точность 97,1% всего за 72 итерации, а на ProverBench и PutnamBench — 70,8% и 41,5% соответственно, при не более чем 220 итерациях на задачу.