从希尔伯特纲领到生成式 AI：证明、字符串与计算的边界

今天使用生成式人工智能（AI）时，我们常看到回答在屏幕上一点点展开，仿佛机器正在边想边写。（当然，还有其他机制共同达成了这个效果，不全是计算机生成造成的。）

把这个现象放回数学基础研究的历史，会发现一条值得追问的联系：形式证明可以写成有限的符号串，程序也能用有限的符号串描述，而语言模型生成的文本同样是符号序列。哥德尔、图灵与今天的数学人工智能，围绕这些符号提出了不同的问题：证明怎样被检查，系统怎样谈论自己的证明，机器怎样搜索答案，以及哪些目标根本无法靠无限搜索达成。

这条联系并不意味着不完备定理直接解释了语言模型的每一次失败。它提供的是一个更精确的视角：当我们要求机器在指定规则下寻找证明时，必须区分生成能力、验证能力和目标本身的可证明性。

图：从形式符号到生成模型，证明的表达与计算的边界贯穿其中。

一、希尔伯特的梦想：让数学证明能够机械检查

20 世纪初，数学基础研究面对着一个重要问题：我们凭什么相信数学推理是可靠的？对于 1 + 1 = 2 这样的计算，人们容易形成直观把握；当研究对象扩展到无限集合和复杂的抽象结构时，直觉本身却不足以承担全部论证责任，集合论悖论更使基础问题无法回避。

希尔伯特纲领希望把数学组织成明确的形式系统，并以他所认可的有限方法证明其一致性。形式化要求符号、公理和推理规则都足够明确，使一份证明中的每一步原则上都能接受机械检查。这比“把证明写得详细一点”更严格，也不只是今天意义上的程序自动验证。[1]

在这样的系统里，一段推导可以表述为：采用公理1和公理7，得到公式A；应用推理规则3得到公式B，再应用推理规则5得到公式C，继续推导，最终得到命题 P。这里的编号只是说明结构，真正的证明必须给出各条公式，并满足指定规则，不能靠写上“应用规则”就跳过论证。

一旦符号和检查规则确定，整份证明就可以表示为有限的符号序列。检查者不必接受“这一步显然成立”这样的口头保证，而能逐项核对它是否符合规则。今天的形式验证正继承了这个核心思想：一个候选证明是否合格，应当有明确的判断依据。

二、哥德尔编号：让数学谈论自己的证明

1931 年，库尔特·哥德尔（Kurt Gödel）发表了不完备性论文。证明中的关键技术之一是把符号、公式和证明进行算术编码，通常称为哥德尔编号。这样，关于形式表达式的某些问题就能够转化为关于自然数的问题。[2]

为了说明原理，我们可以先给几个符号分配编号。下面只是教学示例，并非哥德尔原论文采用的完整编码表：

• “0” → 1
• “1” → 2
• “+” → 3
• “=” → 4
• “(” → 5
• “)” → 6

在这个约定下，公式 0 = 0 对应编号序列（1，4，1）。但给单个符号编号还不等于把整个公式编码成一个自然数，我们还需要一种能够保存顺序并恢复序列的办法。例如用连续素数作底数，把符号编号作为指数，就可将该序列编码为 2¹ × 3⁴ × 5¹ = 810。借助唯一素因数分解，可以从这个数恢复相应的编号序列。

要处理更复杂的公式，如 ∀x（x + 0 = x），还须给量词、变量等其他符号安排编号，并规定完整的编码和解码方法。一整份证明也能进一步编码：先编码每条公式，再编码这些公式的有限序列。重要的并非选择哪几个数字，而是编码必须有效、可恢复，并允许用算术表达有关检查的关系。

原本，证明及其合法性是我们在形式系统外部讨论的对象。经过适当编码，系统内部的算术公式也能够表达“这个自然数编码了一份证明”“这份证明的结论是某个公式”等关系。外部研究并未因此消失，但证明的一部分结构确实进入了算术能够描述的范围，这为哥德尔的自指构造提供了基础。

三、从今天看，证明也是程序可以处理的数据

有了现代计算机，我们可以先把证明理解成一种结构严格的文本。例如，公理1、公理2、规则3、公式A、规则7、公式B和定理P，可以作为一段示意推导中的中文标签；实际的形式证明则必须填入这些标签所代表的公式，以及每一步所依赖的前提。

随后可以编写一个验证程序，接收候选证明，检查其中的符号、公式及推导是否合法，再返回通过或不通过。对公理和规则具有适当有效性的形式系统，这类检查能够机械执行。如果公理只是可枚举的，证明记录还可以包含足以验证其公理来源的证据，使搜索与检查仍能有效组织起来。

这个视角让哥德尔编号更容易理解，却不能抹去编号在定理中的作用。把证明存成计算机文件，与在算术系统内部表达“某数是一份证明的编码”，是两个相关但不同的要求：前者处理数据，后者还要说明系统内部能够表达哪些关于这些数据的关系。

四、能不能把所有候选证明都搜索一遍

现在假设我们有一个命题 P。我们想知道：P 到底是真的还是假的？进入机械证明搜索之前，还要选定形式系统 T，把目标明确为寻找 P 或其否定的形式证明。本文统一用 ¬P 表示 P 的否定；找到哪一方的证明，首先回答的是系统中的可证明性问题。

若证明使用有限字母表，就可以按长度由短到长、同长度按固定顺序枚举所有有限字符串。以字母 a、b、c 为例，枚举可以从 a、b、c、aa、ab、ac、ba、bb、bc 继续下去。对每个候选字符串 s，验证程序分别检查它是不是 P 的证明，或者是不是 ¬P 的证明。

如果 s 证明了 P，程序就报告“P 在 T 中可证”并停止；如果 s 证明了 ¬P，就报告“¬P 在 T 中可证”并停止；否则继续检查下一个候选。只要枚举不会漏掉任何有限候选，而每次检查都能结束，存在的证明最终就一定会被检查到。要进一步把这些报告解释为有关真假的可靠结论，还需要系统对相应解释具有可靠性。

这台朴素的证明搜索器在思想上已经成立，实际效率却可能极差。绝大多数被枚举的字符串甚至不是合法公式，更不用说有效证明。不过在讨论可计算性时，我们首先关心的是它原则上会不会到达目标，然后才是需要付出多少资源。

五、真正的困难：两边都可能没有证明

如果 P 对选定的系统 T 是独立的，就意味着 T ⊬ P 且 T ⊬ ¬P。其中符号 ⊬ 表示“不能在该系统内证明”，两个表达式分别说明 P 和它的否定都没有相应的形式证明。

这时，刚才的搜索程序会检查候选字符串1、候选字符串2、候选字符串3，持续运行下去。它不会找到 P 的证明，也不会找到 ¬P 的证明，因为在指定系统中，这两个目标都不存在。搜索空间能够不断扩大，并不意味着空间里必然有我们想找的对象。

不完备性结论有明确的适用条件。按照哥德尔第一不完备定理及罗瑟的加强形式，一个一致、可有效公理化且足以表达相应初等算术的理论，不可能判定其语言中的全部句子。这里不能省去一致性、有效性和算术表达能力，也不能把结论泛化为“任何规则系统都必然不完备”。[3]

六、没有证明，不等于没有真值

“真”和“可证明”不是同一个概念。可证明性总要相对于某个形式系统及其规则来谈；真假则相对于一种解释或模型来谈。对于算术句子，人们常关心的是它在标准自然数结构中是否成立，而这与某套公理是否能够推出它并不重合。

例如，假定某个算术句子 P 在标准自然数中为真，但它对系统 T 独立，那么 T 中既没有 P 的证明，也没有 ¬P 的证明。此处“不存在证明”始终指 T 中的证明，不是说任何更强理论、任何外部论证都无法处理它。

相应地，一致且不完备的理论可能有在某句子上给出不同解释的模型。它们说明公理没有把这个问题完全固定下来，不意味着在一个已经指定的经典模型里，该句子同时既真又假。把系统、证明和解释分开，才能准确理解搜索器究竟缺少什么。

七、生成式 AI 与字符串有什么联系

典型的自回归语言模型会根据上下文计算下一词元的条件分布，可写成 P（xₙ₊₁｜x₁，x₂，…，xₙ）。这里的 P 表示概率分布，与前文作为命题名称的 P 依语境区分；x₁ 至 xₙ 是已经给定的词元，xₙ₊₁ 是接下来要生成的词元。

词元（token）是模型处理文本的单位，可能对应一个字、一个词、词的一部分，或者标点等内容。模型按某种解码策略选择下一词元，将它纳入上下文，然后继续生成；选择并不总是取概率最高的一项，还可能包含采样等机制。因此“根据前面的文字预测后面的文字”是一个便于理解的概括，而不是全部实现细节。[5]

输出序列可以记成 x₁、x₂、x₃、x₄、…。这解释了回答为何能逐步展开，但屏幕上的逐字效果还受到缓冲、批量返回等因素影响。我们能够据此理解一类模型的基本生成机制，却不能仅凭界面动画断定它的内部计算步骤。

八、推理文本也需要接受检查

让语言模型证明一道数学题时，它可能依次写出“设……”“考虑……”“因此……”和“所以得证”。这些表达构成一段推理文本，也可以抽象地记为步骤序列 s₁、s₂、…、sₙ，但呈现出证明的语言形式，并不保证逻辑上已经成立。

朴素枚举器按固定顺序提出候选，而语言模型依据训练所得的模式和当前上下文生成候选；现代自动定理证明系统也往往使用复杂的搜索策略，并不都靠暴力枚举。它们的共同点在于要组织候选表达，区别在于候选从何而来，以及用什么标准检查。

如果输出进入形式验证器，候选就必须满足精确的语法、类型和推理规则。自然语言中的“显然”“类似可得”不能自动变成合格的形式步骤，缺失的中间论证需要补全。生成能力在这里负责提出值得尝试的方向，验证能力负责决定哪些候选真正符合指定标准。

九、逐步生成为什么可能走偏

当模型说“这个问题的证明如下”时，我们很容易想象它已经拥有一份完整、可靠的答案，只是在依次念出来。实际的生成过程可能综合已学习的知识、上下文中的条件和逐步产生的中间内容；有些答案还会受检索或工具返回影响，不能一概解释为从某个固定答案库里照读。

对典型的自回归生成而言，新输出会成为后续计算的上下文。如果前面误用了一个条件，后面的表达就可能继续建立在错误前提上，于是读起来越来越顺，却离目标越来越远。反过来，额外的计算、回溯或外部检查也可能发现问题并促成修正，因此一次早期错误不等于后续必然失败。

这解释了为什么连贯的推理文本仍然需要校验。表述流畅、局部步骤看似合理和整份证明成立，是不同层面的判断。对于数学任务，关键不只是模型能否把话继续说下去，还在于后续步骤是否仍满足题设、逻辑规则和结论所要求的条件。

十、加入形式验证器：把生成变成可检查的搜索

设想把模型接入一个形式证明环境：模型先提出候选证明，形式验证器随后检查。通过时，系统保存已验证的结果；未通过时，把错误信息返回给生成环节，据此修改候选，再次提交检查。下图中的蓝色序列表示生成与验证，绿色对勾表示通过，黄色回路表示失败后修改候选并重新验证。

图：模型生成候选，验证器检查；通过则结束，未通过则修改候选并重新提交。

此时，任务变成了搜索一个能够通过指定形式规则检查的字符串。验证通过的含义也应说清楚：在验证器及其可信计算基础正确、没有跳过证明义务的前提下，形式化结论从给定前提和公理中成立。若形式化时误写了原题，或者引入了原题没有的假设，程序即使通过检查，也可能没有回答读者真正提出的问题。

这个循环增强了结果的可核查性，却不保证每个目标最终都能成功。生成器可能持续提出无效候选，搜索也可能因预算耗尽而中止；若目标在当前系统中不可证，修改再多次也不会产生该系统内有效的目标证明。

十一、无限尝试与存在证明是两回事

现在可以把证明搜索与不完备性联系起来。设一台数学 AI 不断提出候选 s₁、s₂、s₃、…。若其中某个候选 sₖ 是 P 的有效证明，我们可以简记为“sₖ 是 P 的证明”；若另一个候选 sⱼ 是 ¬P 的证明，也可用同样方式检查。这里说的是一份具体证明，而不是假定每个命题都存在一个可以直接调用的“证明函数”。

对不会漏掉候选的穷举过程，只要证明存在，就能保证最终遇到它；对启发式或概率式的 AI 搜索，证明存在本身还不提供这一保证。它可能反复走向相似的错误方向，或始终未探索某条关键路径，这属于搜索策略的问题。

如果 P 和 ¬P 在 T 中都没有证明，困难就更根本：在这个形式系统里，没有任何候选能通过目标检查。这时，增加图形处理器（GPU）、扩大上下文或延长搜索时间，都不能使不存在的证明凭空出现。机器仍然可以主动停止并报告未解决，只有“找到证明才停止”的特定搜索程序才会一直运行。

十二、不完备性对“万能数学家”的提醒

模型再大一些、推理时间再长一些、计算资源再多一些，会不会就解决全部数学问题？对于许多已有证明但难以发现的问题，改进资源与策略确实可能有效。然而“不容易找到证明”与“在指定系统中没有证明”，不能混为一谈。

哥德尔式限制针对的是满足相应条件的固定形式理论。它没有证明某一道尚未解决的日常数学题必然独立，也没有证明人类拥有超越一切计算系统的直觉。把一次解题失败直接归因于不完备性，和把所有失败都归因于算力不足，同样缺乏依据。

我们可以增加公理、改换理论，在更强的框架中处理原来独立的问题。但为什么接受新公理，以及它带来什么后果，需要新的数学论证与判断；如果新理论仍然一致、有效且足够强，它也不能逃离相应的不完备性限制。

十三、从哥德尔到图灵：搜索程序会不会停止

程序可以由有限字符串描述，于是一个自然的问题出现了：给定任意程序和输入，能否总用某个算法正确判断它最终会不会停机？在现代计算理论的表述中，停机问题的不可判定性说明，不存在这样一个对所有实例都正确并且自身总会结束的通用算法。艾伦·图灵（Alan Turing）1936 年关于可计算性和判定问题的工作奠定了这一理论基础。[4]

现在看那台证明搜索器：它不断生成候选，一旦找到 P 或 ¬P 的证明便停止。于是“它是否会找到证明”就被转换成了一个特定程序的停机问题。这种转换把数学命题与程序行为联系起来，让抽象的证明搜索具有了直接的计算解释。

不过，某个命题对 T 独立，与某类程序行为不存在通用判定算法，并不是可以不加条件地画上等号的两句话。两者通过编码、归约及形式系统对计算的表达发生联系；具体到一台机器，我们有时能够明确证明它停机或不停机，通用算法不存在并不妨碍解决许多具体实例。

十四、麻省理工学院的“哥德巴赫机器”

2016 年，在麻省理工学院（MIT）开展工作的亚当·耶迪迪亚（Adam Yedidia）与斯科特·阿伦森（Scott Aaronson）研究了行为与数学命题相关的具体图灵机。其中一类机器把哥德巴赫猜想与停机联系起来：它寻找不能写成两个素数之和的、大于2的偶数。[6]

从高层算法看，可以从 n = 4 开始，对当前偶数检查所有可能的素数配对；如果发现它不能写成两个素数之和，程序就停止并给出反例；如果能，就把 n 增加2，继续检查下一个偶数。对每个固定的 n，候选配对是有限的，因此这一轮检查能够结束。

这台搜索器 G 停机，当且仅当哥德巴赫猜想存在反例。如果猜想成立，G 就永远继续检查。于是，对这台专门构造的机器而言，“哥德巴赫猜想是否成立”可以改写为“G 是否永不停机”。这种对应并没有证明猜想本身，也不能因为运行很久没有停止，就断言反例不存在。

把高层搜索过程编译成少量状态和严格转移规则的图灵机，是该研究的具体技术工作。它让“数学问题可以编码为机器行为”不再只是一个抽象口号，而成为可以给出完整规则的对象。

十五、寻找集合论矛盾的机器

还可以构造另一台机器 M，枚举策梅洛—弗兰克尔集合论加选择公理（ZFC）的形式证明，逐一检查是否出现矛盾，例如 0 = 1 的证明。如果找到就停机，否则继续搜索。在标准的有效证明编码下，M 停机当且仅当这套理论不一致；若理论一致，它就不会停机。

在通常的形式化条件下，“M 不停机”表达了这套理论的一致性。哥德尔第二不完备定理说明，如果 T 一致、有效并满足相应算术表达与可证明性条件，它不能在自身内部证明标准形式的一致性陈述。因此，机器是否不停机也可能成为某套理论内部无法证明的问题。[3]

耶迪迪亚与阿伦森的论文《一台行为独立于集合论的较小图灵机》（A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory）给出了具有 7910 个状态的具体机器，并在论文规定的集合论假设下建立相关独立性结论；论文还讨论了与哥德巴赫猜想和黎曼猜想相关的机器。[6]

这里必须把简单的“搜索矛盾”思想实验与论文中的具体机器区分开：7910 状态机器有专门的构造与证明条件，不能把上面的几句算法描述直接当成它的完整定义。尤其“理论不能证明机器不停机”与“理论对机器是否停机两边都不能证明”，也需要各自的论证，不能省略条件相互替代。

十六、把这段历史重新放回 AI

从希尔伯特的形式化要求，到哥德尔将语法关系算术化，再到图灵对机械计算的分析，数学家逐步澄清了符号操作能够做什么、不能保证什么。现代计算机把这些思想变成广泛使用的技术基础，但不同理论解决的问题仍有各自边界。

生成式语言模型在这条历史线上带来了一种新的候选生成方式：用训练得到的统计结构和表示，根据上下文产生后续表达。数学 AI 可以把这种能力嵌入更大的搜索系统，让模型提出方向，让工具执行计算，让验证器审查形式证明。

因此，把它们联系起来的关键不是“都在写字”这一表面相似，而是表示、生成、搜索与验证之间的分工。字符串只是共同的载体；载体中的内容是否有意义、是否表达了正确目标、是否符合推理规则，仍然要分别检查。

十七、为什么生成、搜索与验证值得结合

在形式数学中，验证器能够给出明确的接受标准，而生成器可以利用学习所得的经验，尝试提出更有希望的中间引理、证明步骤或策略。两者结合后，系统既有方向选择能力，也有能够拒绝错误候选的检查环节。

图：左侧候选进入中央验证器；上方为通过结果，下方为未通过后的检查与修订，修订稿再次提交。

不过，推理模型输出较长的中间文本，并不自动意味着它调用了形式验证器。自然语言自检、数值试验、运行代码和检查形式证明，提供的保证各不相同。评估一套数学 AI 时，应具体查看它生成了什么、检查了什么，以及最终结果依赖哪些假设。

第十节的循环适用于真正接入外部检查的系统。它既可以在整份证明层面运行，也可以围绕局部步骤反复尝试；无论粒度如何，最终可信度都依赖目标形式化是否准确、验证标准是否严格，以及候选是否完整通过这些标准。

十八、能生成文本，不等于能生成任意有效证明

在固定系统 T 中，如果命题 P 不可证，就不存在一份符合 T 的规则且以 P 为结论的有限形式证明。模型可以生成许多写着“证明完成”的文本，却不能因此把它们变成有效证明。不存在的目标，不会因为语言表达更加流畅而出现。

这并不妨碍模型提出新猜想、寻找反例、建议新公理，或探索其他理论中的论证。但这些行为改变了任务的性质，需要明确说明新的前提与目标；它们不能被当作原来那份 T 内证明已经找到。

所以，“生成能力很强”是对提出候选能力的描述，“数学真理全部可以被同一有效理论证明”则是另一种更强的主张。不完备性提醒我们二者有本质差别，同时并未否定生成模型在大量可解任务中的价值。

十九、AI 真正可能改善的是搜索方式

朴素搜索把所有字符串依次检查，往往把绝大多数时间耗费在无意义的候选上。实际的证明工具早已使用规则选择、约束传播和各种启发式策略；学习方法可以进一步利用历史证明与当前目标的信息，帮助分配搜索资源。

例如，面对一个证明目标，系统可以优先尝试更可能相关的引理，而不是按固定顺序穷举；尝试失败后，也可以根据错误信息调整方向。这里改善的是“先试什么、如何组合步骤、何时回溯”，并非让原本不可证的命题突然在原理论中可证。

学习得到的偏好也可能漏掉不常见但关键的路径。因此，一个系统若要声称“只要证明存在就保证最终找到”，还须说明搜索的覆盖性质，而不能只展示若干成功例子。实践中，人们常在保证、效率与资源限制之间作出取舍，这正是值得研究的工程与理论问题。

二十、怎样准确理解 AI 推理

AI 推理仍然是一种计算活动，但不能只用“吐字符串”四个字就穷尽对它的解释。字符串可以承载随意的文本，也可以承载复杂的算法、严密的证明或有待验证的猜想；仅仅指出输出是符号序列，还没有评价其中计算与论证的质量。

对数学应用，更有用的问题是：模型提出了哪些候选，搜索过程排除了哪些分支，工具实际验证了哪些结论，以及结果在哪套公理与定义下成立。这些问题能把表面的流畅表达与可检查的数学成果区分开来。

哥德尔与图灵给出的限制，使我们知道某些普遍保证无法实现；生成、搜索和验证技术的进步，则决定我们在具体任务和有限资源下能够走多远。理论边界与实际能力的提升可以同时成立，并不相互抵消。

结语：继续生成，何时能够成为答案

当屏幕上的回答一点点展开时，我们可以把它看作一个计算系统正在构造新的符号序列。若任务是数学证明，真正重要的时刻并不是出现“所以得证”，而是这些符号确实构成了目标系统中可以核查的论证。

从希尔伯特到哥德尔，再到图灵，数学基础研究让我们认识到：明确的规则带来了可靠检查的可能，也让某些不可逾越的限制能够被严格表述。今天的数学 AI 继承了这个问题，并在候选生成与搜索效率上开拓新的方法。

我们完全可以期待机器帮助找到更多证明，也应准确描述这种期待的条件。继续生成可能通向一个此前没有发现的答案，也可能只是继续搜索；只有把目标、系统、策略与验证结果说清楚，才能判断一次推理究竟取得了什么。

参考资料

1. 《斯坦福哲学百科全书》：“希尔伯特纲领”（Hilbert’s Program）。用于形式化与有限主义一致性目标的历史背景。https://plato.stanford.edu/entries/hilbert-program/
2. 库尔特·哥德尔，1931 年：《论〈数学原理〉及有关系统中的形式不可判定命题Ⅰ》（Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I）。https://doi.org/10.1007/BF01700692
3. 《斯坦福哲学百科全书》：“哥德尔不完备定理”（Gödel’s Incompleteness Theorems）。用于第一、第二不完备定理的条件及语义区分。https://plato.stanford.edu/entries/goedel-incompleteness/
4. 艾伦·图灵，1936 年：《论可计算数及其在判定问题上的应用》（On Computable Numbers, with an Application to the Entscheidungsproblem）。https://doi.org/10.1112/plms/s2-42.1.230
5. 汤姆·布朗（Tom Brown）等，2020 年：《语言模型是少样本学习器》（Language Models are Few-Shot Learners）。用于自回归语言模型背景，不能据此断言所有当代产品的内部实现完全相同。https://arxiv.org/abs/2005.14165
6. 亚当·耶迪迪亚与斯科特·阿伦森，2016 年：《一台行为独立于集合论的较小图灵机》（A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory）。https://arxiv.org/abs/1605.04343