模型将形式化推理拆解为三项独立能力：自动形式化（将自然语言数学问题转化为 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 次。
3 个赞
这论文怎么写的啊，要不是美团我都怀疑学术不端了，还有这种对比法，怎么和之前Google的论文一样
3 个赞
对比项太小众了么 
都是老模型，有的甚至不更新了，所以显得这个模型效果很好，对比的都还是对prover有利的数据集，其他的数据集没见，所以老模型打不过新模型分跑不过，我这模型就显得效果很好
嗷嗷，不过这好像是论文的基本操作了吧） 为师教你点真才实学，出了事情不要把为师说出来就好了.jpg
所以说还能这么比，之前Google那个论文也是，什么上古时代的老模型都拿出来对比了
哎这种属于是面向审稿人的论文了吧
乐色东西
美团赶紧更新thinking模型吧
因为本来就是为了这些训的模型
你拿其他资料集比没有意义
学术 != 产品
1 个赞
我寻思这个工作不就是做 Prover 吗，不测 Prover 数据集测什么
AlphaProof 也是一样啊，这些都是领域特定模型，事实证明做的就是好，才三四个月就有50引了，或者说你比 Nature 审稿人或者做这个方向的人更懂这个领域（
天天 sota 就是没人用，能不能别总只想着跑分，花点心思把模型做好用点
衡量一个Prover模型的水平，不应该看它在已知语法下背诵了多少旧定理，而应该看它在从未见过的逻辑结构下的泛化能力，先不说这几个测试集最晚的都发了至少一年半多了，这里面DeepSeek-prover-v2-671B以外剩下的哪有一个模型和570B一样大，有几个都不如它零头大，这难道不是一种大力出奇迹吗？这样的对比有什么意义嘞，怎么不多对比几个同级别的moe模型？这不就是一种大炮打蚊子
先不说论文发布给大公司放行这件事，我就说了美团为了这个sota特调了模型以大欺小算不算？AlphaProof能上Nature，是因为它在强化学习架构上实现了范式创新，和这种特调模型是一回事吗？
当你拥有2025年的算力、巨大的参数量和更新的合成数据时，如果你跑分不赢两年前的老模型，那反而是巨大的失败。赢了是为什么不是scaling law的功劳，怎么代表了它在逻辑推理上就有进化了？
AlphaProof证明了其价值，是因为它解决了IMO 2024的现场新题，MiniF2F-Test是2021年发布的，OlympiadBench是2024年初的，对于一个2026年发布的模型，这些数据集早已被洗过无数遍了，获取语料的时候没包进去吗？如果真牛的话为什么不拉出来拿新题比比，2025年的题都不做做吗？
先与 SOTA 模型比，然后再与 Prover 模型比
看起来没啥问题
至于找新题什么的，也要别人认才行
1 个赞
2025年的IMO题也有啊，怎么不一起发出来做做看看 
嘛，反正就几种可能
偏离焦点或效果不好之类的
而且 IMO-AnswerBench 也算包含 2025 年的题目吧
论文也硬
那些乱七八糟我先不谈，你就说有没有一个开源的同级别模型吧，大力出奇迹贡献了一个开源 SOTA Prover 模型不算贡献吗？
赢了是为什么不是 scaling law 的功劳，怎么代表了它在逻辑推理上就有进化了？
可以是 scaling law 的功劳啊，为什么不能呢？一个大大的 scaling law 放在这里我为什么不去用它呢？报告啊有任何地方声称了好处完全不是 scaling law 带来的吗
人家就是美团的，不调自己的模型调谁的模型？为什么就非得多调几个比啊
HisPO 没有做消融/对比，这是这个文章的一个比较严重的缺陷，但说的一文不值甚至“学术不端”（例如混测试数据etc.）你就得拿出能实锤的证据了
没办法调用对应的API，但是这是openrouter测试longcat flash chat的，这个模型去年八月发布的，测试的是去了特定信息的imo2023年第一题，模型直接用了2024年发布的思路，当然如果你说训练prover的时候特地避开了这个语料污染我也没办法
如果都是背题的话，这个sota发布了有什么意义嘞？
1 个赞
特定训练了现在都是，打比分大家