Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

• URL: http://arxiv.org/abs/2607.01223v3
• Date: Thu, 09 Jul 2026 15:39:53 GMT
• Title: Theoria: Rewrite-Acceptability Verification over Informal Reasoning States
• Abstract summary: We present Theoria, a verification architecture that closes this gap.<n>A candidate solution is rewritten into a sequence of typed state transitions.<n>Every transition is independently auditable.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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%]).

Related papers

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  A research idea may be novel, coherent, and scientifically plausible, yet its proposed method may remain insufficiently specified for faithful implementation.<n>We study the codification readiness of implementation-facing research-method specifications, defined by whether they provide sufficient methodological information for a competent implementer or coding agent to construct the intended method without unsupported assumptions.<n>We introduce IdeaAMBIG, a benchmark of 660 evidence-grounded instances: 163 real-world gaps from reports and GitHub issues, and 497 controlled synthetic gaps injected into codification-ready references.
  arXiv  Detail & Related papers  (2026-09-09T17:59:04Z)
• Explanation Multiplicity: Circuit-Level Interpretability Evidence Does Not Survive Defensible Analytic Variation [0.0]
  EU AI Act requires providers of high-risk systems to file technical documentation describing how the system reaches its decisions.<n>Mechanistic interpretability is the obvious source of such evidence, and circuit discovery is its most developed instrument.<n>We ask whether that evidence survives the condition under which it would be relied upon: two competent analysts, the same system, the same tool, different defensible settings.
  arXiv  Detail & Related papers  (2026-08-13T20:27:56Z)
• Share the Judge, Learn the Deferral: Where Specialization Helps LLM Evaluation [0.1269104766024433]
  We study 99,952 public, rubric-conditioned examples.<n>Supplying the correct rubric improves locked-test accuracy by 2.11 points over a response-only control.<n>On RewardBench 2, learned correctness heads route examples through a 0.6B-4B-8B cascade without changing any reward score.
  arXiv  Detail & Related papers  (2026-07-30T10:29:22Z)
• Selective QA over Conflicting Multi-Source Personal Memory: A Diagnostic Testbed and Method Comparison [11.187819120306825]
  Existing benchmarks rarely show whether an error came from the evidence given to a method or from the method's conflict-resolution step.<n>We study this as selective QA over conflicting multi-source personal memory.<n>We develop a benchmark containing 18 question templates across 8 reasoning types, 480 personas, 4 random seeds, and 34,560 instances.
  arXiv  Detail & Related papers  (2026-05-28T15:33:39Z)
• FinVerBench: Benchmark Validity and Calibration in Large Language Model Financial Statement Verification [0.0]
  FinVerBench is a benchmark and validity study for financial statement verification.<n>It is built from SEC 10-K variant filings for 43 S&P 500 companies.
  arXiv  Detail & Related papers  (2026-05-28T08:30:15Z)
• Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning [16.398764816978584]
  Lean is increasingly used to judge natural-language mathematical answers, but its signal is partial.<n>We show this signal is (i) sharply coverage-dependent, that is the proof-winning answer is correct 96% of the time at high proved coverage but 20% at low.<n>A 7B autoformalizer proves a class for only 28% of problems, and a manual audit finds only approximately 43% of those faithful.<n>We propose COVCAL, a selector over Lean-trace diagnostics that certifies a finite-sample selective-risk bound on accepted answers or abstains.
  arXiv  Detail & Related papers  (2026-05-27T11:59:28Z)
• Deployment-complete benchmarking [0.0]
  Deployment-complete benchmarking tests whether benchmark evidence determines a deployment action.<n>A benchmark is complete for a claim exactly when the action is constant on each evidence fiber.<n>Mixed fibers expose missing deployment information, and completion curves quantify the evidence required to resolve ambiguity.
  arXiv  Detail & Related papers  (2026-05-25T16:15:22Z)
• Agentic Proving for Program Verification [44.663012714194025]
  Agentic systems have emerged as state-of-the-art approaches for automated theorem proving in formal mathematics.<n>We evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation.
  arXiv  Detail & Related papers  (2026-05-22T15:41:27Z)
• Adaptive Consensus in LLM Ensembles via Sequential Evidence Accumulation: Automatic Budget Identification and Calibrated Commit Signals [0.0]
  DASE produces a commit-type routing partition that generalises across benchmarks.<n> Adaptive stopping, not injection bandwidth, drives accuracy.<n>Injection-based methods exhibit an inverted-U accuracy-vs-inference trajectory.
  arXiv  Detail & Related papers  (2026-05-05T19:24:10Z)
• HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
  Humanity's Last Exam (HLE) has become a widely used benchmark for evaluating frontier large language models.<n>We introduce HLE-Verified, a verified and revised version of HLE with a transparent verification protocol and fine-grained error taxonomy.<n>We evaluate seven state-of-the-art language models on HLE and HLE-Verified, observing an average absolute accuracy gain of 7--10 percentage points.
  arXiv  Detail & Related papers  (2026-02-15T02:50:15Z)
• CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
  We show that correctness of a solution is encoded as a geometrically separable signature within the trajectory of hidden activations.<n>ClUE consistently outperforms LLM-as-a-judge baselines and matches or exceeds modern confidence-based methods in reranking candidates.
  arXiv  Detail & Related papers  (2025-10-02T02:14:33Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  We introduce Veracity Search (VS), a discrete search algorithm over veracity assignments.<n>It performs otherwise intractable inference in the posterior distribution over latent veracity values.<n>It generalizes VS, enabling accurate zero-shot veracity inference in novel contexts.
  arXiv  Detail & Related papers  (2025-05-17T04:16:36Z)
• Exploring Response Uncertainty in MLLMs: An Empirical Evaluation under Misleading Scenarios [49.53589774730807]
  Multimodal large language models (MLLMs) have recently achieved state-of-the-art performance on tasks ranging from visual question answering to video understanding.<n>We reveal a response uncertainty phenomenon: twelve state-of-the-art open-source MLLMs overturn a previously correct answer in 65% of cases after receiving a single deceptive cue.
  arXiv  Detail & Related papers  (2024-11-05T01:11:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.