Theoria: Rewrite-Acceptability Verification over Informal Reasoning States
06:00 · July 2, 2026 · arXiv cs.AI RSS
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%]).
Summary
Theoria addresses a core limitation in AI verification: formal proof assistants deliver strong guarantees once a problem is fully formalized, yet they cannot scale across most natural-language reasoning tasks, while scalar LLM judges cover far more ground but return opaque scores that cannot be audited and remain vulnerable to the same coherence failures as the models they evaluate. The system rewrites a candidate solution into an explicit sequence of typed state transitions. Each transition is paired with one justification—citation, computation, or a fact supplied by the problem—and the verifier checks only whether that justification licenses the observed change between consecutive states. The governing invariant is completeness of change: every difference between states must be accounted for, so any hidden premise or unstated assumption appears as an unlicensed mutation rather than passing unnoticed.
Because verification occurs locally against an explicit before-and-after diff, the architecture reduces the scope of each LLM judgment and produces a human-readable proof trace in which every step can be challenged independently. On the HLE-Verified Gold set of 185 expert text-only problems, Theoria certifies 105 solutions at 91.4 percent strict precision. The same witness format yields 97.1 percent certified precision on the 65-problem GPQA Diamond subset. In an adversarial evaluation using 95 poisoned proofs spanning 15 domains, structured verification detects 94.7 percent of errors compared with 83.2 percent for holistic LLM judging, with the largest gains on hidden premises and fabricated citations—the error classes the formal analysis predicts will be most exposed by the state-transition representation.
The approach is positioned as complementary rather than competitive with existing methods. Holistic judges reach comparable precision at matched coverage yet fail on largely disjoint subsets of problems, while formal tools remain preferable once a specification has been successfully encoded. By exposing each premise and transformation under a typed local license, Theoria also creates a more tractable intermediate target for downstream autoformalization than free-form prose.
Why it matters
This research directly supports the Dutch and EU focus on ethical, transparent, and trustworthy AI by providing a rigorous method to audit LLM reasoning. It offers researchers and advanced practitioners a novel framework to mitigate hallucinations and ensure compliance with emerging AI regulations.
