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
In top-tier benchmark tests measuring model logical reasoning capabilities,
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
Currently, Meituan has fully open-sourced this model and its code on GitHub and Hugging Face platforms.
With the launch of
