何时应该信任人工智能系统'的答案?正式证明助理提供确定性，但无法达到大部分问题分布;标量法学硕士法官提供覆盖范围，但产生不透明的分数，无法事后审核，并且与任何法学硕士一样受到一致性问题的影响。我们提出了 Theoria, 一种验证架构来弥补这一差距。候选解决方案被重写为一系列类型化状态转换,，每个状态转换均由明确的理由, 许可，无论是引用, 计算, 还是给定问题的事实,，并且每个转换都是独立可审核的。基本的不变量是变化的完整性: 必须考虑连续证明状态之间的每个差异,，因此隐藏的前提会以未经许可的突变的形式出现，而不是默默地传递。在 HLE 验证黄金(185 纯文本专家问题), Theoria 证明 105 的严格精度为 91.4% (Wilson 95% CI [84.5%, 95.4%])。每项认证都会生成人类可读的证明跟踪，其中每个步骤都可以独立质疑。整体法学硕士法官在匹配的覆盖范围上达到了相当的精度，但在不同的问题上失败了(Jaccard 0.14-0.36),，使这些方法互补。在 15 个领域的 95 个对抗性中毒证明中，, 结构化法官的得分为 94.7%，而整体判断的得分为 83.2% (p= 0.0017)。总体 11.5 个 pp 的差距集中在隐藏前提 (90.6% 与 62.5%, 之间，有 28 pp 差异) 和捏造的引用 (100% 与 90%), 的错误类别，其中形式分析预测有优势; 在算术和定理误用错误, 上的性能是相同的，但没有预测到任何优势。在 GPQA Diamond (n= 65), 上认证的精度为 97.1% (Wilson CI [85.1%, 99.5%])。
When should an AI system的 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%]).
科目: 人工智能 (cs.AI); 计算和语言 (cs.CL); 机器学习 (cs.LG); 计算机科学逻辑 (cs.LO); 软件工程 (cs.SE)
Subjects: Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)