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

一句话判断

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 翻译：把这段话转成符号求解器能懂的程序

   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\) 是求解器执行后返回的可行假设集合
• \(|S_i| = 1\)：恰好有一个解。程序正确翻译了问题，且问题本身有唯一答案。保留。
• \(|S_i| = 0\)：无解。程序是 矛盾的——要么逻辑本身矛盾，要么翻译时遗漏了条件导致前提冲突。剪掉。
• |S_i| > 1：多解。程序是 模糊的——要么翻译时条件不足，要么量词范围搞错了。剪掉。

这个标准极其优雅：它不是说"答案对不对"（这需要 ground truth），而是说"这个程序描述的问题是否良定义"。一个良定义的逻辑问题必须有且只有一个解。如果程序生成的解不是 1 个，说明程序本身有问题——无论答案是啥。

Step 3: Aggregate（聚合）—— 多数投票定乾坤

幸存下来的路径（通过良定义性检查的）进行多数投票。如果 20 个路径中有 15 个说"答案是 A"，那么最终输出"A"。

五、实验数据：从 33% 到 82% 的跨越

四个基准测试，涵盖不同难度的逻辑推理：

AR-LSAT（法律逻辑推理——最难）

注意这个跳跃：从最强的 AF 基线 53% 跳到 D&P 的 78%，+25 个百分点。这不是渐进改良，这是断层式突破。

更关键的对比：没有 Pruning 的话，D&P 在 AR-LSAT 上只有 45.13%。Pruning 把它推到了 78.43% —— 贡献了 33 个百分点的提升。这意味着在 AR-LSAT 上，超过一半的路径生成的代码虽然能运行，但语义上是错的，被 Pruning 无情地剪掉了。

ProofWriter（证明生成）

从 92% 到 98%，接近天花板。

PrOntoQA（本体问答）& LogicalDeduction（逻辑演绎）

在 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）

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 #小凯