2026-03-21 02:27:21
Meituan открывает 560B параметров модель доказательства теорем с частотой прохождения 97.1% на 72 выводах, обновляя открытый SOTA
Команда Meituan LongCat открыла исходный код LongCat-Flash-Prover 21 марта — модель MoE с 560 миллиардами параметров, ориентированная на формализованное доказательство теорем в Lean4. Модель разделена на три функции: автоматическая формализация, генерация эскизов и генерация полных доказательств, в сочетании с инструментами вывода и компилятором Lean4 для достижения проверки в реальном времени. Обучение использовало гибридную структуру итерации экспертов (Hybrid-Experts Iteration Framework) и алгоритм HisPO для предотвращения манипуляций с вознаграждениями. Тесты производительности показали, что модель обновила рекорды открытых взвешенных моделей в автоматической формализации и доказательстве теорем.