Meituan открывает 560B параметров модель доказательства теорем с частотой прохождения 97.1% на 72 выводах, обновляя открытый SOTA

Новости Gate: 21 марта команда LongCat от Meituan выпустила в открытый доступ LongCat-Flash-Prover — модель MoE с 560 миллиардами параметров, ориентированную на математические рассуждения в формализованном языке доказательств теорем Lean4. Весовые коэффициенты модели опубликованы по лицензии MIT, модель доступна на GitHub, Hugging Face и ModelScope.

Эта модель разбивает формализованные рассуждения на три независимых способности: автоматическую формализацию (преобразование математических задач на естественном языке в формальные выражения Lean4), генерацию набросков (создание доказательных каркасов в стиле лемм) и полное создание доказательств. Все три способности интегрированы с помощью инструментария Agent, который осуществляет интерактивное взаимодействие и проверку рассуждений в реальном времени через TIR и компилятор Lean4.

В части обучения команда предложила Hybrid-Experts Iteration Framework для генерации стартовых данных, а на этапе обучения с подкреплением внедрила алгоритм HisPO для стабилизации долгосрочного обучения MoE-модели, а также добавила механизмы проверки согласованности и легитимности теорем, чтобы предотвратить манипуляции с наградой (reward hacking).

Бенчмарки показывают, что LongCat-Flash-Prover обновил состояние искусства по автоматической формализации и доказательству теорем среди моделей с открытыми весами. На тесте MiniF2F он достигает 97,1% успешных решений всего за 72 рассуждения, а показатели ProverBench и PutnamBench составляют 70,8% и 41,5% соответственно, при числе рассуждений на задачу не более 220.