№putnambench·concept
PutnamBench
别名
- 首次出现
- 2026-06-05
- 最近出现
- 2026-07-06
- 累计提及
- 10
§ 01综述
PutnamBench 是一个面向高等数学问题求解与形式化证明的基准测试，它基于威廉·洛厄尔·普特南数学竞赛（William Lowell Putnam Mathematical Competition）的 672 道题目，要求参赛者用 Lean 4 证明助手将解答形式化。作为衡量 AI 在数学推理和定理证明领域能力的关键指标，PutnamBench 近年来成为各大 AI 模型比拼数学能力的战场。
PutnamBench 近期进展
Leanstral 1.5 模型创纪录：Mistral AI 发布的 Leanstral 1.5（119B MoE），专为 Lean 4 代码生成设计，成功解决了 PutnamBench 中 587/672 道题目，超越此前所有模型，且基于 Apache-2.0 开源协议，降低了使用门槛。Mistral AI发布Leanstral 1.5：Apache-2.0的Lean 4代码Agent可解587道Putnam题
Goedel-Architect 新突破：研究者提出 Goedel-Architect 框架，通过蓝图生成与精炼策略，在 PutnamBench 等基准上取得了接近最优的表现，展示了从自然语言到形式化证明的新路径。Goedel-Architect：通过蓝图生成与精炼实现形式化定理证明新突破
当前焦点与观察点
当前 PutnamBench 的竞争已从单一模型能力转向智能体与工具链整合：Leanstral 1.5 通过 MoE 架构和细粒度训练大幅提升数学形式化效率，而 Goedel-Architect 则强调分步推理的自适应策略。值得注意的是，这些进展均依赖开源生态，且成果可直接复现。随着解决题目比例接近 90%（587/672），下一阶段焦点可能是剩余难题的攻克，以及如何将这些能力迁移到现实数学研究场景。