程序、求解器与符号工作

自然语言链很灵活，但它把两种不同的工作交给同一个模型：分解问题，以及执行分解后的步骤。对算术、代码、表格、定理证明和许多规划任务来说，这不是一个好的分工。模型可能理解了结构，却在局部计算上出错。程序辅助推理把模型放回它擅长的位置：把含糊的问题翻译成结构化产物，而执行则交给拥有精确规则的运行时。

翻译才是学习到的部分

核心模式是：

$$p = T_\theta(x), \qquad y = E(p),$$

其中 $x$ 是自然语言任务，$T_\theta$ 是作为翻译器的模型，$p$ 是程序、查询、符号推导或证明脚本（即可被机器检查的证明），$E$ 是带显式语义的执行器。PAL 让模型为数学、符号和算法推理生成 Python 程序，再由解释器计算答案 (Gao et al. 2022)。Program of Thoughts 对数值和金融推理做了同样的拆分：模型写出近似代码的推理，外部计算机负责算术 (Chen et al. 2022)。Faithful Chain-of-Thought 则把这个想法推向可解释性：先把问题翻译成符号推理链，再由确定性求解器执行 (Lyu et al. 2023)。

关键变化不在于「代码很神奇」，而在于错误表面变了。自然语言链可以流畅而错误，却不会撞上任何清楚的边界。程序要么解析成功，要么解析失败。单元测试要么通过，要么失败。证明脚本要么通过类型检查，要么返回类型错误（也就是某个证明步骤被拒绝）。符号产物给系统提供了反馈入口，这也是本章放在搜索和验证器之间的原因。

def program_aided_reasoning(question):
    program = model.generate(
        "Translate the problem into a small deterministic program.\n" + question
    )
    try:
        value = sandboxed_python(program, timeout=2.0)
    except RuntimeError as err:
        repair = model.generate(format_error(question, program, err))
        value = sandboxed_python(repair, timeout=2.0)
    return model.generate(format_final_answer(question, value))

这也是推理与编排开始相互靠近的地方。解释器就是一个工具。沙箱、超时和修复循环都是 harness 决策。第 41 章 会把它推广成完整的智能体运行时，但最小版本已经在这里出现了。

由构造得到的忠实性

思维链忠实性之所以有争议，是因为可见解释未必是导致答案的那段计算。符号执行给出一个更窄但更强的性质。如果最终答案来自运行 $E(p)$，那么产物 $p$ 就处在答案的因果上游。模型为什么选择 $p$ 仍可能不透明，它给出的自然语言解释仍可能是事后整理，但被执行的那部分可以检查。

Faithful CoT 明确区分了这一点。它要求语言模型把自然语言翻译成符号链，再用确定性求解器推出答案 (Lyu et al. 2023)。保证是有条件的：只要翻译正确，解释就忠实于求解器的计算。这比「模型隐藏计算完全可见」小得多，却是工程用得上的主张。

代码生成里也有同一结构。模型可能幻觉一个算法；但候选一旦变成代码，测试和静态检查就能找出很大一类错误。这正是编程任务成为推理模型核心场景的原因：它同时提供丰富的分解语言，以及会回话的运行时。

运行时成为推理器的一部分

外部执行器不是被动基础设施。它改变了推理的含义。

• Python 与 SQL 把算术、聚合和表格推理变成执行问题。模型的任务是选择变量、操作和 schema 引用。
• 计算机代数系统（CAS）与 SMT 求解器（前者对符号数学做代数运算，后者按背景理论判定可满足性、检查逻辑约束）把代数和约束满足变成带精确语义的搜索问题。模型负责形式化。
• 证明助手 把证明变成一串可类型检查的步骤。模型写 tactic（构造证明的命令）或 term，由一个被称为内核（kernel）的小型可信核心负责检查。
• 网页或检索工具 把缺失事实变成观察。ReAct 表明，把推理与动作交错起来，可以在问答里减少幻觉，因为观察会作为外部证据进入轨迹 (Yao et al. 2022)。

这张列表是一条从宽覆盖、弱检查到窄覆盖、强检查的梯度。它对应 第 27 章 的验证器阶梯。运行时越形式化，流畅但错误的空间越小；但模型要把任务翻译成那种形式语言，难度也越高。

证明助手这一级已不再是纸上谈兵。AlphaProof 用 AlphaZero 式强化学习训练智能体写 Lean 证明，在 2024 年 IMO 题目上达到银牌水平 (Hubert et al. 2025)；DeepSeek-Prover-V2 把强化学习与递归子目标分解结合起来，在 Lean 4 中做到 miniF2F-test 上 88.9% (Ren et al. 2025)。AlphaProof 报告的瓶颈是自动形式化，也就是把非形式化命题翻译成 Lean，正是上面这条梯度所指出的那笔翻译成本。

失败移动到了接口处

程序辅助推理没有消灭失败。它把失败移动到可测试的边界上。

• 翻译错误。 程序解决的不是用户问的那个问题。执行是精确的，但精确地执行了错误形式化。
• 状态缺失。 模型漏掉单位、表格列或隐藏约束。没有进入产物的信息，运行时无法补回来。
• 沙箱错误。 生成程序不安全、太慢、非确定，或依赖不可用包。执行器必须是受控服务，而不是裸 shell。
• 修复循环漂移。 错误消息有帮助，但反复修复可能让产物偏离原问题，除非验证器持续把它拉回任务本身。

第一类失败最难。一个程序可能通过自己的测试，却回答了错误规格。对生产系统来说，这正是程序辅助推理必须和结构化输出、测试生成、审查一起出现的原因。运行时让某些错误变清楚；它并不证明规格本身正确。

程序、求解器和证明脚本于是构成一座桥。它们让模型在歧义有用的地方使用自然语言，在歧义昂贵的地方使用形式系统。下一章直接研究形式化那一侧：有哪些验证器，过程监督与结果监督有何不同，以及检查器何时成为推理栈里的稀缺资产。

延伸阅读