Adnan KhanAdnanProduct & AI
San Francisco Bay Area
Get in touch

Source note3 min read

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

Source

arXiv

arxiv.org/abs/2607.01223v1

Read the source

Source

Plain-Language Brief

Theoria is a verification architecture presented by Ben Slivinski and Michael Saldivar that aims to address the issue of trust in AI systems' answers. It rewrites candidate solutions into a sequence of typed state transitions, each with an explicit justification. The system ensures completeness of change, making hidden premises surface as unlicensed mutations rather than passing silently. On HLE-Verified Gold (185 text-only expert problems), Theoria certifies 105 problems at 91.4% strict precision. It also performs better than holistic LLM judges on adversarial poisoned proofs and GPQA Diamond.

What the Document Says

  • Theoria is a verification architecture.
  • It rewrites candidate solutions into a sequence of typed state transitions, each licensed by an explicit justification.
  • Every transition is independently auditable.
  • The foundational invariant is completeness of change: every difference between consecutive proof states must be accounted for.
  • On HLE-Verified Gold (185 text-only expert problems), Theoria certifies 105 at 91.4% strict precision.
  • Every certification produces a human readable proof trace.
  • Holistic LLM judges achieve comparable precision at matched coverage but fail on different problems (Jaccard 0.14-0.36)
  • 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%)
  • Performance is identical on arithmetic and theorem-misapplication errors.

Key Concepts Mentioned

  • Theoria
  • Verification Architecture
  • AI Systems' Answers
  • Typed State Transitions
  • Explicit Justifications
  • HLE-Verified Gold
  • Holistic LLM Judges
  • Adversarial Poisoned Proofs
  • GPQA Diamond

Claims Made by the Document

  • Theoria closes the gap between formal proof assistants and scalar LLM judges.
  • Theoria certifies 105 problems at 91.4% strict precision on HLE-Verified Gold (185 text-only expert problems).
  • Holistic LLM judges achieve comparable precision but fail on different problems compared to Theoria.
  • Structured judges catch 94.7% versus 83.2% for holistic judging on adversarial poisoned proofs.
  • The overall performance gap concentrates in hidden premises and fabricated citations.
  • Performance is identical on arithmetic and theorem-misapplication errors.

Evidence Used

  • The text from the paper provides information about Theoria's design, its performance, and its comparison with holistic LLM judges.

Methods / Approach

  • Rewriting candidate solutions into a sequence of typed state transitions.
  • Ensuring completeness of change.
  • Independently auditing each transition.
  • Producing human readable proof traces.

Limitations Stated by the Authors

  • The paper does not discuss the computational complexity or scalability of Theoria.

Limitations Noted by the Agent

Agent interpretation — not from the source.

  • The agent may not fully understand the specific technical details and implications of Theoria, requiring further research to explore its limitations in more depth.

Open Questions

  • What is the computational complexity of Theoria?
  • How does Theoria perform on larger problem sets?
  • Are there any potential disadvantages or limitations to Theoria that have not been addressed in the paper?

Notes for Future Q&A

May include interpretation. Labeled where it does.

  • The paper focuses primarily on the design and performance of Theoria, with limited discussion on its potential drawbacks.

Raw Abstract / Excerpt

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%]).