За даними 1M AI News , команда Meituan LongCat відкрила код LongCat-Flash-Prover — модель MoE з 560 мільярдами параметрів, спеціалізовану на математичних завданнях у мові формалізованого доведення теорем Lean4. Ваги моделі випущені за ліцензією MIT і вже доступні на GitHub, Hugging Face та ModelScope.
Модель розбиває формалізоване міркування на три незалежні здібності: автоматичну формалізацію (перетворення математичних задач у природній мові на формальні твердження Lean4), генерацію ескізу (створення каркасу доведення у стилі лем) та генерацію повного доведення. Усі три здібності реалізуються за допомогою інтеграції інструментів агента з інтерактивним перевірками через Lean4-компілятор (TIR).
Щодо навчання команда запропонувала Hybrid-Experts Iteration Framework для генерації даних для початкового етапу та ввела алгоритм HisPO на етапі підсиленого навчання для стабілізації довгострокового навчання моделі MoE, а також додала механізми перевірки теоретичної узгодженості та законності для запобігання reward hacking.
Результати тестування показують, що LongCat-Flash-Prover встановив нові рекорди SOTA у двох галузях — автоматичному формалізуванні та доведенні теорем — серед моделей з відкритими вагами. На наборі MiniF2F-Test досягнуто 97,1% успішності лише за 72 інференси, а на ProverBench і PutnamBench — 70,8% і 41,5% відповідно, при кількості інференсів на задачу не більше 220.