On the journey of large models moving into vertical and specialized fields, Meituan has just submitted a remarkable answer that has drawn attention from both the academic and industrial communities.

On March 21, Meituan officially open-sourced a large-scale mathematical proof model named LongCat-Flash-Prover. This giant with 567.7 billion parameters employs an advanced MoE (Mixture of Experts) architecture, and has been deeply optimized for extremely complex mathematical formal proof problems.

image.png

In top-tier benchmark tests measuring model logical reasoning capabilities, LongCat-Flash-Prover has demonstrated dominant strength:

Breaking Records: Achieved an impressive score of 97.1% in the MiniF2F-Test, requiring only 72 reasoning attempts.

Overcoming Challenges: Successfully solved 41.5% of the problems in the PutnamBench task. Both of these figures set new global SOTA (State-of-the-Art) records.

To truly give large models the rigor of a "mathematician," Meituan has achieved several key technical breakthroughs:

Eliminating Hallucinations: Introduced a multi-stage strict verification process based on AST (Abstract Syntax Tree), and integrated Lean4 formal language, fundamentally eliminating AI's "nonsense" in logical deduction.

Training Algorithm Evolution: To address the chronic instability of long-range tasks in MoE models, Meituan introduced its self-developed HisPO algorithm, combined with a theorem consistency detection mechanism, effectively preventing the "cheating" reward hacking behavior of the model during the reinforcement learning phase.

Efficient Architecture: The total parameter count of 560 billion ensures the model's profound knowledge base, while the MoE architecture ensures flexibility and efficiency during inference.

Currently, Meituan has fully open-sourced this model and its code on GitHub and Hugging Face platforms.

With the launch of LongCat-Flash-Prover