📌 📄 内容摘要:
谨言慎行 (@Anano) 在 美团开源560B参数定理证明模型：72次推理通过率97.1%，刷新开源模型SOTA 中发帖
[image]
模型将形式化推理拆解为三项独立能力：自动形式化（将自然语言数学问题转化为 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%，每题推理次数不...
────────── 链接信息 ──────────
🔗 论坛链接: linux.do
📎 访问地址: https://linux.do/t/topic/1792278/1
─────────────────────────────
📢 来源：LINUX DO
