Varto用Isabelle完成PutnamBench全部证明：AI数学推理进入可验证时代

最近一段时间AI 解数学题的能力肉眼可见地在变强。对话里给一个微积分、数论或者组合题主流大模型往往能给出像模像样的推导步骤甚至最终答案也经常是对的。但问题是你信它吗更准确地说你能证明它“真的会”吗传统的 AI 数学基准测试大多只比对最终答案少数会做分步打分但推理过程本质上是“人看模型写了什么”而不是“机器验证了它是正确的”。于是出现了一个一直存在的尴尬模型可能在第三步就偷换概念第五步用了不存在的定理最后答案却碰巧对了。这种“答案对但过程错”的情况在传统评测里几乎无法被有效拦截。Varto 最近公布的结果把这件事往前推进了一大步。根据项目标题的表述Varto 在 Isabelle 定理证明器中完成了 PutnamBench 全部题目的形式化证明。这里的“完整证明”不是修辞而是一个机械可验证的状态每一道题目都生成了 Isar 证明脚本并且通过了 Isabelle 证明器的逐行检查。这篇文章会重点拆解三件事PutnamBench 到底有多难、Isabelle 验证链路是如何工作的、Varto 这类项目为什么值得关注。同时我会给出一条可以在本地复现的 Isabelle AI 证明工作流让你亲手体会到“机器真正看懂证明”和“人觉得证明没问题”之间的差异。如果你正在研究 AI Agent、AI 编程或者数学推理验证这篇文章适合你。1. 这篇文章真正要解决的问题先说一个反常识的现象目前大多数 AI 数学评测本质上是在“信任模型的自述”。你让模型写完整推导然后人工或规则引擎判断推导是否合理。但人工判断会累规则引擎容易被训练集过拟合而且两者都很难回答一个问题模型给出的推理链路是否每一步都符合严格的逻辑规则形式化数学验证提供了另一种思路。它不判断模型的“推理过程看起来合不合理”而是要求模型先把自然语言题目转写成定理证明器能够理解的形式化命题再给出一个证明脚本最后由证明器自动检查这个证明是否成立。如果成立那就是成立的如果不成立证明器会指出是哪一步出了问题。Varto 的意义在于它把这条链路做成了一种可复现的成果在 Isabelle 中完成了 PutnamBench 的完整证明。这意味着它覆盖的不是题库里的随机子集也不是人工筛选后的“简单题”而是全部题目。读这篇文章你能获得什么理解 PutnamBench 的定位以及它为什么是 AI 数学推理的“试金石”掌握 Isabelle 与 Isar 语言的基础用法以及如何把一道数学题转写成可证明的理论文件看懂 Varto 这类“AI 证明器”项目的技术路径模型生成证明脚本证明器给出反馈Agent 根据反馈迭代修复学会自己搭一条最小验证链路包括环境准备、代码示例、运行验证和常见问题排查。与其继续在“AI 数学能力到底行不行”这种大问题上争论不如看一套可以机械验证的标准。这正是 Varto 这个结果值得专门写一篇文章来分析的原因。2. PutnamBench、Isabelle 与 Varto先厘清三个概念2.1 PutnamBench为什么是“普特南竞赛题”而不是普通数学题PutnamBench 是以普特南数学竞赛题目为素材构建的 AI 数学推理基准测试。普特南数学竞赛是北美面向本科生的一项高难度数学竞赛它的题目不依赖高等数学的机械计算而是大量考察组合数学、数论、代数、概率和不等式的创造性证明。很多题目的难点不是“算不出来”而是“不知道往哪个方向想”。对 AI 来说这类题目比常规计算题更难因为它要求模型具备几项能力的组合理解自然语言描述的数学问题把问题准确地转写成严格的数学表达式构造一条完整的推理路径再进一步把这条推理路径写成证明器能够接受的形式化脚本。PutnamBench 作为基准测试价值就在于它的题目覆盖面广、难度高不容易靠背题或简单模板糊弄过去。如果一个系统能在 PutnamBench 上完成形式化证明说明它不是“猜了个答案”而是产出了一条可以被独立验证的完整推理链。2.2 Isabelle不是“自动解题器”而是“证明检查器”Isabelle 是一个交互式定理证明器常被简称为 Isabelle/HOL。它有一套严谨的逻辑体系支持用 Isar 语言书写结构化证明。很多人第一次用 Isabelle 会感到困惑为什么我写一个“显然成立”的结论还要证明因为 Isabelle 的定位不是帮你猜答案而是逐条检查你写的每一步是否可以从现有公理和引理推导出来。和 Lean、Coq 类似Isabelle 也属于“人与机器协作写证明”的工具。区别在于Isabelle 的 Isar 语言更接近结构化数学论文的写法读起来比某些证明器的底层策略更容易理解。同时Isabelle 提供了 Sledgehammer、Nitpick、Quickcheck 这类自动化工具。Sledgehammer 会把当前目标交给多个外部自动证明器搜索证明Nitpick 则尝试构造反例来告诉你“这个命题是错的”。Varto 选择 Isabelle而不是其他证明器从工程角度看是合理的。Isabelle 的自动化工具链相对成熟Isar 脚本可读性好而且大规模数学形式化项目有不少积累。当一个 AI Agent 需要通过“生成脚本 - 证明器反馈 - 修改脚本”的循环来逼近正确证明时证明器的错误信息是否清晰、自动化工具是否好用直接影响迭代效率。2.3 Varto把自然语言数学题变成 Isabelle 证明脚本的项目Varto 是一个把自然语言数学问题转化为 Isabelle 形式化证明的 AI 项目。它的输入是一道数学题的文字描述输出是一个 .thy 理论文件里面包含形式化的命题陈述和对应的 Isar 证明脚本。如果证明脚本没有完全通过 Isabelle 的检查系统就根据错误反馈继续修复直到所有证明目标关闭。从技术路径来看Varto 本质上是一个面向形式化证明场景的 AI Agent。它要处理的不是“代码能否编译”而是“证明脚本能否通过证明器”。这两件事没有本质区别证明器也是一种严格得多的编译器。代码编译不过会报错证明器检查不过同样会告诉你哪个子目标没有关闭、哪个引理不存在、哪个类型不匹配。Varto 最受关注的一点是“完整”二字。它不是在采样后的部分题目上成功而是在整个 PutnamBench 测试集上通过 Isabelle 验证。这意味着它的能力已经超越了“模型碰巧会做几道题”的阶段形成了一条稳定的题目理解、形式化转写、证明搜索、错误修复的流水线。3. “完整证明”为什么值得关注AI 数学验证的范式变化如果把“AI 会做数学题”的标准定义成“最终答案正确”那很多模型早就达标了。但这个标准有一个明显的漏洞答案对不代表推理对更不代表模型掌握了解这类题的规律。传统基准测试至少有四个问题问题说明只看结果最终答案对了就算对过程错误可能被漏掉数据污染竞赛题和解答在网上大量存在模型可能训练过评分主观分步评分依赖人工规则成本高且标准难统一不可复现同一个模型每次生成不同难以稳定复现推理过程形式化证明可以同时缓解这四个问题。证明器只认逻辑推导不认“差不多”证明脚本是文本可以完整保存每个步骤都可以回溯验证任何一次运行都能留下明确的成功或失败记录。当 AI 生成的不再是“答案”而是一份可以被证明器逐行检查的证明脚本时它的推理链路就变成了可以被审计的工程资产。Varto 完成 PutnamBench 的完整证明信号意义就在这里AI 数学能力评测正在从“看答案”走向“看证明”。这种变化对工程实践也有直接启发。AI Agent 在写代码时编译器本身就是验证器AI Agent 在写数学证明时证明器就是验证器。如果一个系统能够在验证器存在的情况下完成全部任务它的输出质量就比“自己说了算”的系统可信得多。当然这里并不是说 AI 从此彻底解决了数学推理问题。完整证明只说明它在当前题目集上通过了验证不说明它掌握了无限扩展的数学能力。但至少它让“AI 会数学”这件事从营销话术变成了有证据支撑的工程结论。4. 环境准备搭建 Isabelle 与 AI 证明工作流要理解 Varto 这类项目最好亲自动手跑一个最小流程。下面从环境搭建开始。4.1 安装 IsabelleIsabelle 是跨平台工具官方提供预编译版本。安装时注意版本与操作系统架构匹配不同发行版的依赖差异不大。如果你在 Linux 服务器上使用建议下载 tar.gz 包并解压到固定目录然后配置环境变量。# 以 Linux 下解压安装为例 tar -xzf Isabelle2024_linux.tar.gz export ISABELLE_HOME/opt/Isabelle2024 export PATH$ISABELLE_HOME/bin:$PATH # 查看版本 isabelle version注意这里示例中的版本号只是演示实际安装请以你下载的发行版目录名为准。Isabelle 自带 jEdit 图形界面同时也支持纯命令行的 batch 模式。做自动验证时不要依赖图形界面要习惯用isabelle build。4.2 创建第一个理论文件Isabelle 的理论文件后缀是 .thy用 theory 关键字声明。一个最简单的理论文件如下theory Demo imports Main begin lemma add_commute: fixes n m :: nat shows n m m n by (induct n) simp_all end把这个文件保存为 Demo.thy然后在同一目录下创建 ROOT 文件。session Demo HOL theories [document false] Demo然后运行isabelle build -D .如果一切正常你会看到类似Finished Demo的输出。这代表 Demo 理论中的所有引理都通过了证明器检查。4.3 接入 AI 模型生成 Isar 脚本Varto 这类系统的核心循环是把自然语言题目交给大模型让模型生成 Isar 证明脚本把脚本写入临时 .thy 文件调用 Isabelle 编译根据编译错误反馈给模型继续修复。这里的关键在于模型的输入输出契约要稳定。一个简单的提示词设计思路如下你是一名 Isabelle/HOL 形式化证明专家。 请把下面的数学问题转写成 Isabelle 理论文件并给出完整的证明脚本。 要求 1. 使用 Isar 语言编写证明 2. 不要使用 sorry 3. 确保所有类型标注清晰 4. 如果目标无法一次性证明可以把主定理拆成若干中间引理。 题目 这里填写自然语言数学题模型输出的是 Markdown 代码块或纯文本的 .thy 文件内容。接下来用一个Shell脚本把生成内容写入理论文件并执行验证。这样就有了一个最小可运行的 AI 证明工作流。5. 完整示例从问题到 Isabelle 证明脚本这一节给出三个层次的示例。第一个示例可以完整跑通第二个演示 Putnam 风格题目的形式化结构第三个是 AI Agent 的管线伪代码。5.1 示例一一条最简单的机器可验证证明创建一个新的理论文件DemoAdd.thytheory DemoAdd imports Main begin lemma left_zero: fixes n :: nat shows 0 n n by simp lemma succ_add: fixes n m :: nat shows Suc n m Suc (n m) by simp theorem add_commutative: fixes n m :: nat shows n m m n by (induct n) simp_all end这段代码里的by (induct n) simp_all表示对 n 做数学归纳法然后用简化器处理所有子目标。它是 Isabelle 中最常见的证明策略之一。运行isabelle build -D .如果所有理论都显示 Finished就代表证明通过。写这段代码时要注意一个问题Isabelle 里的nat加法和普通数学里的加法在直觉上一样但每个引理都必须由机器验证。你写by simp证明器会检查它自己是否能从定义和已有引理中推出目标它不会因为“这显然是对的”就放过你。5.2 示例二模拟 Putnam 风格的求和题形式化Putnam 风格的题目通常需要构造一个完整的推导而不是直接套公式。这里用一个经典求和公式做演示它不属于 Putnam 原题但结构类似theory PutnamLikeDemo imports Main begin theorem sum_of_first_n: fixes n :: nat shows 2 * (\Sumk1..n. k) n * (n 1) apply (induct n) apply simp_all done end在这个公式里\Sumk1..n. k是区间求和k从 1 到 n。整段代码在 Isabelle 中运行时apply (induct n)会把目标分成基础情形和归纳步骤然后用simp_all化简。实际验证时如果simp_all不能一次完全关闭子目标你就需要把归纳步骤拆成更细的引理或者使用 Sledgehammer 搜索可用引理。这个例子演示的是形式化工作的日常写目标、拆目标、让自动化工具帮忙、不行就继续拆。PutnamBench 的题目比这个复杂得多但基本节奏是一致的。所谓的“完整证明”就是所有子目标最终全部关闭没有sorry没有oops。5.3 示例三AI 证明 Agent 的管线伪代码下面用 Python 伪代码演示一个基于模型生成和证明器反馈的迭代循环# 伪代码仅演示 Agent 循环结构 import subprocess def run_isabelle(theory_content: str) - dict: with open(/tmp/agent_demo/AgentDemo.thy, w) as f: f.write(theory_content) result subprocess.run( [isabelle, build, -D, /tmp/agent_demo], capture_outputTrue, textTrue, timeout120, ) return { returncode: result.returncode, stdout: result.stdout, stderr: result.stderr, } def prove_with_model(problem_text: str, model) - dict: messages [ {role: system, content: 你是 Isar 证明生成助手不要使用 sorry。}, {role: user, content: f请为以下问题生成 Isabelle 证明\n{problem_text}}, ] for step in range(3): generated model.generate(messages) result run_isabelle(generated[theory_content]) if result[returncode] 0 and Finished AgentDemo in result[stdout]: return {status: proved, theory: generated[theory_content]} feedback extract_isabelle_errors(result[stdout]) messages.append({role: assistant, content: generated[theory_content]}) messages.append({role: user, content: f证明未通过错误如下\n{feedback}\n请修复。}) return {status: failed, last_output: result[stdout]}这段代码的关键设计是把 Isabelle 的编译输出当作模型的环境反馈。模型第一次生成的证明脚本大概率过不了但这不是问题只要错误信息能传回模型修正后的脚本就更接近正确解。这种“生成 - 执行 - 反馈 - 修复”就是 AI Agent 在形式化证明领域的基本工作模式。6. 验证结果与效果判断运行一个 Isabelle 理论文件后结果不是“看起来对了”而是有明确的状态标记。验证成功的标志是isabelle build输出显示Finished YourTheory并且理论文件里没有sorry、oops、undefined等占位项。此时你可以说这个定理的证明已经被机器独立验证了。验证失败时常见输出包括Failed to apply proof method当前证明方法不足以关闭子目标Failed to finish proof还有子目标没有关闭Undefined fact引用了不存在的引理Type unification failed类型推断不一致。如果你的目标是验证 AI 生成的证明不要只看模型说的“我证完了”要运行isabelle build查看实际输出。Finished三个字比模型的一句解释可靠得多。这也是 Varto 结果具备公信力的原因它输出的不是一段“看起来合理的思路”而是可以直接被证明器重放验证的文件。7. 常见问题与排查思路在 Isabelle 和 AI 证明工作流中下面这些问题比较常见问题现象可能原因排查方式解决方案Failed to apply proof method证明策略不够强或缺少必要引理查看当前子目标状态尝试try、sledgehammer补充中间引理或者切换归纳法Type unification failed题目转写时类型标注不清检查:: nat、:: int、:: real是否准确显式声明变量类型避免类型推断歧义Undefined fact引理名拼写错误或未导入对应库使用find_theorems搜索可用引理修正引理名或补充importsSledgehammer timed out单步目标过大拆分引理缩小证明步骤把主定理拆成多个辅助引理Found proof but could not replay外部自动证明器找到了证明但 Isabelle 本地无法重放检查当前会话和依赖库是否一致固定 Isabelle 版本和依赖重复执行确认如果 AI 生成的证明脚本在 Isabelle 中反复失败优先检查类型转写。自然语言里的“整数”和“自然数”在形式化时可能是完全不同的类型一个int与nat混用往往会让 80% 的证明策略失效。8. 最佳实践与工程建议8.1 转写规范先定类型再写命题把自然语言问题转写成 Isabelle 命题时第一件事是确定变量类型。竞赛题里经常出现“正整数”“整数”“实数”它们在 Isabelle 中可能对应nat、int、real。类型不对后续所有证明都会变得异常困难。建议在理论文件开头用fixes明确声明所有变量类型。8.2 定理拆分不要指望一次证明大定理AI 生成证明时最容易犯的错误是试图一步到位。正确的做法是像写代码一样重构证明先写出若干中间引理再逐步组合成主定理。每个引理都是一个可以单独验证的单元sledgehammer也会更容易找到可用证据。8.3 善用自动化工具Isabelle 的try、sledgehammer、nitpick是日常三件套。当你不知道如何证明时先运行try它会自动尝试多种策略如果命题可能是错的用nitpick找反例如果整体目标太大用sledgehammer搜索外部证明器。lemma example: fixes n :: nat shows n * (n 1) (n 1) * n try nitpick sledgehammer by simptry和sledgehammer会输出可用的证明建议你可以把建议固化到代码里避免每次运行都重复搜索。8.4 把isabelle build接入 CI如果团队已经在做 AI 编程、AI Agent 开发建议把形式化证明也纳入持续集成。每次生成新的理论文件就触发一次isabelle build并记录成功或失败日志。这样既能追踪模型能力的回归也能在大量生成结果中筛选出真正可验证的证明。# 在 CI 脚本中调用 isabelle build -D ./proofs8.5 安全边界与授权提醒使用 AI Agent 自动生成证明和代码时要尽量在隔离环境中执行命令尤其是当 Agent 具备执行能力时。不要让模型在未授权的情况下执行任意系统命令也不要让它的输出直接覆盖生产环境中的理论库。所有批量验证都应该在测试环境里完成并保留日志用于追踪。8.6 团队协作把证明脚本当作代码评审形式化证明脚本和普通代码没有区别需要版本管理、代码评审和命名规范。给每个理论文件写清楚注释这道题来自哪里、转写时做了哪些假设、为什么选择这种证明策略。这样团队里的其他人才能维护这份“AI 生成的证明资产”。9. 总结与后续学习方向Varto 在 Isabelle 中完成 PutnamBench 的完整证明这项成果最值得关注的不是某个模型的单项得分而是它验证了一套新的 AI 数学能力评估方式让模型输出可被机器检查的证明脚本而不是一句“我认为答案是对的”。从工程实践角度看这套“模型生成证明 证明器反馈 Agent 迭代修复”的流程和 AI 编程里的“模型生成代码 编译器反馈 Agent 修复”几乎同构。区别在于证明器比编译器更严格它要求的是逻辑等价而不只是语法正确。所以 Varto 类项目对 AI Agent 的开发方法有很强的参考意义只要存在一个可执行、可反馈的验证环境AI Agent 输出质量就能被持续校准。如果你接下来想深入这个方向建议按顺序做三件事安装 Isabelle跑通isabelle build验证一个小型理论文件从 PutnamBench 官网或论文中挑一两道简单题目尝试手写 Isar 证明用一个本地或云端的大模型配合自动化脚本体验“生成证明 - 失败 - 修复 - 通过”的完整循环。形式化数学验证不是 AI 数学能力的终点但它提供了一个稀缺的东西可复现、可审计、可验证的结论。下次再看到“AI 数学能力很强”的新闻时你可以问一个更具体的问题它的证明脚本在哪里通过哪个证明器的检查是不是所有题目都验证过了这三个问题比任何宣传语都有说服力。