Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

LLM Latent Reasoning HDCE KR / KRR Neural-Symbolic MTPLD
2026年07月01日
我们应于何时信任人工智能系统的答案？形式化证明助手虽能提供确定性保障，却无法覆盖大多数实际问题；而标量型大语言模型（LLM）评判器虽具备广泛覆盖能力，但其输出的评分缺乏透明度，事后无法审计，且同样受制于大语言模型固有的逻辑连贯性缺陷。为此，我们提出“Theoria”——一种填补上述鸿沟的验证架构。该架构将候选解重写为一系列带类型的“状态转移”序列，每一次转移均须由明确的依据予以授权，这些依据可以是文献引用、具体计算，或是题目本身所给定的事实；且每一次转移均可独立审计。其核心不变量是“变更完备性”：相邻两个证明状态之间的所有差异都必须得到充分解释；因此，任何隐含前提若未获显式授权，便会以“未授权的突变”形式暴露出来，而不会悄然通过。在HLE-Verified Gold数据集（包含185道纯文本、由领域专家编制的难题）上，Theoria成功认证了其中105道题目的解答，严格精确率达91.4%（威尔逊95%置信区间为[84.5%, 95.4%]）。每次认证均生成一份人类可读的证明轨迹，其中每一步推理均可被独立质疑与检验。相比之下，整体式大语言模型评判器在同等覆盖率下能达到相近的精确率，但其失效案例与Theoria高度互补（Jaccard相似系数仅为0.14–0.36），表明二者确属互补型方法。在涵盖15个领域的95个对抗性污染证明样本上，结构化评判器的检出率达94.7%，显著高于整体式评判器的83.2%（p = 0.0017）。这一总体11.5个百分点的性能差距主要集中于两类错误：一是隐含前提未被显式声明（结构化方法检出率90.6%，整体式方法仅62.5%，相差28个百分点）；二是虚构文献引用（结构化方法达100%，整体式方法为90%）——而这恰恰正是形式化分析所预判其具备优势的错误类型；而在算术计算错误和定理误用错误这两类未被预判具优势的错误上，两种方法表现则完全一致。在GPQA Diamond测试集（n = 65）上，经Theoria认证的解答精确率达97.1%（威尔逊95%置信区间为[85.1%, 99.5%]）。
When should an AI system's answer be trusted? Formal proof assistants offer certainty but cannot reach most of the problem distribution; scalar LLM judges offer coverage but produce opaque scores that cannot be audited after the fact and are subject to the same coherence issues as any LLM. We present Theoria, a verification architecture that closes this gap. A candidate solution is rewritten into a sequence of typed state transitions, each licensed by an explicit justification, whether that be a citation, computation, or problem-given fact, and every transition is independently auditable. The foundational invariant is completeness of change: every difference between consecutive proof states must be accounted for, so hidden premises surface as unlicensed mutations rather than passing silently. On HLE-Verified Gold (185 text-only expert problems), Theoria certifies 105 at 91.4% strict precision (Wilson 95% CI [84.5%, 95.4%]). Every certification produces a human readable proof trace in which each step can be independently challenged. Holistic LLM judges achieve comparable precision at matched coverage but fail on different problems (Jaccard 0.14-0.36), making the approaches complementary. On 95 adversarial poisoned proofs across 15 domains, structured judges catch 94.7% versus 83.2% for holistic judging (p= 0.0017). The overall 11.5 pp gap concentrates in hidden premises (90.6% vs. 62.5%, a 28 pp difference) and fabricated citations (100% vs. 90%), the error classes where the formal analysis predicts an advantage; performance is identical on arithmetic and theorem-misapplication errors, where no advantage is predicted. On GPQA Diamond (n= 65), certified precision is 97.1% (Wilson CI [85.1%, 99.5%]).
许愿