Meituan open-sources a 560B parameter theorem-proving model, achieving a 97.1% success rate over 72 inferences, setting a new open-source SOTA.

Gate News reports that on March 21, the Meituan LongCat team open-sourced LongCat-Flash-Prover, a MoE model with 560 billion parameters focused on mathematical reasoning tasks in the formal theorem proving language Lean4. The model weights are released under the MIT license and are available on GitHub, Hugging Face, and ModelScope.

This model breaks down formal reasoning into three independent capabilities: automatic formalization (converting natural language math problems into Lean4 formal statements), sketch generation (producing proof frameworks in lemma style), and complete proof generation. All three capabilities are integrated with reasoning (TIR) through the Agent toolkit, which interacts with the Lean4 compiler for real-time verification.

For training, the team proposed the Hybrid-Experts Iteration Framework to generate cold-start data. During reinforcement learning, the HisPO algorithm was introduced to stabilize long-term training of the MoE model, along with theorem consistency and validity checks to prevent reward hacking.

Benchmark results show that LongCat-Flash-Prover sets new state-of-the-art in automatic formalization and theorem proving among open-source models. On MiniF2F-Test, it achieved a 97.1% pass rate with only 72 inference attempts. On ProverBench and PutnamBench, it reached 70.8% and 41.5%, respectively, with no more than 220 inference steps per problem.