数学家24小时驳回OpenAI攻破的猜想这个新闻在开发者圈子里传得很快。对大多数不搞数学研究的人来说第一反应可能是“AI又翻车了”但如果只看这一层就错过了这件事里最有技术价值的部分。真正值得讨论的不是“AI有没有证明出猜想”而是它给出了一份逐句都正确、但整篇与目标猜想无关的证明。这里面的问题已经不只是数学问题而是所有大模型生成式任务都会遇到的结构性矛盾模型擅长生成局部正确的文本序列却未必能保证全局内容服务于同一个目标。这篇文章我会从数学证明和形式化验证的角度拆解这件事为什么会出现“每句话都对但证明无关”的情况当前的AI推理系统在数学任务上的能力边界在哪里以及作为开发者我们应该用什么工程手段避免这类“看似正确、实际无用”的结果。1. 这件事的本质不是模型不够聪明是“意图”没有被建模“AI证对了每句话但已跟原猜想无关”这句话听起来像是一个段子但在数学和计算机科学的交叉点上它描述的其实是一个非常严肃的问题。数学证明有两层属性局部正确性证明中的每个推理步骤必须遵循逻辑规则前提到结论是合法推导。全局意图性整条推理链必须最终指向目标命题证明的是你要证明的那个结论。当前大模型在“局部正确性”上表现已经相当不错。经过大规模语料训练之后模型对常见的数学推导模式、符号变换、命题形式非常熟悉它生成单步推理时往往能写出形式上无懈可击的句子。真正出问题的是第二层——“全局意图性”。模型生成证明时并不存在一个显式的“我要证明目标P”的约束贯穿整个生成过程。它只是在每一步选择一个很可能的下一句话最终这些句子串在一起形成一份看似结构完整的证明文本。这就像一个开发团队里每个人都在自己的函数里写出了语法完全正确的代码但没有人定义整个模块对外提供的接口和功能最后把代码拼在一起编译能过程序能跑但用户要的功能一个都没有。问题不在于模型不够聪明而在于“证明的意图”这件事当前的模型训练范式并没有很好地建模。训练时模型学习的是“给定上文下一个token是什么”而不是“给定目标命题生成一串能让目标成立的推理链”。后者需要的是一个目标导向的搜索与验证过程而不是一个单向的文本生成过程。理解了这一层就能理解为什么数学家能在24小时内驳回这份证明。因为审阅者看一份证明首先看的不是每一句话是否合法而是整个证明是否在为同一个目标服务。如果发现证明的推进方向和目标命题之间没有因果联系那不管单句话再正确这份证明也是无效的。2. 从“解题”到“证明”AI数学推理的能力边界在快速移动过去几年AI在数学任务上的表现有一个比较清晰的演进路径。最早被攻克的是“计算”类任务比如解方程、求导、计算定积分。这类任务有确定的算法模型只要学会模式匹配和符号操作就能得到不错的结果。然后是“解题”类任务典型代表是奥数竞赛题。这类题目虽然需要推理但通常有确定的答案和标准的解题路径而且训练语料充足。模型通过大规模练习可以学会识别题型、套用思路。OpenAI的o系列模型在数学竞赛题上已经取得了非常亮眼的成绩很多国际数学奥林匹克难度的题目都能解决。再往后是“证明”类任务尤其是开放性的数学猜想。这跟解题有本质区别解题的目标是确定的答案是否存在、长什么样都有明确判定标准。证明的目标是开放式的你需要自己构造一条从公理到目标的推理链中间可能涉及大量创造性的构造、定义和中间引理。OpenAI这次尝试的猜想类证明正好卡在这个能力边界上。模型能生成看起来合理的数学文本甚至在每一步推理上都符合数学规范但它不具备对“目标猜想的价值和意义”的深层理解。它不知道哪些中间结论与最终目标相关哪些只是在“形式上正确但永远不会通向终点”的死胡同。从另一个角度看这个现象也是自然语言模型的通病它们在“似真性”上非常强在“真理性”上仍然需要外部工具兜底。生成一段数学证明文本让一个数学专业的学生读起来觉得很顺畅这已经不是难事。但要确保这段证明在逻辑上严格成立、在意图上指向正确这不是语言模型单独能完成的事情。3. 为什么会出现“局部正确整体无关”四个技术原因要把这个问题讲清楚不能只停留在“AI笨”的层面上。从技术角度看至少有四个原因导致了这种“局部正确、整体无关”的失败模式。3.1 训练目标与证明目标不一致大语言模型的训练目标本质上是最大化下一个token的预测概率。给定一段“证明的前半部分”模型要预测“后半部分最可能是什么”。在数学语料里“最可能的下一个句子”往往是那个在统计上最顺滑、最符合人类写作习惯的句子而不一定是逻辑上最正确的句子。更关键的是训练目标里没有“目标命题”这个显式输入。模型被要求生成一段证明时它看到的只是“证明目标P”以及之前生成的句子。它并没有一个内部的“我正在证明P”的状态来约束每一步的生成方向。3.2 长程推理的上下文规划能力不足数学证明的难点在于它需要非常长的推理链。一个中等难度的定理证明可能需要几十步甚至上百步的推理。在这个过程中每一步的选择都会影响后续的可行性。当前的Transformer架构虽然在长上下文处理上进步很快但长程依赖仍然是一个短板。模型在生成到第50步时往往已经“忘记”了最初的目标结构或者被自己前面生成的中间结果带偏进入一个虽然数学上合法、但与目标无关的推理方向。这就像在迷宫里走迷宫的人每一条路都走得很稳但走到后面已经不知道出口在哪里了。3.3 缺乏“试错”与“回溯”机制人类数学家做证明不是线性的。他们会尝试一种思路发现走不通退回来尝试另一种。这个“试错回溯”的过程是数学研究的常态。但当前的大模型生成是一次性的前向传播每一步根据当前上下文生成下一个token没有迭代的试错和改进机制。虽然有一些方法比如self-refine、MCTS树搜索可以让模型在采样后自我反思和筛选但这些方法还不是模型本身的能力而是外部包装的推理框架。在缺乏有效搜索的情况下模型只能沿着一条错误的路径一直走下去。3.4 自然语言验证器的验证能力有限“这句话对不对”和“这句话对证明目标有没有用”是两个不同的问题。如果让一个自然语言模型来验证AI生成的证明它能判断的大多是前者句子是否符合语法、推理是否合理、符号使用是否正确。但它很难判断后者这条推理链是否真的在朝着目标推进。这也是为什么数学界对“AI证明”的通用标准越来越偏向形式化验证——用Lean这样的工具让机器严格检查每一个推理步骤是否符合规则并且确保最终结论与目标命题一致。4. 形式化验证让“每一步正确”和“目标一致”同时成立非形式化的自然语言证明存在一个天生的缺陷它的正确性依赖于读者的判断。读者需要自己脑补很多“显然”的步骤也需要自己判断证明是否真的证明了目标。这给了“看似正确、实则无关”的证明留下了生存空间。形式化验证的解决思路很直接把“证明”从自然语言文本变成机器可检查的推理序列让计算机来验证每一步是否符合逻辑规则以及最终结论是否精确等于目标命题。目前主流的证明助手包括 Lean、Coq、Isabelle 等。其中 Lean 因为数学社区活跃、Mathlib 数学库庞大已经成为形式化数学事实上的主流选择。一个简单的 Lean 证明示例可以看到它如何把“证明”和“目标”绑定在一起import Mathlib.Data.Real.Basic -- 命题如果 x 是有理数那么 2 * x 是有理数 example (x : ℚ) : 2 * x x x : by ring在这个例子里example (x : ℚ) : 2 * x x x明确声明了目标命题by ring是证明策略ring会自动完成有理数环上的等式证明。Lean 验证器会检查这个证明是否真的推导出了目标。如果证明步骤与目标无关或者推理不合法Lean 会直接报错。形式化验证之所以能避免“每句话都对但证明无关”的问题是因为它把“证明”从一篇文章变成了一棵精确的推理树。树上的每一个节点都由验证器检查树的根节点就是目标命题。任何一步不合法整棵树都会被拒绝任何一步与目标无关树就没有办法闭合到根节点。5. 一个可复现的最小示例模拟“局部正确整体无关”的证明为了理解“每句话都对但证明无效”到底是怎么发生的我们可以用代码模拟一个简化的版本。假设我们有一个AI生成证明的模块它能输出合法的数学陈述但不知道这些陈述与目标之间是否有因果关系。下面的Python代码演示了这个过程from typing import List def generate_legal_math_statements() - List[str]: 模拟AI生成的中间证明步骤。 这些步骤在数学上都是合法陈述但并未构成对目标的证明。 steps [ ∀ x, x 0 x, # 加法单位元真命题 ∀ x, x * 1 x, # 乘法单位元真命题 ∀ x, x (-x) 0, # 加法逆元真命题 ∃ n, prime n, # 存在素数真命题 如果 a | b 且 b | c则 a | c # 整除传递性真命题 ] return steps target ∃ x, x * x 2 # 目标命题存在 x 使得 x 的平方等于 2 def proof_is_valid_for_target(steps: List[str], target: str) - bool: 简化版验证器。 真实的形式化验证器会检查每一步推理是否合法 以及最终结论是否等价于目标命题。 这里只模拟最终结论是否等于目标的检查。 if not steps: return False final_conclusion steps[-1] return final_conclusion target steps generate_legal_math_statements() print(生成的证明步骤) for i, step in enumerate(steps, 1): print(f Step {i}: {step}) print(f证明目标{target}) print(f验证结果{通过 if proof_is_valid_for_target(steps, target) else 不通过})运行这段代码输出是生成的证明步骤 Step 1: ∀ x, x 0 x Step 2: ∀ x, x * 1 x Step 3: ∀ x, x (-x) 0 Step 4: ∃ n, prime n Step 5: 如果 a | b 且 b | c则 a | c 证明目标∃ x, x * x 2 验证结果不通过这个示例里AI生成的每一个陈述都是数学上正确的命题。加法单位元是对的乘法单位元是对的加法逆元是对的存在素数和整除传递性也是对的。但整个证明序列与“存在 x 使得 x 的平方等于 2”这个目标毫不相干。这就是OpenAI那份证明被驳回的核心原因。AI不是在“证明过程”上犯错而是根本没在证明目标命题。它只是生成了一串“像是证明的东西”里面充满了正确的数学事实但它们组合在一起并不构成对目标的证明。如果把这个逻辑验证进一步简化成代码逻辑可以这样理解验证器的设计思路验证器不仅要检查证明的最终结论是否等于目标还要检查每一步是否由前面的步骤合法推出。这个“合成性检查”是形式化验证的核心价值。import re def validate_formal_proof(steps: List[str], target: str) - bool: 更接近真实形式化验证器的简化逻辑 1. 每一步必须是一个合法的数学陈述这里用非空和括号闭合做简化判断 2. 最终结论必须与目标逻辑等价 3. 中间步骤之间构成合法的推导关系这里简化为文本连续性检查 for step in steps: if not step or not _is_legal_statement(step): print(f非法推理步骤{step}) return False if steps[-1] ! target: print(最终结论与目标不一致) return False return True def _is_legal_statement(statement: str) - bool: 极简的合法性检查非空、括号闭合、包含逻辑符号。 真实的Lean验证器会检查每一步是否符合自然演绎或演算规则。 if not statement.strip(): return False if statement.count(() ! statement.count()): return False if not any(sym in statement for sym in [∀, ∃, →, ∧, ∨, ]): return False return True这段演示代码告诉我们一个工程关键点验证器的价值不只是检查结果的“真”而是检查整个推理过程中的“链条完整性”。如果没有这种链式检查模型生成的文本再流畅也不能称为证明。6. 工程化审查AI数学证明的四个层次从“OpenAI被驳回”这个案例里开发者可以提炼出一套对AI生成数学内容进行工程化审查的方法。这套方法本质上是多层防线核心是不要让AI输出的文本直接通过“正确性”检查从不同维度建立验证机制。6.1 层次一局部推理合法性校验对AI生成的每个推理步骤单独检查它是否符合逻辑规则。这可以借助一些符号计算库或逻辑引擎完成。比如在Python里用SymPy检查符号变换是否正确或者用z3求解器验证某个约束是否可满足。from z3 import Int, Solver, Not, unsat # 假设AI声称如果 x 3 且 x 5则 x 4 # 用z3检查这个结论是否一定成立注意整数域 x Int(x) s Solver() s.add(x 3, x 5, x ! 4) # 构造一个反例场景 if s.check() unsat: print(在整数域上x 3 且 x 5 时 x 必须等于 4推理合法) else: print(f存在反例推理不成立模型给出的x值为{s.model()})这种校验可以拦截掉大量“看似合理、实际错误”的单步推理。6.2 层次二全局目标相关性检查单步正确不等于整体有用。需要有一个机制把证明的最终结论与目标命题进行一致性比对。最简单的方式是使用逻辑等价性检查。对于复杂命题可以把目标命题和AI生成证明的结论分别转成某种规范形式再做比较。如果做不到自动化的逻辑等价可以退而求其次做关键词和结构的对齐检查确保证明过程中没有偏离目标主题太远。6.3 层次三形式化验证器强制检查这是最严格的一层。把AI生成的证明翻译成Lean或Coq的代码用形式化验证器编译。如果编译通过说明证明在形式逻辑上是严格成立的并且确实证明了目标命题。这不是“辅助判断”而是一锤定音的标准。6.4 层次四人类专家审阅即使通过了形式化验证仍然需要人类专家审阅。原因在于形式化验证保证的是“在给定的公理系统和定义下证明成立”。但AI可能在定义上做了“手脚”比如通过自定义一个非标准定义让目标命题变得trivially true这偏离了数学家的原始意图。数学家驳回AI证明很多时候就是发现AI“重新定义了问题”或“证明了另一个更简单的命题”。7. 常见误区与分析框架关于AI数学证明有几个常见的误解需要澄清说法实际情况技术解释AI将很快取代数学家可能性很低当前生成式模型的核心能力是“模式匹配”和“文本生成”不是“目标驱动的创造性探索”AI生成的证明是假的不够准确它是局部正确、全局无效不是无中生有地编造人类拿AI证明没办法正好相反数学家24小时就能驳回因为审阅者通过“目标相关性”这一关就能淘汰大多数结果形式化验证可以解决一切不完整形式化验证能保证逻辑正确但不能保证数学家的原始意图被准确翻译成形式化命题作为开发者最值得记下的判断是AI生成内容的价值取决于是否有一个外部验证器来审查它的输出。数学证明的验证器是Lean代码生成的验证器是编译器加测试用例SQL生成的验证器是数据库执行计划文案生成的验证器是人工审核流程。没有验证器的AI应用输出的质量只能靠运气。8. 从“AI证明数学”到“AI参与软件开发”OpenAI在数学证明上踩的这个坑在AI辅助软件开发中有几乎一模一样的版本。很多开发者都遇到过这样的场景让AI生成一个功能模块代码看起来结构清晰、函数命名规范、语法完全正确但运行之后发现它实现的功能和需求文档完全对不上。它可能实现了一个类似但不同的功能或者它写的代码能通过编译却不满足任何一条验收标准。这跟“AI证对了每句话但已跟原猜想无关”是同一个失败模式局部层面每个函数语法正确每个API调用合法。全局层面整个程序没有解决用户最初提出的问题。在软件开发中对应的工程解法是用测试用例锚定意图。在让AI生成代码之前先写清楚验收测试。AI生成代码之后跑测试验证功能是否真的满足需求。测试如果全过说明AI不仅“写对了代码”而且“写对了功能”。这相当于用外部验证器把AI的生成过程约束到了正确的目标上。# 需求编写一个函数返回斐波那契数列的第 n 项 # AI可能生成的代码语法正确但功能错误 def fib(n): return n * 2 # 验收测试锚定真实的意图 def test_fib(): assert fib(1) 1 assert fib(2) 1 assert fib(3) 2 assert fib(5) 5 assert fib(10) 55如果AI生成了fib(n) n * 2测试会在第一项就失败。这比人工审查代码更快地暴露了“局部正确、全局无关”的问题。类似地在需求工程中可以用ACAcceptance Criteria来约束AI生成的需求文档。在API设计中可以用契约测试来验证AI生成的接口是否符合规范。在数据库开发中可以用查询结果集来验证AI生成的SQL是否真正回答了业务问题。9. 总结“数学家24小时驳回OpenAI攻破的猜想”这个新闻真正的价值在于它帮助技术人建立了一个重要的判断框架不要被AI生成的表面流畅性迷惑。局部正确只是起点全局意图一致才是终点。对于做大模型应用的开发者这个案例带来的启示很直接如果AI生成的代码能编译先不要高兴跑一遍测试再说。如果AI生成的SQL能执行先确认结果集真的回答了业务问题。如果AI生成的证明看起来很有道理先检查它证明的是不是原来的猜想。形式化验证在数学领域扮演的角色就是单元测试、集成测试、契约测试在软件开发中扮演的角色。它们是“意图的锚”是人类给AI生成结果建立的外部约束。没有这些约束AI的生成能力越强产生的“看似正确、实则有偏差”的内容就越多。下一步值得深入的方向对数学和逻辑推理感兴趣的读者可以花时间了解Lean和Mathlib它代表了“用机器验证数学”的前沿。对AI工程实践感兴趣的读者更值得研究的是“验证器优先”的开发范式——任何AI生成的内容都应该配套一个可靠的验证机制再谈生产效率的提升。