Theoria: 非正式推理状态下的重写可接受性验证

# 基于非形式推理状态的重写可接受性验证
来源: https://arxiv.org/html/2607.01223
###### 摘要

何时应信任AI系统的答案？形式证明助手提供了确定性，但无法覆盖大部分问题分布；标量LLM评判器具有广泛的覆盖范围，但产生不透明的分数，事后无法审计，并且面临与任何LLM相同的连贯性问题。我们提出了Theoria，一种弥合这一差距的验证架构。候选解被重写为一系列有类型的状态转换，每一步都通过明确的理由（无论是引用、计算还是问题给定的事实）获得许可，并且每一次转换都可以独立审计。基础不变量是*变化完整性*：连续证明状态之间的每一个差异都必须被解释，因此隐藏的前提会作为未经许可的变异浮现出来，而不是悄然通过。

在HLE-Verified Gold（185个仅文本专家级问题）上，Theoria以91.4%的严格精度（Wilson 95% CI [84.5%, 95.4%]）认证了105个。每次认证都产生一个人类可读的证明轨迹，其中每一步都可以被独立挑战。整体性LLM评判器在匹配的覆盖率下达到了可比的精度，但在不同的问题上失败（Jaccard 0.14–0.36），使得这些方法具有互补性。在涵盖15个领域的95个对抗性中毒证明上，结构化评判器捕获了94.7%，而整体性评判器捕获了83.2%（p=0.0017p=0.0017）。总体11.5个百分点的差距集中在隐藏前提（90.6% vs. 62.5%，28个百分点的差异）和捏造引用（100% vs. 90%）上，这正是形式分析预测具有优势的错误类别；在算术和定理误用错误上性能相同，这些领域没有预测到优势。在GPQA Diamond（n=65n=65）上，认证精度为97.1%（Wilson CI [85.1%, 99.5%]）。

## 1 引言

推理验证不是让AI系统平均产生更多正确答案的问题。它是决定何时一个产生的答案应该产生合理信赖的问题。对于日常使用，一个合理的答案就足够了。对于科学发现、法律分析、金融建模、医疗决策支持、工程验证或任何其他“安全关键领域”，相关的对象不仅限于答案本身，还包括系统提议使该答案可用的步骤。一个仅仅提高平均准确率的验证器并没有解决信任问题。验证器必须划定一条界限：这些输出已经通过了具有已知失败表面的程序，而那些输出则没有。

如今，存在两种方法。一方面，形式方法将正确性视为核心属性。证明助手如Lean(Lean项目, (https://arxiv.org/html/2607.01223#bib.bib8))、Coq/Rocq(The Rocq Prover项目, (https://arxiv.org/html/2607.01223#bib.bib6))和Isabelle(Nipkow et al.,2002 (https://arxiv.org/html/2607.01223#bib.bib7))接受或拒绝证明项，现代AI系统通过将自然语言问题翻译成形式目标并搜索形式证明来利用这一点(Xin et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib9); Google DeepMind,2024 (https://arxiv.org/html/2607.01223#bib.bib10); Hubert et al.,2025 (https://arxiv.org/html/2607.01223#bib.bib11); Tsoukalas et al.,2026 (https://arxiv.org/html/2607.01223#bib.bib12); Achim et al.,2025 (https://arxiv.org/html/2607.01223#bib.bib13); Chen et al.,2026 (https://arxiv.org/html/2607.01223#bib.bib14))。一旦规范被完全形式化，形式验证会产生强有力的结果。然而，这种方法在必须解释非形式、自然语言需求时变得脆弱。当主要挑战在于确定哪个形式规范准确地反映了现实世界的问题时，验证内核可能会完美地证明一个不正确的定理。因此，自动化形式化的障碍不仅仅是当前工具的限制，而是一个基本的语义边界。

另一方面，标量奖励和评判器系统在普通的推理轨迹上运作，覆盖了更多的问题分布。过程奖励模型(Lightman et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib15); Wang et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib16); Yuan et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib17))提供了密集的训练信号，而LLM作为评判器的流水线(Zheng et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib18); Gu et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib19))扩展了定性评估。它们的弱点是分数不是“验证证书”。标量可以正确或错误，但不能像证明那样是完整或不完整的。LLM作为评判器的评估依赖于定性推理，继承了这些相同的逻辑脆弱性。它不记录使用了哪个前提，哪个转换被许可，或者是否有一个额外的假设悄然进入。

Theoria占据了这个空间的第三个点。它不将非形式推理翻译成Lean，也不要求LLM分配一个整体质量分数。相反，它将求解器的答案重写为一种见证，即一个初始状态和一系列状态到状态的转换。每个转换恰好携带一种理由类型：*引用*、*计算*或*问题给定的*。验证者询问所述的理由是否许可从前一个状态到下一个状态的整个变化。这是一个局部问题，并且与“结论是否成立？”不同。重写问题是：给定这个前状态、这个后状态、这个理由类型和这个证据，观察到的变化是否可以接受？

其思想是，一个精心选择的见证格式可以使验证者的易错性不那么具有破坏性。LLM评判器不被信任为预言机。它们被分配了受限的局部义务，针对一个显式的差异。证明见证被设计成使得最可能重要的错误——即假设、捏造引用、无根据的计算、静默的约定选择——必须作为状态的可见变化浮现出来，从而被对抗性评判器捕获。该架构不再依赖于评判器从散文中重构整个证明。这是*可扩展监督*的一个具体实例：系统产生结构化的产物，人类或下游审计员可以在可处理的粒度上进行检查，而无需从模糊的输出中重构潜在的推理。

第2 (https://arxiv.org/html/2607.01223#S2)–3 (https://arxiv.org/html/2607.01223#S3)节介绍了相关工作与重写框架。第4 (https://arxiv.org/html/2607.01223#S4)节阐述了重写见证的形式属性，包括隐藏前提的暴露保证以及关于哪些错误类别受益的可测试预测。第5 (https://arxiv.org/html/2607.01223#S5)–6 (https://arxiv.org/html/2607.01223#S6)节描述了架构和结构性论证。第7 (https://arxiv.org/html/2607.01223#S7)节讨论了校准。第8 (https://arxiv.org/html/2607.01223#S8)节报告了在HLE-Verified Gold上的实证评估，包括仅求解器的基线（第8.3 (https://arxiv.org/html/2607.01223#S8.SS3)节）、整体性评判器基线（第8.4 (https://arxiv.org/html/2607.01223#S8.SS4)节）、错误重叠分析（第8.5 (https://arxiv.org/html/2607.01223#S8.SS5)节）、跨模型裁决（第8.6 (https://arxiv.org/html/2607.01223#S8.SS6)节）、一个直接测试命题4.5预测的对抗性鲁棒性测试（第8.7 (https://arxiv.org/html/2607.01223#S8.SS7)节），以及在GPQA Diamond上的分布外评估（第8.8 (https://arxiv.org/html/2607.01223#S8.SS8)节）。

## 2 相关工作

Theoria位于三条先前工作线的交叉点。其贡献不在于使用多个模型、步骤检查或修复（这些想法相当常见）。其贡献在于具体的见证格式：在非形式推理上的状态重写，具有类型化的理由和变化完整性不变性。

#### 形式证明助手与自动化形式化。

Mizar(Bancerek et al.,2018 (https://arxiv.org/html/2607.01223#bib.bib5))、Coq/Rocq(The Rocq Prover项目, (https://arxiv.org/html/2607.01223#bib.bib6))、Isabelle/HOL(Nipkow et al.,2002 (https://arxiv.org/html/2607.01223#bib.bib7))和Lean(Lean项目, (https://arxiv.org/html/2607.01223#bib.bib8))提供了可信的内核，其中证明项要么通过检查，要么不通过。AI自动化形式化攻击了入门成本。DeepSeek-Prover(Xin et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib9))使用了大规模合成的Lean数据。AlphaProof(Google DeepMind,2024 (https://arxiv.org/html/2607.01223#bib.bib10); Hubert et al.,2025 (https://arxiv.org/html/2607.01223#bib.bib11))在奥赛级别将学习搜索与Lean验证结合起来。AlphaProof Nexus(Tsoukalas et al.,2026 (https://arxiv.org/html/2607.01223#bib.bib12))、Aristotle(Achim et al.,2025 (https://arxiv.org/html/2607.01223#bib.bib13))和AxiomProver(Chen et al.,2026 (https://arxiv.org/html/2607.01223#bib.bib14))扩展了形式化路径。这些系统有助于阐明Theoria的边界。Theoria是为问题保持非形式、正确的形式目标不明显、或形式化成本超过用例的场景而设计的。因为一个Theoria见证已经通过类型化的本地许可暴露了每个前提和状态变化，所以它比自由形式的散文更容易成为自动化形式化的目标。理论上，可以在下游附加一个形式证明器来完成可形式化的步骤。

#### 过程监督与学习验证。

Lightman等人(Lightman et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib15))表明过程监督在数学推理中优于结果监督。Math-Shepherd(Wang et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib16))自动构建过程级监督。隐式PRM(Yuan et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib17))从结果级数据中提取步骤级信号。ReST(Gulcehre et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib23))和ReST-MCTS*(Zhang et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib24))使用奖励信号来指导推理生成。这些系统将步骤视为评估的对象。不同之处在于返回的对象类型。PRM输出一个标量，可以指导采样、重新排序或强化学习，但它不跟踪前提之间的逻辑步骤，也不识别每个状态变化。标量奖励是策略优化所需要的，但它不能替代证明见证。

#### LLM作为评判器。

Zheng等人(Zheng et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib18))确立了LLM作为评判器作为一种可扩展的评估方法。文献记录了位置效应、冗长效应、自我增强和提示敏感性(Gu et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib19))。Theoria使用LLM评判器，但赋予它们更狭窄的角色：不是评估全局正确性，而是回答一个类型化的局部问题，关于一个被引用的理由是否许可一个特定的状态变化。

#### 结构化自然语言验证。

Ling等人(Ling et al.,2023 (https://arxiv.org/html/2607.01223#bib.bib20))将推理验证分解为逐步的子过程。MATH-VF(Zhou and Zhang,2025 (https://arxiv.org/html/2607.01223#bib.bib21))使用形式化器和批评家以及CAS工具。证明者-验证者博弈(Kirchner et al.,2024 (https://arxiv.org/html/2607.01223#bib.bib22))优化了较小验证者的可读性。SAVeR(Yuan et al.,2026 (https://arxiv.org/html/2607.01223#bib.bib27))和图结构化验证(Fang et al.,2025 (https://arxiv.org/html/2607.01223#bib.bib28))对中间信念状态进行建模。这些工作与Theoria对推理格式是验证的一部分的广泛直觉一致。Theoria在两个方面有所不同：(1) 它跟踪状态的变化而不是语句之间的逻辑步骤，以及 (2) 它使用少数操作标签，如引用、计算或问题给定，以保持指令简单和词汇无歧义。

## 3 重写框架

### 3.1 证明见证作为状态轨迹

一个Theoria证明见证由一个初始状态$S_0$和一个有限的步骤序列组成

$(S_1, \tau_1, e_1)$, $(S_2, \tau_2, e_2)$, $\dots$, $(S_n, \tau_n, e_n)$
每个状态$S_i$是一个有序的字符串列表，表示当前已经确定的内容以及仍需确定的内容。按照惯例，索引0保存正在求解的表达式：最初是一个目标变量（例如，“ANSWER = ?”），最终是解析出的答案。这种表示故意不如证明助手的核心语言那样形式化，并且比自由散文更受约束。它不是证明项，而是一个可以检查差异的状态对象。

一个步骤$(S_i, \tau_i, e_i)$是从状态$S_{i-1}$到状态$S_i$的转换，由类型为$\tau_i \in \{\texttt{citation}, \texttt{computation}, \texttt{problem\_given}\}$的证据$e_i$证明。验证者接收问题陈述和整个证明作为上下文，然后询问一个刻意局部的问题：类型为$\tau_i$的理由$e_i$是否许可从$S_{i-1}$到$S_i$的整个变化？

### 3.2 变化完整性不变性

令$\Delta(S_{i-1}, S_i)$表示一个步骤引入的实质性变化：添加的断言、移除的断言、加强的假设、实例化的参数、重写的表达式、改变的领域、改变的定义以及对答案槽的更改。令$L_{\tau}(e; S_{i-1}, P)$表示在前一状态$S_{i-1}$和问题$P$的上下文中，类型为$\tau$的证据$e$所许可的变化集。则重写可接受性条件是：

$\Delta(S_{i-1}, S_i) \subseteq L_{\tau}(e_i; S_{i-1}, P)$ (1)
并附加要求：应用该许可所需的所有前提都存在于$S_{i-1}$中，或由先前证明的步骤引入。

这就是*变化完整性不变性*。每一个变化都必须被解释。一个证明步骤并不仅仅因为新状态为真或可以从旧状态全局推导出来而可接受。只有当所述的理由解释了观察到的转换时，它才是可接受的。该不变性是一个关于证明状态变化的守恒定律。它防止前提静默地进入。在普通散文中，一个证明可以从“令$p$为一个奇素数”移动到“因此勒让德符号具有性质$X$”，同时静默地导入$p \nmid a$、一个关于最小剩余数的约定以及一个其假设仅部分满足的定理。在重写见证中，每个导入的条件必须要么存在于先前的状态中，要么作为$S_i$的一个新元素出现（在那里评判器可以询问引用是否许可它）。

### 3.3 理由类型

引用涵盖定理、恒等式、定义、定律和推理规则。被引用的结果必须存在，在当前状态下适用，并解释所有变化。它不能许可未声明的附加条件或比定理提供更强的结论。

计算涵盖算术、代数化简、符号操作、枚举和确定性运算。其主要义务是正确性。