Gate News 消息，3月21日，美團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次。
