Мейтуань випустила відкриту модель доведення теорем з 560 мільярдами параметрів, яка досягає 97,1% успішності за 72 кроки висновку, оновлюючи світовий рекорд у відкритому сегменті.

Gate News повідомляє, 21 березня команда LongCat від Meituan відкрила вихідний код LongCat-Flash-Prover — модель MoE з 5600 мільярдами параметрів, яка зосереджена на математичних доведеннях у формалізованій мові Lean4. Ваги моделі опубліковані за ліцензією MIT і вже доступні на GitHub, Hugging Face та ModelScope.

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

Щодо тренування, команда запропонувала гібридну ітераційну рамку Hybrid-Experts для генерації стартових даних, а на етапі підкріплювального навчання застосувала алгоритм HisPO для стабілізації довгострокового тренування MoE-моделі, а також додала механізми перевірки відповідності та легітимності теорем для запобігання шахрайству з винагородою.

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