北京
给AI一道研究生级别的数学题，它不能只给答案，还得写出能通过机器检查的证明。这就是ProofBench在做的事。
这个基准由Vals AI联合一批Lean 4专家打造，专门衡量形式化定理证明能力。每道题都配有一句自然语言的定理陈述，以及一份经过审核的Lean 4形式化版本。模型要做的，是产出一份能被Lean 4检查器接受的证明。
题目难度落在研究生或高年级本科水平，覆盖分析、代数、概率、数论和逻辑几个方向。榜单跑在一个不公开的100道题的私有切分上，模型以智能体方式工作，可以调用Mathlib搜索和代码执行工具，每道题最多允许40轮交互。
分数怎么算
数据来自Vals AI公开的ProofBench榜单。图表呈现的是证明成功率，也就是模型的Lean 4证明通过形式化检查器的题目占比。
评分是二元的，每道题要么过要么不过，没有部分分。榜单的标准误、推理强度设置、延迟和单次测试成本，都保留在数据导出里。
因为证明是由Lean 4编译器检查，而不是由某个裁判模型打分，所以分数反映的是经过验证的形式正确性。每个模型只出现一次，采用Vals AI选定的固定推理强度配置。
榜单里还有个特殊选手
榜单还收录了Harmonic的Aristotle定理证明系统。它运行在自己的测试框架里，数据被存储下来，但没有进入图表排名。
形式化验证的好处在于，它把"证明对不对"这件事从主观判断变成了编译器的确定性输出。没有裁判偏好，没有评分尺度争议，过就是过。
代价也很直接：二元评分意味着没有中间地带，一道题卡在最后一步和完全没思路，在分数上没有任何区别。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
