美團開源560B引數定理證明模型：72次推理通過率97.1%，重新整理開源模型SOTA

美團 LongCat 團隊開源 LongCat-Flash-Prover，一個 5600 億引數的 MoE 模型，專攻形式化定理證明語言 Lean4 的數學推理任務。模型權重以 MIT 協議釋出，已上線 GitHub、Hugging Face 和 ModelScope。 模型將形式化推理拆解為三項獨立能力：自動形式化（將自然語言數學問題轉化為 Lean4 形式語句）、草圖生成（產出引理風格的證明框架）和完整證明生成。三項能力均通過 Agent 工具整合推理（TIR）與 Lean4 編譯器實時互動驗證。 訓練方面，團隊提出 Hybrid-Experts Iteration Framework 生成冷啟動資料，並在強化學習階段引入 HisPO 演算法穩定 MoE 模型的長程任務訓練，同時加入定理一致性和合法性檢測機制防止 reward hacking。 基準測試顯示，LongCat-Flash-Prover 在開源權重模型中重新整理了自動形式化和定理證明兩項 SOTA。MiniF2F-Test 上僅用 72 次推理即達 97.1% 通過率，ProverBench 和 PutnamBench 分別達到 70.8% 和 41.5%，每題推理次數不超過 220 次。 [1M AI News]