一份关于"验证架构边界"的实验报告
日期：2026-08-18　模型：deepseek-chat　验证器：SymPy 1.14
所有原始数据与代码见 data/、logs/、src/ 目录，可完全复现
摘要
本文不是一个"我的系统比 baseline 强"的成功报告。本文是一个有完整实验链条支持的否定性结果：我们系统性地证明，在 deepseek-chat + 高中一元二次函数范围内，“分解→求解→验证→组合"的多智能体架构无法超越裸LLM的单次调用，并建立了8种失败模式的分类学和信任分层的设计原则。
八轮实验（5+5+20+2 题，三次完整重跑）的数据显示：系统准确率从 16/20 降至 13/20，而裸LLM baseline 恒为 20/20。防御机制（类型系统、终局验证、规则派生）消除了部分信任点，但引入了新的错误类型，且准确率方差大于防御的净效应。
本文的核心贡献是失败模式分类学：8种有数据实证的LLM多步推理失败模式，每种配有定义、实验证据、对策和当前状态。以及一个被数据支持的结论：在LLM已强的领域，“加验证器"不是免费午餐——验证增加了系统的错误点，却没有覆盖所有错误类型。
关键词：LLM验证、多智能体推理、否定性结果、失败模式分类学、信任分层
一、引言
1.1 直觉：为什么"分解+验证"看起来应该更好
人类解数学题的过程天然是模块化的：读题→拆解→分步求解→组合答案→检查。既然LLM会犯错，直觉上，给它加一个"裁判”（如SymPy符号引擎）来验证每一步，应该能减少错误。
这个直觉催生了无数"LLM+验证器"的架构尝试。但社区缺少一样东西：系统性的失败分析。大多数工作只展示成功案例，对失败案例轻描淡写。本文试图填补这个空白——用完整的实验链条，解剖一个"直观上应该更好"的架构为什么实际上更差。
1.2 本文贡献声明
本文的核心贡献不是"一个更好的数学解题系统”，而是：
一个被数据支持的否定性结果：在 deepseek-chat + 高中一元二次函数范围内，多智能体验证架构的准确率低于裸LLM（13~16/20 vs 20/20）。
8种失败模式的分类学：每种模式有定义、实验证据、对策和修复状态，形成可引用的框架。
信任分层的设计原则：LLM的每一步必须降级为"声明意图"，数学由确定性代码执行；验证规格必须锚定在不依赖LLM声明的地面真值上。
可复现的实验链条：全部数据、代码、审计脚本开源，八轮实验结果可独立验证。
1.3 相关工作
多智能体推理和LLM验证是活跃方向，但现有工作侧重成功案例：
Toolformer / Gorilla：LLM调用外部工具（计算器、API），但未系统分析工具验证的边界。
ReAct / Reflexion：LLM通过行动-观察循环自我修正，但"修正"依赖同一模型的另一次采样。
AlphaProof / Lean：形式化证明系统提供确定性裁判，但仅限于可形式化的数学领域。
本文的不同之处在于：我们不假设验证器是万能的，而是系统性地测量它在什么条件下失效。
二、架构设计
2.1 七层防御流程
plain
题目输入
│
▼
[1] 入口分类 LLM 输出数学血统权重 + 隐含约束（规则复核）
▼
[2] 拆解 LLM 拆成子任务（含权重、答案类型、验证方案、依赖关系）
▼
[3] 拆解自查 把拆解结果和原题一起发回 LLM 检查完备性
▼
[4] 逐个子任务 LLM 求解 → SymPy 验证（三态：PASS/FAIL/UNSURE）
│ FAIL → 反馈纠错（最多 3 次）→ 仍错 → 回溯重拆
▼
[5] 组合 LLM 按验证状态如实标注组装，输出结构化答案 {“answer”,“text”}
▼
[6] 终局验证 规则从题面派生规格，对最终答案集合抽样验证
│ FAIL → 修正循环（最多 2 次）→ 仍 FAIL → 诚实失败
▼
[7] 输出 答案 + 完整可信度标记（子任务验证状态、终局验证状态、answer_verified）
2.2 关键设计决策
三态裁判（PASS / FAIL / UNSURE）
验证器必须能弃权：看不懂就返回 UNSURE，不判错、不误杀。
PASS：通过（确定性符号计算 / 数值容差内）
FAIL：不通过（触发反馈纠错）
UNSURE：看不懂（标记待人工确认，流程继续）
为什么：SymPy 不是万能裁判。sin²x 与 1-cos²x 形式不同但相等，√3 与 1.732… 写法不同——裁判必须懂"语义等价"，也必须承认自己不会（弃权）。P4 的教训：裁判弃权时，组合器必须如实标注，不能声称已验证。
类型系统
拆解器为每个子任务声明答案类型（value/interval/point_set/union/inequality），验证器反查实际类型，不符 → FAIL 纠错。
为什么：P5 的"区间 [0,2] 被压缩成点集 {0,2}“是机械性篡改——类型系统把它变成编译错误。它防不了语义错误（并/交/补、case split 完备性），但把"机械篡改"从 LLM 自由写作中物理隔离。
终局验证 + 规格规则派生
组合器输出结构化答案后，用规则从题面派生的规格（区间/表达式/条件全部正则提取）对最终答案抽样验证：
集合内部点不满足条件 → FAIL（答案过宽，强证据）→ 修正循环 → 再验证
外部点全满足 → 提示可能过窄（弱证据，UNSURE 不误杀）
为什么：组合阶段的最终答案原本不在验证环内（P5/B 的失败根源）。且终局验证规格不能由 LLM 声明（模式 6：信任递归）——改为从题面规则提取后，#8 假 PASS 的"条件错"路径被消除。
已知边界：采样式验证无法发现漏掉的候选/内部空洞（模式 5）——完备性盲区 = 采样天花板 + 验证器极限的叠加，原理性开放。
诚实失败出口
子任务重试耗尽 → 回溯重拆（最多 2 轮）→ 仍失败 → 输出"卡在 XX 子任务”，不硬答
终局验证 FAIL 未修正 → 明确标记"最终答案不可信"
answer_verified 与 ok 严格分离：ok 只表示"流程走完"，不表示"答案已验证"
为什么：system_ok 与答案正确性零相关是实测实锤（5/5 全 true 但 2 题错）。诚实失败比自信地错更有价值。
2.3 设计权衡与防御映射

三、实验链条

关键观察：
防御的净效应为负（16 → 13）
方差（±1.5）大于防御效应
准确率主要受 LLM拆解随机性 支配，防御机制的影响在噪声范围内
3.4 关键案例深度剖析
案例 A：P1 —— 完备性盲区（模式5）
题目：已知二次函数 f(x) = x² − 2ax + a² − 1 在区间 [0,2] 上的最大值为 3，求实数 a 的所有可能值。
真答案：a = 0 或 a = 2。
系统的死法：拆解层只指定验证 f(0)=3 → a=2，压根没拆出对称的 f(2)=3 → a=0。裁判对"a=2 使 f(0)=3"判定 PASS——它判对了，但这个问题从没被问到。裁判无法发现它没被要求检查的东西。
教训：“每个候选都成立”（易）与"没有遗漏候选"（难）是两件事。这是验证的数学性质，不是bug。
案例 B：P5 / 新题 B —— 组合层篡改（模式4）
题目：已知二次函数 f(x) = x² − 2ax + a² − 1 在区间 [0,2] 上的最小值为 −1，求实数 a 的所有可能值。
真答案：0 ≤ a ≤ 2（整个区间）。
系统的死法：子任务全过（推理文本也对），但组合器写 boxed 答案时把"整个区间"缩成了"0或2"。而且就算把"0或2"拿去做终局验证，两个候选代回最小值都是 −1 ✓ 全过——“漏掉整个区间"对候选式验证天生隐形。
修复后：类型系统强制声明interval类型 + 终局验证检查内部点（a=1时f(1)=-1✓）。B题[-1,1]被当场FAIL→修正为[0,1]→PASS。
案例 C：#8 —— 信任递归（模式6）
题目：已知函数 f(x)=x²-2ax+2a 在区间 [0,2] 上的最小值为 -2，求实数 a 的值。
真答案：a=-1 或 a=3。
实验7（LLM声明终局验证）：系统给出错误答案a=1-√3 或 3，但终局验证PASS——因为LLM声明的final_check条件本身有误。裁判验证的是"LLM告诉它要验证的东西”。
实验8（规则派生终局验证）：终局验证规格从题面正则提取（不依赖LLM），错误答案被当场FAIL→修正未成功→诚实失败。
教训：只要验证规格还由LLM声明，裁判就永远差最后一层地面真值。
四、失败模式分类学（核心章节）
本项目的独立产出：一份有数据实证的失败模式清单。每个模式都有：定义 → 实验证据 → 对策 → 当前状态。
模式 1：自洽地错（内部自洽的假世界）
定义：错误答案有看似干净的推导路径，长着"标准答案的脸"——有封闭形式、因式分解、漂亮区间。任何不做计算验证的评审都无法怀疑。
证据：对抗实验里 LLM 生成的标准答案 3/5 是错的（P1 的 a=-1或3、P3 的 m<1或m>2、P5 的 a=0或2），每个都有完整推导路径；复盘 LLM 拿着它们把对的判错、把错的判对。
对策：标准答案必须先过 SymPy 审计再开跑。
状态：✅ 已制度化（audit_*.py，20/20 通过）。
模式 2：伪验证（语言空间声称验证）
定义：输出文本声称"经验证"，但验证器根本没干活（全 UNSURE）或验证对象不是最终答案。
证据：P4 三个子任务验证状态全 UNSURE，输出却写"经验证，这两个根均满足原方程"；system_ok 与答案正确性零相关（5/5 全 true 但 2 题答案错）。
对策：combiner 逐条标注验证状态，禁止把 UNSURE 说成已验证；system_ok 语义拆分出 answer_verified。
状态：✅ 已修复（combiner 诚实化）。
模式 3：拆解层污染
定义：拆解器（LLM）把错误公式或幻觉答案直接写进子任务描述/验证规格，后续全部"自洽地"顺着错。
证据：竞赛题 A，子任务把区间内差值公式错写成 (a-1)²（真值分段），子任务 4 把幻觉答案 {-5/6,3,13/6} 写进任务描述；3 个关键子任务全 UNSURE，裁判没兜住。
对策：拆解覆盖性检查（自查已实现，但对同类模型偏差无效）；终局验证兜底。
状态：⚠️ 部分缓解（终局验证可抓，拆解完备性仍开放）。
模式 4：组合层篡改
定义：子任务全对、推理文本全对，但组合器写最终答案时篡改逻辑（压缩、漏写、自相矛盾）。
证据：P5 推理"所有 0≤a≤2 都满足"但 boxed 写"0或2"；新题 B 推理对、终局写 [-1,1]。
对策：类型系统（跨类型转换报错）+ 终局验证（抽样）+ combiner 结构化输出。
状态：✅ 大部分修复（B 题 [-1,1] 被当场抓获并修正）。
模式 5：完备性盲区（最深）
定义：代入/抽样验证只能验证"找到的候选"，永远无法发现"漏掉的候选"。这是验证的性质，不是 bug。
证据：P1 系统找到 a=2 验证通过，永远不知道 a=0 被漏；#13 同理（漏解 a=0）；#15 区间答成点集，外部点探不到内部空洞。
对策：需要"声称集合 ≡ 原条件全解"的覆盖性证明——参数最值类的全解计算（solveset）本身不可行。
状态：❌ 原理性开放（采样天花板 + 验证器极限的叠加）。
模式 6：信任递归
定义：每一步都问"谁验证这一步"——若验证规格（条件、方程、区间）由 LLM 生成，裁判验证的是"LLM 告诉它要验证的东西"。
证据：#8 假 PASS（LLM 声明的 final_check 条件可能有误）；P3 第二轮 c=m²-4 穿透（验证器对错误前提验证通过）。
对策：验证规格从题面规则派生（确定性、不依赖 LLM）；LLM 声明仅兜底。
状态：✅ 规则派生已实现（覆盖参数集合类题目）。
模式 7：预测失败模式是编造的
定义：LLM 对"baseline 会怎么错"的预测是幻觉式归因——先编一个错误，再编一个"为什么犯这个错误"的故事。
证据：P1 预测"会得到 a=1±√2"，尝试所有合理错误路径均无法推出该值；对抗集预测 0/5 应验。
对策：预测必须可证伪，复盘必须对照实际数据而非预测自圆其说。
状态：✅ 方法论修正（补跑全量、SymPy 审计标准答案）。
模式 8：验证器极限（无免费午餐）
定义：封闭计算问题（方程、不等式、求导）有机器裁判；开放问题（证明、建模、应用题）没有。数学没有 AlphaGo 的免费裁判。
证据：#18 零点类条件无法用 min/max/diff 表达 → 假 FAIL（误杀正确答案）；证明/几何类题型全程无裁判。
对策：把"开放验证"翻译成"封闭计算"；翻译不成功就诚实标记 UNSURE。
状态：⚠️ 架构边界所在（可翻译性边界）。
分类学总表

五、根本原因分析
5.1 验证的性质：相对正确性 vs 绝对正确性
验证器验证的是：“在假设 H 下，结论 C 是否成立”。但 H 本身可能是错的。
P3 中 c=m²-4 是错的，验证器对错误前提"自洽地"判了 PASS。这是相对正确性（relative correctness），不是绝对正确性（absolute correctness）。相对正确性在数学上价值有限——一个自洽的错误体系可以无限推导。
5.2 信任递归：为什么验证规格不能由LLM声明
终局验证的规格如果由LLM生成，系统只是在推迟信任点——从"信任LLM的答案"变成"信任LLM的验证条件"。#8的假PASS证明：条件错了，裁判就对错答案盖了章。
规则派生消除了这一层信任递归（从题面确定性提取），但引入了新的限制：
覆盖有限（6/20题）
其余仍靠LLM兜底（信任递归残余）
5.3 不可能三角
在当前技术条件下（deepseek-chat + SymPy），通用性、准确性、可验证性三者最多取其二：

你不可能用同一个架构同时满足三者。
5.4 价值窗口的实证：在当前范围内为空
价值窗口 = {题 | LLM会错} ∩ {题 | SymPy能验}
从全部实验数据看：
LLM会错的题：在 deepseek-chat + 一元二次函数范围内，baseline 20/20 全对。LLM没有犯错。
SymPy能验的题：即使LLM做对了，验证器也只有40%的PASS率，60%UNSURE。
两个条件的交集：没有一道题是"LLM会错且SymPy能验"的。
六、对社区的启示
6.1 “加验证器"不是免费午餐
验证机制增加了系统的复杂度（7层流程、6种防御、34个裁判测试用例），却没有覆盖所有错误类型。每增加一个环节，系统的联合状态空间指数增长，出现最弱一环的概率随之增加。
6.2 多智能体系统的可靠性瓶颈在接口
系统的可靠性不是"人多力量大”，而是"链的强度取决于最弱一环，且环节越多，出现最弱一环的概率越高"。本系统的错误不在SymPy（裁判可靠），而在：
拆解层决定"验证什么"（可能不完整）
组合层写"最终答案"（可能篡改）
验证规格层声明"验证条件"（可能错误）
校准完美的裁判，不等于找到所有正确答案。
6.3 否定性结果的价值
在AI/ML领域，否定性结果很少被发表，但它们对社区的价值极大。本文的实验链条告诉所有想做"LLM+验证器"的人：在LLM已经很强的领域，验证层可能不仅不加分，反而因为信任递归和完备性盲区而减分。
6.4 信任分层思想的迁移
即使本架构在当前范围内不工作，其设计思想对其他领域仍有参考价值：
代码生成：规则派生测试用例，而非LLM声明测试条件
合同审查：规则派生合规检查点，而非LLM判断合规性
医疗诊断：规则派生禁忌症检查，而非LLM声明诊断标准
核心原则不变：LLM只做"声明"，确定性代码做"执行"，验证规格锚定在不依赖LLM的地面真值上。
七、局限与未来工作
7.1 实验范围限制
模型单一：仅测试 deepseek-chat，未覆盖 GPT-4o、Claude、 weaker models
题型单一：仅覆盖一元二次函数相关题（顶点、最值、判别式、零点），未覆盖数列、组合、证明
语言单一：仅中文题面
7.2 未测试的领域
MATH竞赛级题目：baseline可能真正会失败的地方，但可翻译性边界可能更窄
证明题：完全在SymPy能力范围外
应用题/建模题：需要自然语言到数学模型的翻译，误差空间更大
7.3 覆盖性证明的研究方向
完备性盲区（模式5）是原理性开放问题。一个可能的方向是：
对特定题型（如二次函数区间最值），人工证明"全解集合 = {端点, 极值点}“的覆盖性定理
将定理编码为验证规则，让系统能声明并验证"完备性”
代价是通用性丧失——每新增一种题型需要人工定理+编码
八、结论
我设计了一个对抗性实验想证明系统比 baseline 强，结果发现：
生成预测的 LLM、求解的 LLM、复盘的 LLM，全都因为缺少确定性裁判而自信地错——连"标准答案"都错了 3/5。
这个失败本身，实证了项目的核心主张：推理链上的每一层都必须挂接可验证的裁判，而裁判必须理解"完备性"而不只是"正确性"。
本文用八轮实验、27题、三次完整重跑的数据证明：在 deepseek-chat + 高中数学范围内，"分解→求解→验证→组合"的多智能体架构无法超越裸LLM。但失败不是终点——
我们建立了一套有数据实证的失败模式分类学，提出了信任分层的设计原则，并诚实地标出了架构的边界。
这比"我又加了一个补丁"更有价值。
附录

A. 20题完整测试集
见 data/problems_20.json（L1×7 / L2×7 / L3×6，标准答案全经SymPy审计）。
B. 逐题实验结果（三次运行对比）

C. 代码索引

D. 裁判单元测试结果
34/34通过，覆盖：
类型核查（4例）
终局验证（5例）
幻觉答案击穿（1例）
原有验证类型（24例：root/extreme/interval_extreme/equality/satisfies/inequality）
完整数据、代码、附录见仓库：https://github.com/1549080929-debug/math_agent
本文所有实验数据、代码、审计脚本均已开源，可独立复现。
作者声明：本文是一个否定性结果报告，系统准确率低于裸LLM。失败分类学和信任分层设计原则是独立产出。