上一章《扩散语言模型》换了生成顺序，答案可能算错；这一章换的是「谁来算」。 大模型能写出天衣无缝的推理，然后给出算错的答案——它在「生成一段像推理的文字」，而不是「执行一次推理」。 神经符号的路子是——别让它算，让它把问题翻译成形式化的样子，再交给一个真的会算的东西（求解器）。
| 对比 | 生成（神经网络） | 求解（符号系统） |
|---|---|---|
| 在做什么 | 给定前文，产出最可能的下一个 token（词元） | 给定约束，在解空间（所有可能答案的集合）里搜索一个满足条件的解 |
| 输出性质 | 「看起来对」——没有正确性保证 | 「保证对」——在算得完的前提下，要么找到解，要么证明无解 |
| 强项 | 理解模糊的、自然语言的、没有明确定义的问题 | 精确计算、穷尽搜索、严格验证 |
| 弱项 | 多步算术、长链推理、严格约束 —— 会自信地算错 | 理解不了自然语言；问题稍大就搜索爆炸 |
你找一个懂中文的人帮你解一道数学题。
方案 A：让他凭脑子算，然后口头告诉你答案——他可能理解得很好，但也可能算错。
方案 B：让他先把题目准确翻译成数学式子，然后把式子交给计算器。
两边都在做自己擅长的事：「翻译」是模型的强项，「计算」是计算器的强项。符号系统（用规则一步步推导的系统）和求解器就是那个计算器——让模型做翻译官、求解器做计算器，就是神经符号（neurosymbolic）的全部动机。
这个类比管到「谁来算」为止：真实问题里，「把题目看懂、补全隐含前提」常常才是最贵的那一步。
| 方式 | 数据往哪流 | 典型用法 |
|---|---|---|
| ① 神经 → 符号 | 模型把自然语言问题翻译成形式化约束，交给求解器执行 | 计算器、代码解释器、约束求解、SQL（数据库查询语言）生成。 今天最成熟、最常用的一条 |
| ② 符号 → 神经 | 用求解器生成保证正确的推理链，拿去训练模型 | 合成训练数据（呼应阶段 5 的 RLVR：用可自动验证的结果当奖励的强化学习）。 穷举小规模问题、生成带标准答案的推理过程 |
| ③ 神经 ↔ 符号 | 循环交互：模型提方案 → 验证器挑错 → 模型修正 → 再验证 | Lean/Coq（把证明写成计算机能逐行检查的语言）里的定理证明、代码生成跑单测（单测 = 单元测试）。 这也是所有「采样 + 验证」范式的形状 |
下面是一个真实的组合求和问题。求解器这边跑回溯搜索（一层层试着填，填错就退回来换一个）—— 它会真的枚举、真的剪枝、真的给出答案。 模型那边用概率模拟它的出错行为（这一点下面标清楚，不糊弄你）。
互动 · 同一个问题，两条路
路线 A · 让模型直接答
路线 B · 翻译成约束再求解
路线 A 只是「挑一个看起来合理的」，它不会告诉你这次对不对。
路线 B 的搜索只要跑得完，答案就是保证正确的，还能告诉你「一共有几个解」「无解」——这些生成模型给不了。
剪枝让搜索量比暴力枚举小得多，这是符号求解的效率来源。
往下拖那两个滑块：只要验证足够便宜可靠，「多生成几个」就能换成「更高的正确率」。 下面那三个现象，用的都是这一条。
假设模型单次答对的概率是 p。你让它答 N 次，再让一个验证器帮你挑出对的—— 最终成功的概率是：
互动 · 采样 N 次 + 验证，成功率怎么涨
像一场考试：学生答题就是生成，一道题可能做错；老师批卷就是验证，看一眼答案对不对。 批卷比答卷快得多——所以「多叫几个学生各答一份、老师挑出对的那份」， 往往比「逼一个学生答到全对」更划算。 这个类比管到「答案对错一眼能看清」为止：开放题没有标准答案，老师也判不了。
图解 · 这条公式解释了三个看似无关的现象
上面的公式假设验证器永远判断正确。现实里它经常不成立：单测只能测你写了的用例，
写作、共情这类开放任务根本没有验证器。
所以「验证比生成容易」是一个方向，不是一个自动兑现的保证：越能严格判定的任务，这条路越灵。
「神经网络 + 符号系统」已经大规模落地、效果极好的例子，不是定理证明，而是写代码。
| 环节 | 谁负责 | 为什么合适 |
|---|---|---|
| 理解需求 | 神经网络 | 把模糊的自然语言需求变成具体的实现意图——这是语言模型的强项 |
| 生成代码 | 神经网络 | 代码是「半结构化的自然语言」，模型在大量代码上训练后能写得像模像样 |
| 执行 | 解释器 / 编译器 | 精确、确定、不会算错。这是符号系统的主场 |
| 验证 | 单元测试 / 类型检查 | 可自动运行、给出明确的通过 / 失败。这是「便宜的验证器」 |
| 修正 | 神经网络 | 把报错信息读回去，改一版再试——这就是上面说的「循环交互」 |
图解 · 代码同时满足三个条件
定理证明有验证器（Lean 编译器），但形式化、生成证明都难，训练数据也稀少；写作则根本没有验证器。
| 方向 | 代表 | 做了什么 |
|---|---|---|
| 工具调用 | 计算器、Python 解释器、SQL、搜索引擎 | 今天最普遍的一类。模型决定「该用哪个工具、传什么参数」， 工具负责精确执行（呼应阶段 7 的 Agent） |
| 代码 + 测试 | AlphaCode、GPT 系列 + 单测 | 生成大量候选，用测试筛。Codeforces（编程竞赛网站）上平均排到前 54%，略低于人类中位 |
| 几何定理 | AlphaGeometry | 神经模型负责「往哪个方向添辅助线」，符号引擎负责严格推导。 IMO（国际数学奥林匹克）几何题上达到接近金牌水平 |
| 形式化数学 | Lean + LLM、AlphaProof、DeepSeek-Prover | 把证明写成计算机能检查的形式化语言，逐行验证。 IMO 2024 上 AlphaProof 与 AlphaGeometry 2 合计拿到 28 分（银牌上沿） |
| 程序综合 | DreamCoder、程序归纳 | 不生成答案，而是生成解决问题的程序。学到的程序可以复用 |
| 概率逻辑 | DeepProbLog、神经符号概念学习 | 把逻辑规则和神经网络端到端地结合，可微地训练规则（可微 = 能算出梯度，所以能端到端训练） |
| 知识图谱 | KG + LLM 混合问答 | 结构化知识保证事实正确，模型负责理解问法（呼应阶段 7 的 RAG） |
图解 · 谱系其实就是一条线：符号占多少
越往右，正确性的保证越强，能处理的问题面越窄——这就是这一章一直在说的取舍。
前六节反复说「让符号系统去算」。可它到底怎么算的？为什么它给出的答案保证对？ 这一节把那一半拆开——看完这棵真的搜索树，你脑子里就有「穷尽搜索」这张图了。
互动 · 一棵真的搜索树：从上往下试，走不通就回头
一串钥匙、一把锁，你一把一把试。
① 每试一把，就是树上往下走一层；② 试错了就退回来换下一把（回溯）；
③ 更聪明的做法是——钥匙一看就太宽插不进去，那这把连试都不用试（剪枝）。
「保证对」的来源：你把该试的都试过了，所以要么找到能开的那把，
要么能说「这里根本没有」——这就是符号系统比生成模型多出来的那件事。
悬停卡里的 a、b、c，树上对应的一层会亮：第一层在定 a，第二层在定 b； c 不用搜——目标和 T 一确定，c 就唯一确定了。
图解 · 剪枝省掉的，比真的试了的还多
橙色是「不剪枝要试的」，绿色是「剪枝后真的试的」。两根柱子的高度差，就是剪枝省下来的。
图解 · 问题一大，剪枝省得越多
目标是 6 时两条线还挨着；到 12，暴力那条已经冲上去了，剪枝那条几乎没动。
| 瓶颈 | 说明 | 什么时候真的会痛 → 换什么 |
|---|---|---|
| ① 翻译本身就是瓶颈 | 把自然语言问题准确地写成形式约束，难度不比直接解它低；现实中「看懂题目、补全隐含前提」往往才是最贵的一步。翻译错了，再可靠的求解器也救不回来——它只会精确地给出错误的答案。 | 题目带歧义、要靠常识补全 → 先让模型把题意和约束复述一遍，给人核；核不动就别上这条路 |
| ② 只在有严格定义域的领域可用 | 数学、代码、约束满足、逻辑推理有明确对错；写作、共情、审美根本没有「求解器」——你没法把「这段话说得得体吗」写成约束满足问题 | 任务沾主观评价 → 别用这条路，改用「采样 + 人评」或直接生成 |
| ③ 求解器会爆炸 | 符号求解的复杂度常常是指数级：小规模能跑，规模一大就卡死。这是符号 AI（用人写的规则做推理的 AI）在 1980 年代撞上的墙，今天只是被机器学习绕开了，没有被解决 | 变量一多就超时 → 缩小问题规模，或退回近似、学习的方法 |
| ④ 边界模糊 | 真实问题往往部分可形式化：一半写成约束，另一半靠常识。线画在哪，目前没有原则性的方法，只能一个任务一个任务地试 | 只能试 → 先挑「能完全形式化」的子任务下手 |
图解 · 问题一大，求解器就爆炸
纵轴是对数——看上去只是爬了一点，实际每多一个变量就翻一倍； 横着那条虚线是「一秒大约能算十亿次」的位置。
「神经符号」听起来像是「两者优点都要」的万能答案，但实际效果取决于一个很朴素的问题：
这个问题有没有一个可靠的验证器？
有 → 这条路非常有效（代码、数学、约束）；
没有 → 那所谓的「符号部分」就只能是一层薄薄的格式约束，帮不上实质的忙。
回到第 4 节那张「采样 N 次 + 验证，成功率怎么涨」： 把「采样次数 N」从 1 拖到 32，看「至少一个正确」怎么从 p 爬到接近 100%； 再把「单次正确率 p」往左拖到 5%——模型几乎不会，多试几次也能救回来。
这条不对称性就是整章的价值：生成是碰运气、可以重复很多次；验证只要做一次，而且便宜得多。
| 任务 | 生成它 | 验证它 |
|---|---|---|
| 找一个满足约束的解 | 要在巨大的解空间里搜索，还可能压根没有解 | 拿到一个解，逐条代入检查就行——多项式时间（工作量随规模温和增长，不会爆炸） |
| 写一个能通过所有测试的程序 | 每一个 token 的选择都可能把整段带偏 | 把测试跑一遍，通过 / 不通过是一个确定的事实 |
| 写一段得体的道歉信 | 模型很拿手 | 无解——没有验证器，这条不对称性在这里直接消失 |
这一章主要跟 A、B、C 三条暗线搭得上话，D–F 没有额外要说的。
| 暗线 | 这一章的回答 |
|---|---|
| A 信息流动 | 这一路上换了两次语言：自然语言问题 → 形式化约束（符号表达式）→ 解 → 自然语言解释。
瓶颈全在第一次转换——也就是第 7 节 ① 那个瓶颈。
神经那一半始终按 |
| B 什么被牺牲了 | 牺牲了覆盖面，也牺牲了可迁移性：这套管线是「一个任务一套翻译 + 一套求解器」， 换一个领域就要重做一遍（第 7 节 ④「边界模糊」说的就是这个）。 换来的东西很硬：一个要么给对、要么明确说无解的答案。 在写作、共情这类任务上它换不到任何东西——那些领域连验证器都没有 |
| C 参数账本 | 这一章的账不在权重上，在「用多少次生成换一次正确」上。第 4 节那条成功率公式就是账本： p=30% 时，N=1 → 30%、N=4 → 76.0%、N=10 → 97.2%、N=32 → 99.99%； 最极端的一格是 p=5%、N=32 → 80.6%。验证只在最后挑一次，不跟着 N 翻倍—— 这就是整条路线能成立的经济学基础 |
它接住了什么：《扩散语言模型》换了「生成顺序」这个先验， 这一章换的是更根本的一件事——「谁来算」： 想得再久，也解不开一个本该交给求解器的问题；而一旦有了验证器，「多想」就直接变成「多试」。
它给下一章留了什么：如果连「想多久」都能按题目难度分配， 那「走多少层」为什么不能？这就是《自适应计算》要接的那件事。
核心区分是生成 vs 求解：模型当翻译官，求解器当计算器。只要验证足够便宜可靠， 多生成几个就能换成更高的正确率——所以判断一个神经符号方案，只问一句：它的验证器是什么？
上面讲的都是「够用」的版本。想往下挖，这里有三个入口—— 它们不是必修内容，是给想再往前走一步的读者准备的。