程序、求解器与符号化工具

语言模型可以识别问题的结构，却仍可能在算术、格式错误的查询或一个无效证明步骤上丢掉答案。可执行推理把这些工作分开：模型提出程序、查询、约束系统或证明；运行时按照明确规则解释这项产物；任务级检查再判断结果是否回答了原始请求。运行时会让一些错误显现出来，但不会保证翻译正确。精确执行了错误形式化的解答，仍然是错的。

这种模式之所以重要，是因为自然语言和形式系统的失效方式不同。自然语言足够宽松，可以表达一个条件尚未充分说明的问题；程序或证明必须先满足语法和接口要求，才能运行。把一部分工作移入可执行产物，可以把系统的可测试边界放到更合适的位置，但用户原意和产物表达之间的语义缺口仍然存在。

可执行产物需要明确约定

真正有用的抽象不是「模型调用 Python」，而是概率翻译器与受控执行器之间的一道类型化边界：

$$p \sim q_\theta(p \mid x,C), \qquad r = E_\Gamma(p), \qquad r=(s,o,\tau,u).$$

这里，$x$ 是原始请求；$C$ 是产物约定，包括语法、类型、允许的操作、输入结构和输出结构；$q_\theta$ 是参数为 $\theta$ 的模型在该约定下对产物给出的分布；$p$ 是一次采样得到的产物；$\Gamma$ 是固定的执行环境，包括运行时与依赖版本、数据快照、权限和资源上限；$E_\Gamma$ 是这个环境中的执行器；$r$ 是结构化结果。结果的四个字段分别是状态、取值、轨迹和资源用量，即状态 $s$、类型化输出 $o$、执行轨迹 $\tau$ 和资源用量 $u$。常见状态包括 ok、parse_error（解析错误）、type_error（类型错误）、policy_violation（策略违规）、runtime_error（运行时错误）和 timeout（超时）。

确定性程序也只有相对于该环境才是确定的。SQL 查询读取的是某一个数据库快照。Python 代码受浮点规则、软件包版本、区域设置和时间来源影响。求解器可能返回 unknown，也可能耗尽预算。可复现性要求记录 $\Gamma$，而不只是保存生成的文本。

约定应当足够狭窄，使产物可以在执行前接受检查。计算器任务可以只允许一门小型表达式语言，而不是任意 Python。报表任务可以只允许查询白名单结构，而且凭据只读。证明服务可以只接收一个定理陈述和一个证明项，导入项由服务固定。较小的语言可以同时减少歧义和权限。

执行成功不等于答案正确

下面三项检查回答三个不同问题：

1. 良构性： $p$ 是否符合约定 $C$？解析、结构校验、类型检查、导入策略和静态限制都属于这一层。
2. 执行成功： $E_\Gamma$ 是否在权限和资源预算内完成，而且状态为 ok？
3. 任务一致性： 产物、假设、输入和结果是否仍与 $x$ 相符？

验收规则可以明确写出这三个层次：

$$\operatorname{Accept}(x,p,r) = W_C(p) \land [s=\texttt{ok}] \land A(x,p,r).$$

$W_C(p)$ 是约定 $C$ 定义的良构谓词，$s$ 是结果 $r$ 中的执行器状态，$A(x,p,r)$ 是任务一致性检查。$s=\texttt{ok}$ 外的方括号表示对这个条件取布尔值。Accept 只有在三个条件全部成立时才为真。

前两项检查往往可以机械完成，第三项才是难点。程序可以完全正常地运行，却使用了错误的税率。SQL 查询可以语法正确，却把客户标识符和账户标识符接错。证明可以证成一个定理，但定理中的量词与非形式化主张并不一致。精确执行只会把错误形式化封装起来，并不会修好它。

下面这个可运行示例把翻译明确表示为一小份数据产物。题目问：240 个螺栓的五分之三要装箱，每箱 12 个，需要多少箱？两个产物都能执行，只有一个保留了题目给出的分数。

from fractions import Fraction

problem = {"total": 240, "fraction": "3/5", "per_box": 12}

artifacts = [
    (
        "wrong but runnable",
        {"total": 240, "fraction": "2/5", "per_box": 12},
    ),
    (
        "correct artifact",
        {"total": 240, "fraction": "3/5", "per_box": 12},
    ),
]

def execute(artifact):
    packed = artifact["total"] * Fraction(artifact["fraction"])
    boxes = packed / artifact["per_box"]
    if boxes.denominator != 1:
        raise ValueError("the result is not a whole number of boxes")
    return boxes.numerator

def check_task(problem, artifact, result):
    for field in ("total", "fraction", "per_box"):
        if artifact[field] != problem[field]:
            return f"contract rejects: {field} mismatch"
    expected = execute(problem)
    if result != expected:
        return "contract rejects: result mismatch"
    return "contract accepts"

for label, artifact in artifacts:
    result = execute(artifact)
    verdict = check_task(problem, artifact, result)
    print(f"{label}: executes to {result}; {verdict}")

输出为 wrong but runnable: executes to 8; contract rejects: fraction mismatch 和 correct artifact: executes to 12; contract accepts。这个检查器能发挥作用，是因为示例已经把任务拆成结构化字段。换句话说，$A$ 表示任务一致性检查；对于自由形式的法律、医疗或商业请求，构造 $A$ 可能比执行产物 $p$ 更难，仍可能需要人工审查、独立测试、以来源为依据的约束或弃答。

各类运行时究竟能证明什么

「工具使用」把语义差异很大的系统归到了一起。关键问题不是工具够不够形式化，而是一次成功返回究竟能证明什么。

SMT 是「可满足性模理论」的缩写。这类求解器会在布尔可满足性上加入算术、数组或位向量等理论。它可以为可满足的编码给出模型，可以在受支持的片段中证明不可满足，也可以返回 unknown。计算机代数系统则按照定义域假设处理表达式。两者都不理解编码之外的用户意图。

证明助手提供了一道更窄也更强的边界。在 Lean 中，策略和自动化会构造证明项，再由一个小型内核对照形式环境检查这些证明项 (Moura and Ullrich 2021)。这种架构缩小了可信检查核心，但保证仍然以定理陈述、定义、导入项和公理为条件。它也不表示可以安全构建不可信的证明包，因为策略和其他元程序可能在最终内核检查之前执行代码。

把检索放进表格，是为了划清类别边界。ReAct 把推理、动作和观察交错起来，使轨迹可以利用外部证据 (Yao et al. 2023)。观察结果是新信息，不是证书。网页可能过时，工具可能失败，动作也可能改变状态。因此，检索还需要来源核验和授权，不能只看它是否执行成功。

程序辅助方法证明了什么

Gao 等人在 2022 年提出程序辅助语言模型（PAL），相关工作于 2023 年发表于 ICML。PAL 让模型把中间推理写成 Python 程序，再交给解释器执行。这项研究的实验证据覆盖十三项数学、符号和算法任务 (Gao et al. 2023)。这些结果支持一个边界明确的结论：当分解过程可以写成代码时，外部执行可以替模型完成局部计算。

Chen 等人的 Program of Thoughts（PoT）于 2023 年发表于 TMLR，采用类似的分工来处理数值推理。评测覆盖五个数学应用题数据集和三个金融问答数据集 (Chen et al. 2023)。PoT 可以交错生成解释文本和程序语句，但只有执行的语句才具备解释器语义，注释和普通文字仍只是模型输出。

Lyu 等人在 2023 年提出 Faithful Chain-of-Thought，把产物从 Python 扩展到其他形式。它把请求翻译成含有任务专用符号语言的推理链，再用 Python、Datalog 或 PDDL 规划器执行符号部分。论文评测了数学应用题、规划、多跳问答和关系推理 (Lyu et al. 2023)。这些领域都能暴露有用的形式化中间结果，但不能证明任意开放式推理都能以同样方式翻译或检查。

这些工作的共同贡献在于提供一套接口，而不是新的真相来源。变量、操作、关系和假设仍由模型选择，运行时只是让这些选择产生明确后果。它的价值恰恰在于：解析失败、类型违规、反例或遭拒绝的证明，都可以作为结构化反馈交还控制器。

忠实性有三层含义

可执行推理常被称为忠实，但需要把三种主张分开：

• 执行忠实性是指返回值确实由已执行产物机械推导而来。如果系统以 ok 状态得到 $r=E_\Gamma(p)$，并且在没有未经检查的模型旁路时呈现类型化输出 $o$，那么 $p$ 就处于答案的因果上游。也就是说，最终答案必须由这份产物的执行结果产生。
• 语义忠实性是指 $p$ 正确表达了原始请求，包括实体、单位、假设和约束。执行本身不能证明这一点。
• 叙述忠实性是指解释准确描述了产物和执行轨迹。模型写出的解释仍可能是事后编造，也可能与代码矛盾。

Faithful CoT 加强的是第一种性质。它并不会暴露模型的隐藏计算，也不能说明翻译器为何选择了 $p$。翻译正确是任务答案正确的必要条件，却不是「答案确实由执行器根据产物生成」这一较窄因果事实的必要条件。

这一区分会影响最后的呈现步骤。若系统未经检查就返回 model.generate(explain(result))，模型便多了一条篡改正确结果的路径。生产系统应当确定性地呈现类型化取值，或者从生成说明中提取答案，并核对它是否等于执行器输出。解释可以灵活，答案与执行结果之间的绑定不能松动。

修复是一轮受控搜索

执行反馈可以改善候选，但修复循环需要遵守与 第 25 章 中搜索控制器相同的纪律。首先要对失败分类：

• 解析、结构或类型错误属于产物约定问题；
• 策略错误涉及禁用的导入项、操作或权限；
• 运行时、超时和资源错误发生在环境 $\Gamma$ 中；
• 任务检查失败说明翻译或假设有问题；
• 呈现错误发生在类型化输出到用户可见答案的绑定环节。

每次尝试都要保留不可变的原始请求，产生一份带版本的产物，并只接收某一类失败的结构化诊断。控制器需要尝试次数上限，以及总成本或墙钟时间上限。每份修复后的产物都必须按完整约定重新检查，语法修复不能继承上一版的语义批准。如果没有候选通过，系统应当弃答或回退，而不是返回最后一个能运行的产物。

诊断信息同样是一道输入边界。不要把原始秘密、任意工具输出或未经限制的编译器日志送回模型。错误信息需要规范化，敏感值需要删除，长度需要限制，不可信文本也要明确标记。修复提示仍然是提示，工具输出可能包含控制器不应服从的指令。

形式化之后，形式证明才有强保证

证明内核可以把自己的保证说得很精确。设 $K$ 是健全的内核，$\Delta$ 是由定义和公理组成的形式环境，$\pi$ 是证明项，$\varphi$ 是待检查命题，那么

$$K(\Delta,\pi,\varphi)=\operatorname{accept} \quad\Longrightarrow\quad \Delta\vdash\varphi.$$

推导符 $\vdash$ 表示 $\varphi$ 可以从 $\Delta$ 推导出来。这是对形式对象的强保证，但它本身没有说明 $\varphi$ 是否忠实翻译了非形式化问题，$\Delta$ 中的公理是否可以接受，或外围构建过程是否安全。要实现高保证检查，定理陈述和允许使用的环境必须来自可信来源；生成的证明应在隔离环境中构建，再由内核或独立检查器复查。

近期的定理证明系统同时展示了这道边界的强度和成本。在 2024 年国际数学奥林匹克评测中，AlphaProof 证明了五道非几何题中的三道，这些题目由专家手工形式化；AlphaGeometry 2 则解出了几何题。AlphaProof 与 AlphaGeometry 2 的组合系统获得 42 分中的 28 分，等同于银牌成绩。最难的题目使用了耗时数日的计算 (Hubert et al. 2026)。因此，这次现场评测没有衡量从非形式化语言到形式语言的翻译，专家预先完成了非几何题的形式化，之后系统才搜索证明。

DeepSeek-Prover-V2 同样从形式化的 Lean 定理陈述开始。这个 6710 亿参数模型在由 244 道题组成的 miniF2F 测试集上，每个定理采样 32 份证明时证明了 82.4%，使用 Pass@8192 预算时证明了 88.9%，即最多生成 8,192 份证明，其中至少一份被接受 (Ren et al. 2025)。Pass@8192 不是单样本准确率，这项基准也不衡量从非形式化语言到形式语言的翻译。这些限定不会削弱已经通过检查的证明，只是指出实验实际测量的内容：形式化陈述和检查器已经存在之后的证明生成。

执行器是一道安全边界

生成产物属于不可信代码，即使它只用来做算术。超时机制本身不是沙箱。生产执行器应当把权限限制在狭窄范围内：

• 每次运行都使用无特权身份，并放在用完即弃的隔离环境中；
• 默认禁止网络和文件系统访问，只开放明确指定的输入；
• 限制 CPU、内存、输出量和墙钟时间，同时限制进程与系统调用；
• 固定产物使用的运行时、依赖项、结构和数据快照；
• 使用只读数据库凭据、允许访问的数据表清单，以及查询成本和返回行数上限；
• 把消息、付款、部署和写入操作的授权放在代码沙箱之外；
• 记录来源信息，包括请求、产物哈希、环境版本、输入、状态、轨迹、资源用量、检查器版本和最终呈现；
• 发布前按输出结构和任务检查验证结果。

这些控制既服务安全，也服务正确性。固定环境可以让结果复现。最小权限也能限制翻译错误造成的损害。来源记录能帮助运维人员区分翻译器错误、运行时变化、过期数据、检查器失效和呈现错误。第 56 章 会详细讨论权限边界，第 41 章 则会把它放回更大的智能体运行时。

程序和求解器把一部分推理变成可观测的计算，却不会决定哪些观察值得信任，也不会决定如何评价中间工作。下一章会直接讨论这个缺失环节：结果检查器、过程监督、习得评判器和形式验证器。

延伸阅读