AXIOM：一种信任优先的神经符号执行架构，用于可验证的数学推理

# 一种信任优先的神经符号执行架构，用于可验证的数学推理  
来源: https://arxiv.org/html/2606.00671  

###### 摘要  

我们提出 **AXIOM**，一种面向自然语言数学推理的信任优先神经符号执行架构。在 AXIOM 中，语言模型严格充当*规范化器*：它将非正式问题文本重写为狭窄的模式，由确定性的计算机代数系统（CAS）管道消耗，该管道推导并验证答案，或者将弃权作为一等输出。路由遵循问题形状正则表达式、模式特定提示词和封闭形式 CAS 处理器之间的 1:1:1 对齐，目前已部署 3,100+ 条此类路由，并且在 250+ 次连续发布提交中实现了零 lost_correct 回归。我们在 4 个 MATH 类别上报告实证结果：累积正确率为 94.36%（2,592 / 2,747），可解析输入的信任度为 100.00%（整个 2,747 条记录基准测试中零自信错误答案），所有四个领域均高于每个领域的 70/90/70 下限，每个领域可解析输入的信任度为 100.0%，仅规则处理器的中位延迟为 1 毫秒（占 lm-eval 算术 20,000 条记录基准测试的 88%）。该架构已通过公开部署服务了约 30,000 次生产查询。我们强调的贡献并非最终准确率数字，而是该架构建立的*正向动态*：生产中的每条记录弃权在经历一个发布周期后都有可能变为正确，因为新任务组合时不会对注册表造成回归。实现这一属性的操作纪律——数学模板分桶、lost_correct 扫描作为回归预言机、可解析优先注册、以及弃权作为一等输出——构成了一个超越数学领域的可迁移可信神经符号系统框架。  

---

## 1 引言  

#### 不可验证的 LLM 数学问题  

前沿大语言模型在数学推理基准测试上取得了令人印象深刻的准确率，但它们没有暴露验证路径：在 API 层面，一个自信的错误答案与一个自信的正确答案无法区分。用户没有结构性的手段来判断某个输出是否可靠。这不是某个特定模型的缺陷——这是**提示词-文本-输出**接口本身的结构性问题。  

两种现有的替代方案部分解决了验证问题，但代价是严重限制了输入范围。基于 Lean 的证明器配合 LLM 协作者 [11, 1] 可以针对 Lean 内核验证每条策略，但需要问题事先用 Lean 语法形式化——形式化本身是自然语言查询的瓶颈。封闭专家系统如 Wolfram Alpha [12] 可以用丰富的符号后端回答自然语言输入，但它们的推导轨迹不可检查，并且系统在输入边界未使用 LLM 增强。  

#### 信任优先 vs. 准确率优先  

我们将*信任*定义为 1 - 错误数/尝试数，其中*错误*不包括系统明确返回“未知”的记录。信任不同于*准确率*（正确数/总数）：一个拒绝不安全问题的系统可以在中等准确率下拥有极高的信任。我们的立场是，*自信错误是数学推理中最糟糕的失败模式*，架构设计应当使自信错误在结构上罕见，而不是事后被基准测试惩罚。  

#### 自底向上的架构承诺  

AXIOM 基于信任优先立场做出了四个设计选择：(a) 语言模型充当*规范化器*，将自然语言输入重写为狭窄的特定任务模式，绝不作为求解器；(b) 确定的 CAS 管道推导每个发出的答案；(c) LLM 与 CAS 管道之间的路由是模板对齐的：每条路由任务是一个 ⟨触发器, 提示词, 处理器⟩ 三元组，针对同一个数学模板共同设计；(d) *弃权*是一种一等结构性输出，由三个独立通道（无模板匹配、LLM 未知、处理器无法推导）中的任何一个发出。这种组合产生了一个运行时信任保证，这是单体 LLM 系统或预形式化证明器都无法提供的。  

#### 贡献  

- • **架构**（第 2 节）：一个 1:1:1 ⟨触发器, 提示词, 处理器⟩ 路由架构，一个用于多步骤形状的算子管道链框架，以及用于封闭形式裸算术的仅规则 LLM 旁路。我们在撰写本文时已交付 3,100+ 个任务三元组和 5 个链任务。  
- • **实证评估**（第 3 节）：可解析输入上 94.36% 的累计正确率（2,592 / 2,747），信任度为 100.00%（整个基准测试中零自信错误答案），所有 4 个 MATH 类别（代数、数论、计数与概率、预微积分）均高于 70/90/70 的每个领域下限，并且每个领域可解析输入的信任度均为 100.0%。仅规则路径在 20,000 条记录的 lm-eval-harness 算术套件上达到 100% 正确率。该架构已通过公开部署服务了约 30,000 次生产查询。  
- • **操作原则**（第 4 节）：四个可超越数学领域迁移的原则——数学模板分桶、LOST_CORRECT 扫描作为回归预言机、谓词未识别必须弃权、可解析优先注册与按领域设定的信任下限——每个原则均通过在 250+ 次发布周期中的直接实证观察得到验证。  

#### 可复现性  

该架构的一个实时、公开可访问的部署运行在 https://huggingface.co/spaces/Squagghy/axiom-solver。单查询视图（图 1）展示了每条记录上的 1:1:1 对齐以及弃权通道的结构可见性；累计仪表板（图 2）展示了第 3 节中引用的生产统计数据。  

---

**图 1：生产演示中对“计算 x²+y² 的值，其中 x=3，y=5”的单查询追踪。** 四个暴露的阶段（路由器 / 翻译器 / 处理器 / 答案）实现了第 2.1 节中的 1:1:1 对齐：路由器和处理器引用同一个“数值表达式求值”模板，翻译器块展示了逐字的 LLM 规范重写（Compute 3**2 + 5**2），并带有明确的幻觉警告。最终答案报告了每次查询的成本（1,755 个 token ≈ 0.00035 美元，以 Together.ai 0.18 美元/百万 token 计；第 3.5 节）。三个弃权通道（路由器未命中、LLM 未知、处理器弃权）中的任何一个都会在发出它的阶段变得可见。  

**图 2：生产部署的累计仪表板。** 第一行：主要计数器（总查询数、已回答数、弃权数、回答率）。中间行：结构正确性信号（路由率约 97%；p95 延迟约 865 毫秒，主要由 LLM 绑定的流量主导）。底部行：效率汇总，确认了第 3.5 节中每次查询的占用（LLM 绑定查询、平均每个查询的 token 数、总 token 数、推理成本估算为 token 数 × Together.ai 0.18 美元/百万 token）。下方的实时活动日志将仪表板锚定到真实的自由形式用户流量——每条条目是一个查询，带有每次记录延迟和路由任务。  

---

## 2 架构  

该架构将第 1 节中的信任优先立场实现为一条确定的执行路径：一个问题形状的正则表达式恰好选择一个任务，语言模型将输入重写为该任务的狭窄模式，一个封闭形式的 CAS 处理器推导并验证答案，或者通过结构化的失败原因弃权。我们下面列举的四个设计选择每个都是针对提示词-文本-输出接口的特定失败模式而提出的——1:1:1 任务路由对齐（第 2.1 节）、弃权作为一等输出（第 2.2 节）、用于多步骤形状的组合任务链框架（第 2.3 节），以及仅规则路径（第 2.4 节），该路径在数学模板纯形状上完全绕过 LLM。图 3 总结了单次查询的执行路径。  

**问题文本（自然语言） → 路由器（正则表达式，O(1)） → LLM 重写器（规范化器） → 处理器（CAS，确定性） → 答案 或 未知（任务模式，rule_only=True）**  

**图 3：AXIOM 管道。** 路由器每个查询恰好选择一个任务（对问题形状进行正则表达式匹配，O(1)）。LLM 将输入重写为任务特定的模式；处理器通过 SymPy 确定性地推导和验证答案。rule_only=True 路径对于数学模板纯形状（例如裸算术；占 lm-eval 算术记录的 88%）绕过 LLM。  

### 2.1 1:1:1 任务路由对齐  

AXIOM 中的路由不同于 LLM 增强数学推理中两种流行的模式：“一个模型端到端发出答案”（前沿单体系统）和“LLM 重写为单一结构化形式，然后通用 CAS 处理器消费它”（早期混合系统）。相反，我们覆盖的每一个问题形状都被雕琢成一个三元组：(a) 一个正则表达式触发器，(b) 一个提示词，其少样本示例教授特定于该形状的模式，(c) 一个确定性处理器，仅消费该模式。这三个组件是共同设计的，使得触发器恰好触发那些提示词能够产生规范形式且处理器能够验证答案的形状。我们称此为**1:1:1 对齐不变性**：一个触发器、一个提示词、一个处理器。  

该不变性在两个意义上承载着负载。首先，*信任归因成为局部问题*：路由到任务 T 并产生答案的记录严格通过 T 的代码路径可验证；没有跨任务涌现行为。其次，*注册表增长是线性可加的*：添加任务 T_{N+1} 不会回归任务 T_{1..N}，因为它们的代码路径通过构造是不相交的（不重叠的触发器、隔离的处理器）。在撰写本文时已交付的 N=1,600+ 个任务三元组中，lost_correct 回归在 250+ 次连续发布提交中累计为零。针对归档的 benchJSON 文件运行的预提交迁移扫描充当回归预言机：任何会抢走之前正确记录并产生更差结果的触发器扩大或新任务都会在提交前被捕获（参见第 4 节，原则 #1）。这与单体 LLM 作为求解器系统形成刻意对比，在后者的系统中，每个新能力与所有现有能力共享表示预算，添加能力 N+1 隐式地与 1..N 竞争提示空间、注意力和检索相关性。  

### 2.2 弃权作为一等输出  

在 AXIOM 中，answer=null 的响应在结构上不同于 answer=value 的响应。三个独立通道提供相同的 null：  

1. **路由器未命中**：没有任务的触发器正则表达式匹配问题文本。系统没有模板对齐的解释。记录为 fail_reason=no_task。  
2. **翻译器弃权**：LLM 通过任务提示词中的专用少样本示例返回 unknown。该提示词教导模型识别其重写何时会是猜测。  
3. **处理器弃权**：LLM 产生了规范形式且正则表达式匹配，但确定性 CAS 管道无法推导出经过验证的答案（例如，sp.solve 返回了 ConditionSet，谓词值无法识别，多个解分支需要消歧）。  

图 4 可视化了四个出口。每个通道都是一个结构化的、可被遥测可见的信号，而不是抛出的异常或自信错误的降级。当追踪跨越公共 API 边界时，我们剥离内部任务名称和失败原因，但保留每个阶段的结果（路由器*匹配*、翻译器*弃权*、处理器*跳过*），以便演示 UI 可以渲染哪个子系统拒绝回答。  

**路由器（正则表达式） → LLM 重写器 → 处理器（CAS） → 答案**  
**弃权：否（no_task 路由器未命中; rewrite_abstain LLM未知; handler_abstain 无法推导; {answer: null, abstained: true, fail_reason: ...}）**  
**匹配 → 规范形式 → 已验证 → 答案**  

**图 4：弃权作为一等结构化输出。** 三个管道阶段各自有一个独立的弃权通道（虚线、红色）；当任何一个触发时，公共 API 响应携带一个结构化的 fail_reason 指明阶段。承诺答案路径（顶部、绿色）仅在三个阶段全部成功时采用。这种四出口结构是 AXIOM 信任属性的架构基础：自信错误仅在处理器验证了错误规范形式时发出，永远不会作为静默降级出现。  

这一设计背后的纪律通过在生产部署中遇到的真实 bug 得以说明（30,000 次查询）。一个概率处理器计算了公平骰子上 P(rolling > 4)。LLM 正确产生了 predicate=greater_than_4，但处理器的谓词分发器没有 greater_than_* 家族的分支，静默地降级到默认计数 0 个匹配结果，发出了自信错误答案“0”（期望 1/3）。架构修复是一个白名单守卫：枚举处理器识别的谓词类型，在遇到任何未知谓词时返回 None（处理器弃权），而不是继续使用看起来像合法计数的默认值。这种模式是架构所能产生的最坏失败模式的结构性防御：*谓词未识别必须弃权，绝不可默认为零*。我们在第 4 节中作为原则 #2 讨论泛化。  

### 2.3 组合任务链框架  

某些形状需要在 LLM 提取结构后进行多步确定性计算。一个典型例子是分段函数 f，在多个分支上求值 f(x)=c，然后聚合（例如，*所有解之和*）。这自然分解为三个确定性步骤——解析分段、求解每个分支、聚合实数解——但原子化的 1:1:1 模式无法在不将求解器和聚合器内联到一个单体处理器中的情况下表示它。我们通过 ComposedTask 扩展框架：LLM 的结构化规范形式被一个 Operator 管道消费。每个 Operator 是一个纯函数 ctx ↦ ctx，带有声明的 requires 和 produces 类型集合。注册时的验证强制每个算子所需的键由某个上游算子产生，在定义时而非运行时捕获缺失依赖关系。算子确定性地链接；任何步骤的失败都会中止并返回干净的弃权。关键在于，LLM 调用每条记录恰好发生一次（第一个“初始提取器”算子）——我们不在链中迭代模型。五个 ComposedTask 已在生产中交付，涵盖了上述的分段求解+聚合以及四个*数论*多步形状（计数后取模、从方程求基数、模两变量求值、三约束中国剩余定理）。