🤖 AI

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

本文介绍了 Theoria，一种通过将解决方案重写为具有显式理由的可审计、类型化状态转换来增强 AI 回答可信度的验证架构，该架构在检测隐藏前提和虚假引用方面优于整体式 LLM 评判器，同时在专家级问题上保持了高精确度。

原作者： Ben Slivinski, Michael Saldivar

发布于 2026-07-02

📖 1 分钟阅读☕ 轻松阅读

原作者： Ben Slivinski, Michael Saldivar

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在雇佣一位才华横溢但有时过于自负的建筑师来设计一座桥梁。你不仅想要最终的蓝图，你还需要知道每一根梁柱为什么被安置在那里。如果建筑师说：“这根梁放在这里是因为感觉是对的，”你无法信任这座桥。但如果他说：“这根梁放在这里是因为定律 X，并且这是证明它的计算过程，”你就可以去核对数学逻辑。

这正是 Theoria 为人工智能解决的问题。

问题所在：两种有缺陷的信任方式

目前，我们有两种检查 AI 回答是否优秀的方法，但两者都有漏洞：

“数学家”法（形式化证明助手）： 这就像雇佣了一个只说严谨、不可破坏的数学代码的机器人。它很完美，但它只能理解那些已经被翻译成该代码的问题。而现实世界中的大多数问题（如法律论证或科学理论）是混乱且非形式化的，所以机器人无法理解它们。
“直觉”法（标量评判器）： 这就像让一个人阅读 AI 的文章并给出一个 1 到 10 的评分。它涵盖范围很广，但这个分数是一个黑盒。你不知道它为什么得了 7 分。它是遗漏了某个隐藏的假设？还是伪造了引用？你只得到了一个数字，而且你无法对其进行后期审计。

解决方案：“状态重写”侦探

Theoria 引入了第三种方法。它不要求 AI 写一篇长篇大论，也不要求将一切翻译成数学代码，而是强制 AI 将其答案重写为一个逐步的状态变更日志。

把它想象成一个关于推理的视频游戏存档文件或版本控制系统（类似于 Git）。

设置： AI 从“状态 0”（问题陈述）开始。
动作： 为了得到答案，AI 必须做出向“状态 1”的移动，然后是“状态 2”，以此类推。
规则： 对于每一次移动，AI 必须提供一张票据（理由）。票据只能是以下三种类型之一：
1. 引用： “我正在使用定理 X。”
2. 计算： “我做了计算：2+2=4。”
3. 既定事实： “题目告诉了我这一点。”

核心奥秘：“变更完备性”

这是其中的精髓所在。Theoria 有一个严格的规则：状态 A 到状态 B 之间的每一次变化都必须由票据进行解释。

如果 AI 试图偷偷塞入一个隐藏假设（比如“假设这座桥是用黄金做的”），而没有提供票据，系统就会抓到它。这个“变化”（添加黄金假设）会出现在日志中，但票据（理由）并没有覆盖这一变化。系统会尖叫道：“等等！你改变了状态，但你没给我们看收据！”

这迫使 AI 保持诚实。它无法在长篇大论的文本中隐藏谎言；它必须展示谎言进入对话的具体时刻。

实际运作流程

求解器（The Solver）： 一个 AI 尝试解决问题。
形式化器（The Formalizer）： 第二个 AI 将该解法重写为上述的“状态变更日志”。如果求解器在逻辑上跳跃了，形式化器必须将其记录为一个特定的步骤。
评判员（The Judges）： 专门的 AI 审计员会对每个步骤进行检查。
- “数学评判员” 检查计算是否正确。
- “引用评判员” 检查所引用的定理是否真实存在且适用。
- “事实评判员” 检查该事实是否确实存在于原始问题中。
裁决（The Verdict）： 如果每一步都有有效的票据，则答案被认证（Certified）。如果哪怕只有一个步骤缺失票据或票据造假，则答案被拒绝（Declined）。

研究发现

作者在处理难题（如专家级考试中的题目）时测试了该系统，发现：

高信任度： 当 Theoria 说一个答案是正确时，它的正确率高达 91.4%。
更擅长识破狡猾的谎言： 当 AI 试图隐藏前提（隐藏假设）或伪造引用时，Theoria 能在 90.6% 的情况下将其抓获。而标准的“直觉型”评判员只能抓到 62.5%。
并非万能于数学错误： 如果 AI 只是单纯算错了数学（比如说 2+2=5），Theoria 和标准评判员捕捉错误的能力差不多。Theoria 的特殊优势在于专门针对捕捉隐藏逻辑和伪造来源。
互补性： Theoria 和标准评判员在失败的问题类型上是不同的。如果你同时使用两者，你可以捕捉到几乎所有的错误。

总结

Theoria 并不试图让 AI 变得更聪明，它试图让 AI 的推理过程可审计。

它将模糊、不可靠的文章变成了一份透明的变更账本。它并不承诺每一个答案都是正确的（因为它会拒绝约 43% 的答案，因为无法验证它们），但对于它所批准的答案，你可以查看收据，核对数学逻辑，并确切知道为什么可以安全地信任它。

在这个 AI 可能会产生幻觉事实的世界里，Theoria 是那个会说：“给我看每一步的收据，否则我不签字。”

技术摘要：Theoria —— 非形式化推理状态下的重写-可接受性验证

1. 问题陈述

本文探讨了 AI 推理中的“信任问题”：即如何区分 AI 生成的答案何时应当产生合理的信任，特别是在安全关键领域（科学、法律、金融、医学）。目前的方案面临两难境地：

形式化证明辅助工具（如 Lean, Coq）： 提供数学上的确定性，但由于将非形式化、自然语言需求进行自动形式化（autoformalizing）的成本极高且具有语义脆弱性，因此无法覆盖大多数问题分布。
标量 LLM 判别器（Scalar LLM Judges）： 提供广泛的覆盖范围，但其生成的评分是不透明且无法审计的，继承了 LLM 的连贯性问题，并且无法识别证明为何出错（例如：隐藏的前提或伪造的引用）。

核心挑战在于：如何在不要求完全形式化的前提下验证非形式化推理，同时确保错误（特别是未说明的假设和逻辑跳跃）是可见且可审计的。

2. 方法论：Theoria 架构

Theoria 引入了一种验证架构，将求解器的自然语言答案重写为证明见证（proof witness）：一个类型化状态转换的序列。

2.1 重写框架

Theoria 不将证明视为一段散文，而是将其分解为一个状态轨迹 $(S_0, S_1, \dots, S_n)$ 。

状态 ( $S_i$ )： 代表已确立的事实和当前目标的有序字符串列表。
转换（Transition）： 从 $S_{i-1}$ $S_{i - 1}$ 到 $S_i$ $S_{i}$ 的步骤由特定的**证明理由类型（justification type）**授权：
1. 引用（Citation）： 定理、定义或推理规则。
2. 计算（Computation）： 算术或符号操作。
3. 题目给定（Problem Given）： 题目文本中明确说明的事实。
变化完整性不变性（Completeness-of-Change Invariant）： $S_{i-1}$ 与 $S_i$ 之间的每一个语义差异都必须由所述的理由来解释。如果推导新状态需要某个前提，但该前提在之前的状态中不存在或未在理由中说明，则构成未经授权的突变（unlicensed mutation）。

2.2 验证流水线

系统在一个循环中运行：求解 $\to$ 形式化 $\to$ 判定 $\to$ 过滤 $\to$ 修复。

求解器（Solver）： 提出一个自然语言解法（工具增强型，例如网络搜索）。
形式化器（Formalizer）： 将解法重写为状态转换见证。它强制要求前提在使用前必须是显式的。
并行专业判别器（Parallel Specialized Judging）：
- 计算判别器： 从头开始重新计算步骤。
- 引用判别器： 根据特定的状态差异（state diff），验证所引用的定理是否存在及其适用性。
- 题目给定判别器： 检查事实是否与原始文本一致。
- 初始状态判别器： 审计 $S_0$ 以确保在起始阶段没有引入未经授权的前提。
- 所有判别器都采用对抗性提示（adversarially prompted），旨在发现错误而非确认合理性。
严苛性过滤器（Pedantry Filter）： 区分实质性错误与针对非正式符号或压缩方式的过度严苛。
惯例提升（Convention Lift）： 如果通过记录明确的假设可以解决拒绝问题，则允许系统接受符合标准且可引用的领域惯例的步骤。
认证或拒绝（Certify-or-Decline）： 系统输出一个二元决策。如果所有步骤均通过（或通过惯例提升得到解决），则答案被认证（Certified）。如果任何步骤失败且无法在界限内修复，则答案被拒绝（Declined）。

3. 核心贡献

本文的主要贡献不在于使用了多个模型或步骤检查（这些是常见的），而在于特定的**见证格式（witness format）**及其理论保证：

暴露保证（命题 4.4）： 变化完整性不变性将隐藏前提（全局推理缺口）转化为局部、可观察的未经授权的突变。隐藏的前提要么必须作为状态中的新元素出现（触发授权检查），要么违反不变性。这迫使错误浮出水面，以便被局部判别器检测。
错误类别预测（命题 4.5）： 该格式预测验证优势将集中在：
- 隐藏前提： 被暴露为未经授权的突变。
- 伪造引用： 由于证据被显式类型化并针对差异进行检查，因此会被暴露。
- 无优势： 算术错误和定理误用（定理存在但应用错误）在结构上相对于散文形式并无暴露优势，因为这类错误是语义层面的而非结构层面的。
失效分解： 本文区分了暴露失效（Exposure Failure）（格式隐藏了错误）和判别器失效（Judge Failure）（判别器漏掉了已暴露的错误）。Theoria 旨在最小化前者，将后者留作经验研究。

4. 实验结果

评估在 HLE-Verified Gold（185 个专家级问题）和 GPQA Diamond（65 个研究生水平科学问题）上进行。

4.1 HLE-Verified Gold 表现

认证精确度（Certified Precision）： 91.4% (96/105 正确)，95% Wilson 置信区间为 [84.5%, 95.4%]。
覆盖率（Coverage）： 56.8% (105/185 问题被认证)。
不对称性： 被拒绝的答案出错的可能性约为认证答案的 5.0 倍（错误率分别为 42.5% 和 8.6%）。
对比仅求解器（Solver-Only）： 一个网络增强型求解器在 100% 覆盖率下达到了 83.8% 的准确率。Theoria 的流水线过滤掉了大量错误，将认证桶中的错误率降低到了 8.6%。
对比整体判别器（Holistic Judges）： 整体 LLM 判别器（分配单一置信度分数）在匹配的覆盖率下达到了相当的精确度（92.4–93.3%）。然而，它们在不同的问题集上失败（Jaccard 指数 0.14–0.36），表明两者具有互补的错误覆盖能力。

4.2 对抗鲁棒性

在 95 个中毒证明（注入特定错误类型）的基准测试中：

整体检测率： Theoria 为 94.7% (90/95)，而整体判别器为 83.2% (79/95) ( $p = 0.0017$ )。
错误类别细节：
- 隐藏前提： Theoria 90.6% vs. 整体判别器 62.5% (差距 28 个百分点)。
- 伪造引用： Theoria 100% vs. 整体判别器 90%。
- 算术/定理误用： 两者表现一致（分别为 ~95% 和 ~93%），证实了本文的理论预测，即该格式对于此类错误类型不具备结构性优势。

4.3 分布外表现 (GPQA Diamond)

认证精确度： 97.1% (33/34)。
覆盖率： 52.3%。
在不同基准测试上的高精确度表明，“认证或拒绝”的边界是由推理的可形式化程度驱动的，而非特定基准测试的校准。

4.4 集成潜力

由于 Theoria 与整体判别器在失败的问题集上是互斥的，集成策略（例如多数投票）实现了 93.6% 的精确度与 58.9% 的覆盖率，优于任何单一方法。

5. 重要性与主张

本文声称 Theoria 提供了一种可扩展的监督机制，弥合了原始 LLM 输出与形式化验证之间的鸿沟。

可审计性： 与标量分数不同，Theoria 生成的是人类可读的证明轨迹，其中的每一步都可以被独立质疑。
结构性优势： 该系统并不依赖判别器从散文中重建证明。相反，它将验证任务简化为一个局部问题：“这个理由是否授权了这个特定的状态变化？”
互补性： 本文认为 Theoria 不是整体判别器的替代品，而是一种互补方法。错误集之间极低的 Jaccard 重叠表明，结合结构性不同的验证架构可以产生更高的可靠性。
局限性： 作者承认 Theoria 无法检测产生无观测状态突变的错误（例如对 $S_0$ 中问题陈述的微妙误解），且目前依赖 LLM 判别器而非形式化后端（如 Lean 或 SMT 求解器），尽管其设计旨在与这些工具兼容。

总之，Theoria 证明了通过在非形式化推理上强制执行变化完整性不变性，可以使隐藏的假设和伪造的证据浮出水面，而这些错误在标准的整体评估中往往会被漏掉，从而为 AI 生成推理的信任提供了一个严谨且可审计的边界。