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

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States
arXiv cs.AI 2026年7月1日提交

背景

当前AI系统面临信任挑战：形式化证明助手（如Lean或Isabelle）能提供数学上的确定性，但仅覆盖问题分布的很小一部分；纯标量LLM裁判器覆盖范围广，但输出不透明的事后审计不可，易受幻觉和一致性问题干扰。如何在非正式推理状态下实现可验证、可审计的答案置信度，成为AI安全与可解释性研究的核心痛点。

核心内容

Theoria提出一种验证架构，旨在弥合形式证明与标量裁判器之间的差距。它将候选解决方案重写为一系列带类型的状态转移序列，每个转移均由显式证明（引用、计算或问题给定事实）授权，所有转移均可独立审计。

核心设计基于“变化完整性”（completeness of change）不变性：连续证明状态之间的每处差异都必须被明确说明，否则隐藏前提会以未授权的突变形式暴露而非悄然通过。Theoria将候选解转化为可审计的“重写可接受性”证明链，强制显式化推理过程。

在HLE-Verified Gold（185个纯文本专家问题）数据集上，Theoria以91.4%严格精度认证105个样本（Wilson 95% CI [84.5%, 95.4%]）。每一次认证均生成人类可读的证明轨迹，每个步骤均可独立质询。

与整体LLM裁判器相比，Theoria在匹配覆盖率下精度相当，但两者在不同问题上失败（Jaccard 0.14-0.36），形成互补优势。

在95个跨15个领域的对抗性污染证明数据集上，结构化裁判器（Theoria）检出94.7%，而整体裁判器仅检出83.2%（p=0.0017）。整体11.5个百分点差距主要集中在隐藏前提（90.6% vs 62.5%，28个百分点差异）和虚构引用（100% vs 90%），这正是形式分析预言的优势类别；在算术和定理误用错误上性能一致（未预测优势）。

在GPQA Diamond（n=65）上，认证精度为97.1%（Wilson CI [85.1%, 99.5%]）。

关键要点

• Theoria将候选解重写为带类型状态转移序列，每个转移由显式证明（引用/计算/事实）授权，可独立审计；
• 核心不变性为“变化完整性”：连续状态间每处差异必须明确说明，隐藏前提会被未授权突变暴露；
• HLE-Verified Gold（185个专家问题）：认证105个，严格精度91.4%（Wilson CI [84.5%, 95.4%]），每认证生成人类可读证明轨迹；
• 与整体LLM裁判器互补：Jaccard相似度0.14-0.36，失败问题不同；
• 对抗性数据集（95个/15域）：结构化裁判器检出94.7%（vs 83.2%，p=0.0017），优势主要在隐藏前提（+28 pp）和虚构引用（+10 pp）；
• GPQA Diamond（n=65）：认证精度97.1%（Wilson CI [85.1%, 99.5%]）。

意义与影响

Theoria代表了从“黑箱标量判断”向“可审计、重写可验证推理状态”的范式转变。它显著提升了AI答案的透明度与可信度，尤其在高风险领域（如科学推理、法律论证、数学证明）。通过强制显式化推理链与变化完整性，Theoria减少了隐藏前提和幻觉带来的风险，使AI系统从“可能出错”转向“随时可被独立挑战”。这一方法既补充了形式证明的精确性不足，又超越了纯LLM裁判器的可解释性短板，为构建更可靠的AI代理系统奠定了基础。未来，该架构有望在更广泛的非正式推理任务中推广，推动AI可解释性与安全标准的实质性进步。