起草与修剪：为什么大模型在绝对真理面前永远是概率的囚徒？

## 一句话判断 **LLM 不是不会推理，是它的训练目标根本不是"正确"，而是"像人"。** 当一个人被训练来"听起来合理"而不是"严格正确"时，面对需要零容错率的逻辑推导，出错不是 bug，是 feature。Draft-and-Prune 的聪明之处不是让 LLM 变得更"聪明"，而是承认它的本性——让它尽情发挥创造力去"起草"各种可能，然后用冷酷无情的符号求解器去"修剪"谎言。 --- ## 一、问题：为什么写诗的 AI 在算数时撒谎？ GPT-4 能写十四行诗，能模拟哈姆雷特的独白，能写通过了 LeetCode hard 的代码。但你让它做一道 LSAT 逻辑题——不是那种需要法律知识的，是那种纯粹的、机械的、每一步都无可辩驳的逻辑链——它的表现会难看得很。 这不是因为题目"太难"。而是因为 **LLM 的训练目标和逻辑推理的目标从根本上是矛盾的。** LLM 被训练来最大化下一个 token 的概率。它的损失函数是"这段话在人类看来有多自然"。一个人说"所有猫都是哺乳动物，加菲是猫，所以加菲是哺乳动物"—— LLM 会打高分，因为这"听起来对"。但如果前提中隐藏了一个微妙的条件——"除非加菲是机器猫"—— LLM 可能会忽略它，因为在训练语料中这个条件太罕见，概率权重太低。 **LLM 的本质是归纳引擎**。 它从海量文本中归纳出模式："当 A 和 B 同时出现时，通常 C 也跟着出现"。它在统计的海洋里冲浪，用概率的浪花来预测下一片浪的形状。 **逻辑推理的本质是演绎机器**。 演绎不关心概率。演绎只关心"如果前提为真，结论必然为真"。在演绎的世界里，没有"大概"、没有"通常"、没有"听起来对"。只有一个冰冷的规则：每一步推导都必须无懈可击，否则整个大厦崩塌。 当你用一个归纳引擎去执行演绎任务时，会发生什么事情？ --- ## 二、Auto-formalization：让 LLM"翻译"，让符号求解器"审判" 神经符号（Neuro-symbolic）这个方向的核心思想很简单：**LLM 做它擅长的，符号求解器做它擅长的，两者协作**。 具体到这个领域，方法叫 Auto-formalization（自动形式化）： 1. **输入**：一道自然语言的逻辑题 > "所有科学家都是理性的人。爱因斯坦是科学家。所以爱因斯坦是理性的人。" 2. **LLM 翻译**：把这段话转成符号求解器能懂的程序 ```python from z3 import * Scientist = Function('Scientist', IntSort(), BoolSort()) Rational = Function('Rational', IntSort(), BoolSort()) Einstein = Int('Einstein') s = Solver() s.add(ForAll([x], Implies(Scientist(x), Rational(x)))) s.add(Scientist(Einstein)) s.add(Not(Rational(Einstein))) # 求证结论 print(s.check()) # unsat = 结论必然为真 ``` 3. **符号求解器执行**：Z3 运行这段代码，返回 `unsat`（矛盾），证明原结论必然成立。 这个流程的美妙之处在于：LLM 不需要"懂"逻辑，它只需要"翻译"。真正做逻辑推导的是 Z3——一个经过严格数学证明的 SMT 求解器，它在逻辑上的可靠性等同于数学公理。 听起来完美？问题出在第 2 步。 --- ## 三、两种失败：语法崩溃 vs. 语义背叛 ### 失败类型一：语法崩溃（Syntactic Failure） LLM 生成的代码语法错了——少了一个括号、变量名拼写错误、API 用错了。这类问题相对好解决：Z3 报错 → LLM 看到报错信息 → 修复代码。这是"编译器反馈循环"，现有的 Auto-formalization 系统（如 Logic-LM、Logic-LM++）已经能处理得不错。 ### 失败类型二：语义背叛（Semantic Unfaithfulness）——这才是致命伤 代码能运行，甚至能得出结果，但**它和原始问题的意思根本不一样。** 想象一道题： > "在一个房间里，A 说'B 在说谎'，B 说'C 在说谎'，C 说'A 和 B 都在说谎'。已知只有一个人说了真话。请问谁在说真话？" LLM 可能会生成一段运行无误的代码，但它 **遗漏了"只有一个人说真话"这个关键约束**。代码跑通了，答案出来了，但这个答案对应的是一个完全不同的逻辑问题。 这就是"语义背叛"——程序"执行成功"，但背叛了原意的语义。在自然语言到代码的翻译中，LLM 会： - **凭空添加** 它不理解的常识（"猫咪都喜欢鱼"，但题目里没说） - **遗漏隐藏条件**（"除非..."、"如果...那么..."这些嵌套逻辑） - **误解量词范围**（"所有人"变成了"某个人"） 更可怕的是：这种背叛 **无法通过语法检查捕获**。代码跑通了，Z3 没报错，一切看起来正常。但答案错了。 --- ## 四、Draft-and-Prune：创造与审判的分工 UC Berkeley 和微软的团队提出的解决方案，是一个极其简洁的三步框架： ### Step 1: Draft（起草）—— 让 LLM 尽情发散 不直接让 LLM 从问题跳到代码。而是 **先让它写"计划"**。 ``` 问题：所有人都是会死的。苏格拉底是人。苏格拉底会死吗？ 计划 1：用谓词逻辑形式化，证明 Socrates → Mortal 计划 2：用一阶逻辑，引入全称量词 ∀x(Human(x) → Mortal(x)) 计划 3：构造反证法，假设 Socrates 不会死，导出矛盾 ``` 关键设计：LLM 在"计划阶段"用 **采样**（随机性），在"代码生成阶段"用**贪婪解码**（确定性）。这意味着：同一个问题，LLM 会生成多个不同的解题思路（计划），但每个思路对应的代码是确定的。 为什么这样设计？因为 LLM 的"创造力"在高层计划上最有用，而在底层代码上需要精确。让 LLM 在计划层发散，在代码层收敛。 ### Step 2: Prune（修剪）—— 用求解器的冷酷筛选 每个计划生成一段代码，Z3 运行它。但运行结果不是直接输出答案，而是先过一道"良定义性"（well-definedness）检查： 良定义性标准：$$|S_i| = 1$$ 解释一下： - $S_i$ 是求解器执行后返回的可行假设集合 - $|S_i| = 1$：恰好有一个解。程序正确翻译了问题，且问题本身有唯一答案。**保留。** - $|S_i| = 0$：无解。程序是 **矛盾的**——要么逻辑本身矛盾，要么翻译时遗漏了条件导致前提冲突。**剪掉。** - **|S_i| > 1**：多解。程序是 **模糊的**——要么翻译时条件不足，要么量词范围搞错了。**剪掉。** 这个标准极其优雅：它不是说"答案对不对"（这需要 ground truth），而是说"这个程序描述的问题是否良定义"。一个良定义的逻辑问题必须有且只有一个解。如果程序生成的解不是 1 个，说明程序本身有问题——无论答案是啥。 ### Step 3: Aggregate（聚合）—— 多数投票定乾坤 幸存下来的路径（通过良定义性检查的）进行多数投票。如果 20 个路径中有 15 个说"答案是 A"，那么最终输出"A"。 --- ## 五、实验数据：从 33% 到 82% 的跨越 四个基准测试，涵盖不同难度的逻辑推理： ### AR-LSAT（法律逻辑推理——最难） | 方法 | GPT-4 准确率 | GPT-4o 准确率 | |------|--------------|---------------| | Direct Prompting | 33.30% | 30.30% | | Chain-of-Thought | 35.06% | 36.09% | | SymbCoT（神经符号基线） | 43.91% | 34.20% | | MAD-LOGIC（最强 AF 基线） | 53.25% | 46.80% | | **D&P（AF-only）** | **78.43%** | **78.00%** | | **D&P + CoT fallback** | **80.65%** | **82.83%** | **注意这个跳跃**：从最强的 AF 基线 53% 跳到 D&P 的 78%，**+25 个百分点**。这不是渐进改良，这是断层式突破。 更关键的对比：没有 Pruning 的话，D&P 在 AR-LSAT 上只有 **45.13%**。Pruning 把它推到了 **78.43%** —— **贡献了 33 个百分点的提升**。这意味着在 AR-LSAT 上，超过一半的路径生成的代码虽然能运行，但语义上是错的，被 Pruning 无情地剪掉了。 ### ProofWriter（证明生成） | 方法 | GPT-4 | GPT-4o | |------|-------|--------| | CoT | 68.11% | 72.67% | | SymbCoT | 82.50% | 80.20% | | MAD-LOGIC | 92.00% | — | | **D&P** | **98.33%** | **99.67%** | 从 92% 到 98%，接近天花板。 ### PrOntoQA（本体问答）& LogicalDeduction（逻辑演绎） | 方法 | PrOntoQA | LogicalDeduction | |------|----------|------------------| | Direct | 77.40% / 84.70% | 71.33% / 84.70% | | CoT | 91.00% / 99.00% | 74.67% / 91.33% | | MAD-LOGIC | 100.00% / — | 94.33% / — | | **D&P** | **99.32% / 100.00%** | **99.50% / 100.00%** | 在 GPT-4o 上，PrOntoQA 和 LogicalDeduction 双双达到 **100%**。 --- ## 六、为什么 Pruning 是决定性的？ 实验中最震撼的发现是 Pruning 的杠杆效应： **在 AR-LSAT 上：** - 无 Pruning：45.13% - 有 Pruning：78.43% - **差值：33.30%** 这告诉我们什么？ **LLM 能生成大量"看起来对"的代码，但其中大部分是语义上的谎言**。 如果不加 Pruning，直接聚合这些谎言，结果比 Chain-of-Thought 还烂（45% vs 35%）。但一旦用良定义性标准过滤掉矛盾的和模糊的，幸存下来的代码质量高得惊人。 用论文的诊断指标来说： - **ExecRate（执行率）**：Pruning 大幅降低——因为很多路径被判定为矛盾或模糊，连执行结果都不计入 - **Acc@Exec（可执行程序中的准确率）**：Pruning 大幅提升——因为被剪掉的恰恰是那些"能跑但错"的程序 这就像一群人投票。如果不加筛选，让所有人（包括醉酒的人和恶意的人）都投票，结果可能很差。但如果先筛掉"明显不靠谱"的人，剩下的人的共识质量会好得多。 --- ## 七、核心洞察：不是更大，是更对 D&P 的框架揭示了一个被业界长期忽视的真理： > **在逻辑推理领域，盲目扩大模型参数的收益，远不如在推理阶段投入计算资源的收益**。 ### 训练期计算 vs. 推理期计算（Test-Time Compute） | 维度 | 训练期计算（Scaling） | 推理期计算（D&P） | |------|---------------------|-------------------| | **目标** | 让模型"见多识广" | 让模型"多角度思考" | | **方式** | 堆数据、堆参数 | 一次生成多个计划、多路径验证 | | **瓶颈** | 高质量逻辑数据稀缺 | 计算成本可控，且不需要额外数据 | | **效果上限** | 逻辑推理没有"经验"可言 | 符号验证保证正确性 | D&P 是 inference-time framework—— **零额外训练**。它不改变模型权重，不改变训练数据，只是在推理时多花一点计算（生成 20 个计划，分别验证）。这种"Test-Time Compute"的思路，和 OpenAI 的 o1/o3 系列、DeepSeek 的推理模型是同一方向的。 但 D&P 比单纯的"多采样"更聪明： - **Diversity by Planning**：不是随机采样 20 个答案，而是让 LLM 在"计划层"发散——每个计划是一个不同的解题思路 - **Verification by Solver**：不是让 LLM 自己判断哪个答案对，而是用 Z3 的数学严格性来判定 - **Aggregation by Well-definedness**：不是看"答案是什么"，而是看"问题是否被正确翻译"——这是元层面的验证 --- ## 八、一个费曼式的直觉解释 想象你在教一个聪明但马虎的学生做几何证明题。 **传统方法（Chain-of-Thought）**： > 你让他写步骤，然后他写了一大段，看起来很自信。你一看，第 3 步用了"显然"这个词——但那个"显然"其实不显然，是错的。你已经看到了最后，没法回头了。 **Logic-LM（早期 AF）**： > 你让他把题翻译成几何画板的指令。他翻译了，但漏了"等边三角形"里的"等边"两个字。几何画板跑出了一个漂亮的图，但图对应的是另一个问题。你以为是正确的，其实是错的。 **D&P**： > 你说："别急着写步骤。先给我三个不同的解题思路。"他给了三个：一个是辅助线法，一个是反证法，一个是坐标法。然后你让他把每个思路都写成几何画板代码。你运行每一个代码，但你不直接看答案——你先检查"这个代码描述的问题是否有唯一解"。如果某个代码跑出了两个可能的答案（模糊），或者跑出了矛盾（无解），你直接扔掉。最后看剩下那些"有且仅有一个解"的答案里，多数人投的是什么。 这就是 D&P。它不假设 LLM 是可靠的翻译官。它假设 LLM 是一个 **有创造力但不可靠的头脑风暴者** ——能产生很多想法，但很多想法是错的。所以需要一个 **冷酷的、不会疲劳的、数学上可靠的验证官** 来筛选。 --- ## 九、局限与未来 ### 局限一：领域依赖 D&P 目前只在"可以被形式化为逻辑程序"的领域有效。数学证明、逻辑推理、约束满足——这些领域有成熟的符号求解器（Z3、Prover9、Isabelle）。但对于 **常识推理**（"如果我把冰箱门打开，房间会降温吗？"）、**因果推理**（"吸烟导致肺癌还是肺癌导致吸烟？"）、**开放域问答**（"特朗普的最新政策是什么？"），目前还没有通用的形式化语言。 ### 局限二：形式化瓶颈 Auto-formalization 本身是一个 AI-complete 问题——要让 LLM 把自然语言完美翻译成形式语言，理论上需要的理解能力和直接做推理是一样的。D&P 通过"多计划 + 验证"来缓解，但没有从根本上解决这个问题。如果 LLM 连"有哪些计划"都想不到，Draft 阶段就失败了。 ### 局限三：计算成本 20 个路径 × 每路径一次 LLM 调用 + 20 次 Z3 求解。这比单次 CoT 贵得多。但论文没有给出具体成本数据。在实际部署中，这可能需要自适应采样——简单的题少采样，难的题多采样。 ### 未来方向 1. **自适应 Draft**：根据问题难度动态调整路径数 k，简单题 k=5，难题 k=50 2. **跨领域形式化**：将 D&P 扩展到数学定理证明（Lean/Isabelle）、程序验证（Dafny）、物理模拟 3. **与推理模型结合**：o1/o3 的"思考链"本身就是 Draft 的一种形式，和 D&P 的"多计划"可以结合 4. **良定义性的扩展**：当前只检查|Si|=1，未来可以引入更丰富的语义一致性检查 --- ## 十、结语：概率与真理的分界线 Draft-and-Prune 不是治愈 LLM 幻觉的灵丹妙药。它是 **接受 LLM 本性后的务实工程**。 LLM 的幻觉不是 bug。它是 **概率生成模型的内生属性**。当你用千亿参数去拟合人类语言的统计分布时，"编造"和"创造"的边界本身就是模糊的。LLM 写十四行诗时，那种"幻觉"我们称之为想象力。 问题不在于 LLM 有幻觉。问题在于 **我们在用错误的工具做错误的事**。让一个"听起来合理"的模型去处理"必须绝对正确"的任务，就像让画家去当法官——他不是不够聪明，是他的训练方向不对。 D&P 的启示是：**未来的 AI 系统不是单一的模型，而是复合体**。 神经网络负责创造力、直觉、模式识别。符号系统负责严谨性、验证、数学保证。两者分工，而非替代。 **真正的智能不是"看起来像人"，而是"知道什么时候该像人，什么时候该像机器"**。 当 LLM 在写诗时，让它像人一样自由。当它在证明定理时，让它像机器一样严格。 Draft-and-Prune 画的这条线，可能比我们想象的更重要。 --- *参考资料：* - *Ni, Z., Liang, Z., Song, L., Cao, C., Zhang, X., Sangiovanni-Vincentelli, A., & Nuzzo, P. (2026). Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning. arXiv:2603.17233.* - *GitHub: https://github.com/zyni2001/draft-and-prune* - *Microsoft Research: https://www.microsoft.com/en-us/research/publication/draft-and-prune-improving-the-reliability-of-auto-formalization-for-logical-reasoning* #DraftAndPrune #AutoFormalization #NeuroSymbolic #LogicalReasoning #LLMHallucination #TestTimeCompute #Z3 #UCBerkeley #Microsoft #硬核拆解 #小凯 #硬核拆解 #DraftAndPrune #AutoFormalization #NeuroSymbolic #LogicalReasoning #LLMHallucination #TestTimeCompute #Z3 #UCBerkeley #Microsoft #小凯