Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

Source

• Source name: arXiv
• Source kind: paper
• Authors / organization: Ben Slivinski, Michael Saldivar
• Venue: arXiv: cs.AI
• Published: 2026-07-01
• Collected: 2026-07-02
• URL: http://arxiv.org/abs/2607.01223v1
• PDF: https://arxiv.org/pdf/2607.01223v1
• DOI: UNKNOWN

Plain-Language Brief

Theoria is a verification architecture proposed by Ben Slivinski and Michael Saldivar that aims to close the gap between formal proof assistants and scalar LLM judges in determining when an AI system's answer can be trusted. Theoria works by rewriting candidate solutions into a sequence of typed state transitions, each with an explicit justification. This allows for independent auditing of each transition and the production of a human-readable proof trace. The authors claim that Theoria significantly outperforms holistic LLM judges on certain types of errors, particularly hidden premises and fabricated citations.

What the Document Says

• Theoria is a verification architecture
• It rewrites candidate solutions into a sequence of typed state transitions
• Each transition has an explicit justification
• Every transition is independently auditable
• The foundational invariant is completeness of change
• On HLE-Verified Gold, Theoria certifies 105 problems at 91.4% strict precision
• Each certification produces a human readable proof trace
• Holistic LLM judges achieve comparable precision but fail on different problems
• On adversarial poisoned proofs, structured judges catch 94.7% versus 83.2% for holistic judging (p= 0.0017)
• The overall performance gap concentrates in hidden premises and fabricated citations
• On GPQA Diamond, certified precision is 97.1%

Key Concepts Mentioned

• Theoria
• verification architecture
• typed state transitions
• explicit justifications
• HLE-Verified Gold
• holistic LLM judges
• adversarial poisoned proofs
• GPQA Diamond

Claims Made by the Document

• Theoria significantly outperforms holistic LLM judges on certain types of errors
• Performance is identical on arithmetic and theorem-misapplication errors
• Certified precision on GPQA Diamond is 97.1%

Evidence Used

• On HLE-Verified Gold (185 text-only expert problems), Theoria certifies 105 at 91.4% strict precision...
• On 95 adversarial poisoned proofs across 15 domains, structured judges catch 94.7% versus 83.2% for holistic judging (p= 0.0017)...
• On GPQA Diamond (n= 65), certified precision is 97.1% (Wilson CI [85.1%, 99.5%])

Methods / Approach

UNKNOWN

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

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