AI证明每句都对却整体跑题？结论对齐与证明助手如何拦截语义漂移

OpenAI 的模型被曝出试图攻破一个数学猜想后数学家大约只用了 24 小时就完成驳回。驳回理由不是某一步推导写错了而是更微妙的问题AI 生成的证明链里每一句话单独看都能证明但整条链走到最后时结论已经和原猜想无关。这类失败在 AI 数学推理中很有代表性它把一个核心弱点暴露得很清楚——局部连贯全局漂移。这篇文章围绕这个案例展开拆解为什么逐句验证仍然会漏掉目标漂移并给出一个可以落地的验证流程如何做结论对齐检查、如何用证明助手拦截跑题定理、如何快速驳回一份看似正确的 AI 证明。无论你是在做 AI Agent 应用开发还是想用大模型辅助科研、编程和论文审稿这套思路都适用。1. 先拆解案例为什么“每句都对”仍会被驳回1.1 现象还原目标、输出和驳回理由假设原猜想是命题 P。AI 给出了一串推理先证明 A1再由 A1 证明 A2一直推到最后得到 Q。数学家拿到输出后做了两件事逐句检查 A1、A2 等中间命题是否成立。检查最后得到的 Q 是否就是原猜想 P。第二件事失败了。AI 证明的 Q 是一个真实成立、并且每一步都能给出依据的命题但它不是 P。它可能只是 P 的一个特例、一个弱化版、一个换了条件的相邻命题甚至是在证明过程中悄悄引入了原猜想没有的假设。无论哪种情况它都不能作为“原猜想被证明”的证据。数学家没有先去逐行钻研整份证明而是先看结论、看假设、看关键分支很快就定位到了漂移点于是整份材料被驳回。整个过程只有 24 小时但效率来自一个清晰的判断目标不对齐后面全部没有意义。1.2 形式有效性与目标相关性是两个维度“AI 证对了每句话”描述的是形式有效性每个推理步骤在逻辑上成立使用的已知定理和推导规则没有错。但证明还需要另一个属性目标相关性最终结论必须和待证猜想完全一致。维度检查内容失败表现自动化程度形式有效性每一步推理是否合法、是否有依据出现错误推导、错误引用定理可以部分用规则和模型检查目标相关性最终结论是否等于原猜想结论被替换、弱化、改变量词或引入新假设目前主要靠人工或语义比对形式有效性和目标相关性是独立的。AI 这次的结果在第一个维度上没问题在第二个维度上失败。这也解释了为什么“每句话都是对的”不能推出“证明是对的”。1.3 为什么现有评测很难发现这类错误很多人在验证 AI 数学输出时采用的做法是让另一个模型逐句判断“这句话对不对”。这种方式只能覆盖形式有效性无法覆盖目标相关性。原因在于单句正确性是一个局部判断只看这一句话和它的上下文。目标相关性是一个全局判断必须把整条证明链的终点和原始猜想放在一起做语义对齐。链越长局部连贯的“惯性”越强漂移越隐蔽。每一句都顺着上一句往下走读者在阅读过程中会逐渐被带离原题但很难在某一处找到明显的逻辑断裂。自然语言没有内置类型检查。一份自然语言的证明即使跑题读起来也可能很流畅只有当你把它放进证明助手或者强制比对结论与目标时问题才会暴露。2. 从 LLM 生成机制看“语义漂移”为什么必然存在2.1 逐 Token 预测擅长局部连贯大语言模型的核心生成机制是逐 Token 预测给定前面的文本预测下一个最可能的 Token。推理过程中模型并没有一个独立的“证明搜索器”在全局范围内寻找从公理到结论的路径。它只是在一个巨大的概率空间里生成一段看起来越往后越合理的文本。这种机制决定了两个特性局部连贯性很强。每个句子都会尽量接住前面句子的语义。全局规划能力弱。模型不会在生成 20 步之后回头检查这 20 步是否真的通向了原猜想。所以当你要求模型“证明某个猜想”时它更擅长的是生成一段符合“证明”这个文本类型的内容而不是精确地服务于那个目标陈述。这是结构性问题不是简单的提示词问题。2.2 漂移的几条典型路径语义漂移不是随机发生的它有几种可预测的路径。在审查 AI 证明时应该优先检查这几类。漂移类型表现危害偷换定义把“连续”换成“一致连续”把“收敛”换成“有界”表面上很像实际命题已变改变量词把“对所有 n 成立”换成“对某个 n 成立”结论显著变弱削弱结论原猜想要求证明“存在性且唯一性”AI 只证明“存在性”目标没有被完整证明引入新假设证明过程中默认了原猜想没有给出的附加条件证明只对特殊情形有效证明完引理后没有回到主定理核心工作量在引理上最后一句没有完成逻辑闭环证明主链缺失上述每一条在单独审视时可能都不算“错误陈述”但它们组合起来就会形成“每句都对、整体无关”的结果。2.3 漂移与幻觉的关系“幻觉”通常指模型生成了与事实不符的内容比如编造参考文献、虚构定理名称。而漂移生成的句子可能是真的只是与目标无关。这两者需要区别对待问题类型单句是否成立与目标是否相关检测难度幻觉否不一定较容易找到一句假话即可语义漂移是否较难逐句检查会放行如果只用“每一步是否有根据”这个标准审查 AI 证明漂移几乎不会被发现。正因为如此它比直接的幻觉更危险。3. 建立“结论对齐”优先的验证流程3.1 在要求 AI 证明前先把猜想形式化自然语言太容易产生歧义。最好的做法是在调用模型之前先把目标猜想写成形式化命题。这个动作有三个作用迫使你自己把猜想的所有条件、量词和结论说清楚。给后续验证提供一份“金标准”陈述。让模型在生成时有一个明确的、不可随意改写的目标。下面用 Lean 4 写一个自然数奇偶性的小例子作为后面的讨论基础。import Mathlib -- 目标命题如果 n 是奇数那么 n^2 也是奇数 theorem odd_square {n : Nat} (h : Odd n) : Odd (n ^ 2) : by rcases h with ⟨k, hk⟩ rw [hk] use 2 * k ^ 2 2 * k ring这段代码的关键点Odd n在 Lean 中被定义成∃ k, n 2 * k 1所以rcases h with ⟨k, hk⟩会拿到一个具体的k和等式hk。rw [hk]把n替换成2 * k 1。use 2 * k ^ 2 2 * k给出一个具体的构造使(2 * k 1)^2 2 * m 1成立。ring负责完成多项式展开。这个例子很小但它演示了“目标先行”的流程先定义好命题再写证明再让机器检查。3.2 用结论对照提示词约束生成在调用大模型时不要只写一句“请证明这个猜想”。应该在提示词中强制要求模型输出结论对照让目标相关性变成一个显式检查点。任务证明下面的猜想。 猜想目标陈述 ∀ n ∈ ℕ若 n 为奇数则 n^2 为奇数。 要求 1. 最终必须给出与目标陈述完全一致的定理。 2. 每一步标注使用的是哪条已知定理。 3. 如果证明过程中得到的是与目标不同的中间结论必须明确说明它和目标的逻辑关系。 4. 最后单独输出“结论对照” - 目标陈述... - 你的最终结论... - 是否等价...这个提示词的价值在于它把“结论对齐”从一个隐含要求变成了显式输出。即使模型最后仍然漂移你也能在“结论对照”里快速发现不一致。3.3 用脚本做结论对齐检查拿到输出后不要直接读全部内容先跑一个结论对齐脚本。下面是一个示意实现实际项目需要根据你的文本类型调整分词和阈值。import re def char_ngrams(text: str, n: int 3): text re.sub(r\s, , text) return {text[i : i n] for i in range(len(text) - n 1)} def conclusion_similarity(target: str, final_claim: str): t_grams char_ngrams(target) c_grams char_ngrams(final_claim) if not t_grams or not c_grams: return 0.0 inter len(t_grams c_grams) return inter / len(t_grams | c_grams) target ∀ n ∈ ℕ若 n 为奇数则 n^2 为奇数 final_claim ∀ n ∈ ℕn^2 ≥ 0 print(conclusion_similarity(target, final_claim))在实际工程中字符 n-gram 只是第一步还可以叠加语义向量相似度、LaTeX 符号归一化、量词结构比对。但最重要的不是算法多复杂而是流程中必须有这个检查环节。没有这个环节后面所有功夫都可能白费。3.4 对中间步骤做依赖链审查结论对齐之后再做依赖链审查。思路是从最终结论往回走逐层寻找“这一步依赖哪些假设”。要回答的问题包括最终结论依赖了原猜想给出的条件吗是否用了原猜想没有给的额外假设是否存在“孤立结论”即某个关键结论在前面从来没有人证明过证明过程中是否偷偷改变了讨论对象比如从自然数换成了整数从函数换成了序列依赖链审查可以手工画图也可以用脚本抽取每句话中的“因为...所以...”结构。生产环境中关键是保证每个关键节点都有可追溯的上游依据。4. 用证明助手堵住“目标漂移”这个口子4.1 证明助手的核心机制目标类型检查Lean、Coq、Isabelle 这类证明助手处理证明的方式和自然语言不同。在证明助手里定理陈述本身就参与了类型检查。在 Lean 中theorem odd_square : Odd (n ^ 2)定义了一个类型。一段证明代码只有落在恰好匹配这个类型的项上才会被接受。如果你写出来的证明实际证明了另一个命题编译阶段就会失败。这正好堵住了“结论已跟原猜想无关”这类漂移目标不一致在形式化系统里不是一个风格问题而是一个类型错误。4.2 最小 Lean 4 示例正确证明与跑题证明下面这两段代码一段是正确证明一段是“每句都对但跑题”的证明。import Mathlib -- AI 声称的最终结论n^2 是非负数 -- 这句话本身完全正确也可以编译通过 theorem square_nonneg {n : Nat} : 0 ≤ n ^ 2 : by exact Nat.zero_le (n ^ 2)如果把这个定理当作odd_square的证据Lean 会直接报错因为0 ≤ n ^ 2和Odd (n ^ 2)不是同一个命题。类型检查把“证明错了对象”这个问题机械地暴露出来。这也说明了形式化验证真正的价值它不是帮你解数学题而是强迫你回答“你证明的到底是什么”。只要陈述不一致编译就过不去。4.3 学习环境与生产环境的实践差异在学习和研究中可以用自然语言加人工抽查的方式快速验证。但一旦要把 AI 证明用于正式论文、代码库或评审流程就需要更强约束。维度学习环境生产环境目标陈述自然语言描述必须先形式化成可编译的定理验证手段人工逐条审查证明助手 结论对齐脚本 人工复核审计记录不一定保留保存模型版本、提示词、输出、验证日志失败容忍度允许临时纠错需要灰度、回滚和可追溯生产环境还需要注意依赖版本固定。Lean、Mathlib 等版本一旦变化同一个定理的编译结果可能不同。自动化流水线要把这些版本信息写进构建记录。5. 人工 24 小时驳回流程与排查路径5.1 一个可复用的驳回流程从数学家的处理方式看高效率驳回不依赖逐行精读而是按优先级推进。时间窗口操作输出0 - 1 小时只读最终结论与目标陈述逐项比对“结论对齐”或“结论不对齐”1 - 6 小时对最终结论和关键中间步做反例搜索反例列表6 - 12 小时画依赖图找新引入的假设和孤立结论依赖图与疑点清单12 - 24 小时对疑点步骤做形式化验证写驳回意见驳回报告驳回报告可以用结构化记录保存方便后续复现和对比。{ conjecture_id: C-2024-001, target_statement: ∀ n, Odd n - Odd (n^2), generated_conclusion: ∀ n, 0 ≤ n^2, step_check: passed, conclusion_alignment: failed, verdict: rejected, reviewer: human-mathematician, hours_to_reject: 24 }这份 JSON 记录说明了一个重要事实step_check是 passedconclusion_alignment是 failed而最终 verdict 是 rejected。这正好对应文章标题里“AI 证对了每句话”却仍被驳回的情况。5.2 从现象倒推原因审查 AI 证明时遇到不同现象应该往不同方向排查。问题现象常见原因检查方式处理建议结论看起来很像原题但总觉得差点什么量词或条件被微调逐词比对目标陈述标注不一致项要求模型重写证明里出现原猜想没有的符号引入了额外假设检查依赖图确认该假设是否为已知定理中间引理全部正确但最后一步很弱主定理没有真正被证明检查最后一句与目标是否同构对最后一步做形式化验证声称证明了“更强的结论”强弱关系被误判验证强弱关系的方向构造反例或形式化比较用自然语言能读懂但无法形式化关键步骤有隐含跳跃尝试在 Lean 中编译定位跳步位置补全证明5.3 需要警惕的危险信号以下几类信号出现时应当立即提高怀疑级别最终结论和原猜想的说法不完全一致哪怕只差一个条件。量词位置含糊比如“总存在”和“对任意”混用。证明中突然出现原猜想没有的新定义、新常数。关键引理的证明被一句话带过而这个引理恰恰是全局的核心。证明的篇幅主要花在引理上最后回到主定理时只有一句“因此原命题成立”。这些信号不一定说明证明错误但它们是最容易出现漂移的位置。审查者应该优先在这些位置投入精力。6. 常见误判、检查清单与最佳实践6.1 四个常见误判第一把“编译通过”当作“证明成立”。编译通过只能说明你写的证明确实证明了你在定理声明里写出的命题。如果定理声明本身已经被悄悄改成另一个命题编译同样会通过。所以必须先确认被编译的声明就是原猜想。第二把“每一步都验证过”当作“整体成立”。这是本次案例的核心教训。单句正确无法保证语义没有漂移尤其当链很长、上下文惯性很强的时候。验证必须有全局对齐这一步。第三把“术语密度高”当作“可信”。大模型非常擅长生成高密度术语。大量专业名词堆叠不等于逻辑完整反而可能掩盖跳跃。第四把“模型说它是证明”当作“它具有证明意图”。模型的目标是生成像证明的文本不是证明出某一个确定命题。两者之间的差异是所有 AI 证明审查流程必须首先承认的现实。6.2 可复用的 AI 证明审查清单实际项目可以使用下面这份清单作为最低审查标准。是否已经把原猜想形式化成可编译的命题。是否提取并核对了 AI 输出的最终结论。是否确认最终结论与原猜想在量词、条件和结论上完全一致。是否检查过证明中引入的所有假设确认没有新增隐藏条件。是否对最终结论和关键引理做过反例搜索。是否对核心步骤做过证明助手编译。是否记录了模型版本、提示词、输出和验证日志。这份清单不需要全部自动化但要落到固定流程里。缺少任何一项都有可能复现这次“每句都对但整体无关”的失败。6.3 什么时候可以信任 AI 证明一个比较稳妥的判断标准是当且仅当目标陈述被严格形式化并且证明在证明助手中由机器检查通过同时人类确认了“被证明的命题就是原猜想”时才可以把它当作正式证明。其他情况下AI 生成的证明更适合被当作“证明草稿”或“思路建议”。它可以帮你找引理、补反例、提供构造思路但不应该直接进入论文或代码库。6.4 下一步实践建议如果想把这套思路落到自己的项目里建议按这个路径推进。第一步学习 Lean 或 Coq 的基本操作先形式化数学课里的定理。不需要多复杂能表达命题和完成简单证明即可。第二步搭建一个结论对齐检查脚本。先跑通“目标陈述 vs 最终结论”的比对再逐步加入依赖链分析。第三步接入大模型 API 时把提示词设计成“必须输出结论对照”的模式并把每次输出、模型版本、验证结果都记录下来。第四步把反例搜索做成自动化。对有限结构可以直接枚举对连续结构可以使用随机采样或数值验证。只要找到反例无论中间推导多漂亮都要立即驳回。AI 数学推理的真正价值不在于替代人类思考而在于把证明草稿的生产速度提高几个量级。代价是审查环节必须比以前更严格。目标对齐、形式化验证、反例搜索、人工复核这四件事合在一起才是 AI 时代处理数学证明的正确姿势。