Sou Hu Cai Jing·2026-03-22 12:22Core Insights - Meituan has open-sourced the LongCat-Flash-Prover model, which features 567.7 billion parameters and utilizes a mixture of experts (MoE) architecture to address complex mathematical proof challenges [1][3]. Group 1: Model Features - The model incorporates a hybrid-experts iteration framework designed to generate large-scale, high-quality formal reasoning trajectories [3]. - It integrates Lean4 and an AST-based multi-stage rigorous verification process to eliminate "hallucination" phenomena [3]. Group 2: Training and Performance - The training process employs a hybrid-experts iteration framework to generate cold-start data, and the HisPO algorithm is introduced during the reinforcement learning phase to stabilize long-range task training of the MoE model [3]. - The model includes mechanisms for theorem consistency and legality checks to prevent reward hacking [3]. - Benchmark tests indicate that the model achieved a score of 97.1% on the MiniF2F-Test with only 72 reasoning attempts, and solved 41.5% of problems on the PutnamBench task using 118 reasoning attempts, setting a new state-of-the-art (SOTA) level in both tests [3]. Group 3: Open Source Information - The open-source model is available on GitHub and Hugging Face [4].