論文の概要: Theoria: Rewrite-Acceptability Verification over Informal Reasoning States
- arxiv url: http://arxiv.org/abs/2607.01223v1
- Date: Wed, 01 Jul 2026 17:56:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-02 19:56:08.019754
- Title: Theoria: Rewrite-Acceptability Verification over Informal Reasoning States
- Title（参考訳）: 理論:インフォーマルな推論状態に対するリライト・アクセプタビリティの検証
- Authors: Ben Slivinski, Michael Saldivar,
- Abstract要約: このギャップを埋める検証アーキテクチャであるTheoriaを紹介します。
候補解は、型付き状態遷移のシーケンスに書き換えられる。
すべての遷移は独立して監査可能である。
- 参考スコア（独自算出の注目度）: 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%]).
- Abstract（参考訳）: AIシステムの回答はいつ信頼されるべきなのか?
正式な証明アシスタントは確実性を提供するが、ほとんどの問題分布に到達できない; スカラーLLM判事はカバレッジを提供するが、事実の後に監査できない不透明なスコアを生成し、LLMと同一のコヒーレンス問題に直面する。
このギャップを埋める検証アーキテクチャであるTheoriaを紹介します。
候補解は型付き状態遷移のシーケンスに書き換えられ、それぞれが明示的な正当性によってライセンスされ、引用、計算、問題生成事実のいずれかであり、全ての遷移は独立して監査可能である。
基本的な不変性は変化の完全性であり、連続する証明状態間のすべての差は考慮されなければならない。
HLE-Verified Gold (185テキストのみの専門家問題)では、Theoriaは105を91.4%の厳密な精度で認証している(Wilson 95% CI [84.5%, 95.4%])。
すべての認証は、独立して各ステップに挑戦できる人間の可読性証明トレースを生成する。
ホロスティックLSMの判定は、一致したカバレッジで同等の精度を達成するが、異なる問題(Jaccard 0.14-0.36)で失敗し、アプローチを補完する。
15ドメインにわたる95の逆毒物証明では、構造化された審査員が94.7%、全体判定が83.2%(p=0.0017)を捕える。
全体の11.5pp差は隠れた前提(90.6%対62.5%、28pp差)と、形式解析が利点を予測するエラークラス(100%対90%)に集中している。
GPQAダイヤモンド(n=65)では、認定精度は97.1%(ウィルソンCI [85.1%, 99.5%])である。
関連論文リスト
- Selective QA over Conflicting Multi-Source Personal Memory: A Diagnostic Testbed and Method Comparison [11.187819120306825]
既存のベンチマークでは、メソッドに与えられたエビデンスやメソッドのコンフリクト解決ステップからエラーが生じたかどうかはほとんど示されていない。
我々はこれをマルチソース・パーソナルメモリの競合に対する選択的QAとして検討する。
8種類の推論型,480のペルソナ,4つのランダムシード,34,560のインスタンスを対象とした18の質問テンプレートを含むベンチマークを作成した。
論文 参考訳（メタデータ） (2026-05-28T15:33:39Z) - FinVerBench: Benchmark Validity and Calibration in Large Language Model Financial Statement Verification [0.0]
FinVerBenchは、ファイナンシャルステートメント検証のためのベンチマークおよび妥当性調査である。
SEC 10-K の S&P 500 社への提出書類から作成されている。
論文 参考訳（メタデータ） (2026-05-28T08:30:15Z) - Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning [16.398764816978584]
リーンは、自然言語の数学的答えを判断するのにますます使われていますが、その信号は部分的です。
このシグナルは (i) 急激なカバレッジ依存であり, 証明に勝つ答えは高いカバレッジでは96%の確率で正しいが, 20%は低い。
7Bオートフォーマライザはわずか28%の問題でクラスを証明し、マニュアル監査ではその約43%が忠実であることがわかった。
受理された回答や棄権に縛られた有限サンプル選択リスクを認証する,リーントレース診断のためのセレクタであるCOVCALを提案する。
論文 参考訳（メタデータ） (2026-05-27T11:59:28Z) - Deployment-complete benchmarking [0.0]
ベンチマークエビデンスがデプロイメントアクションを決定するかどうか、デプロイ完全ベンチマークテスト。
ベンチマークは、各エビデンスファイバー上でアクションが定数であるときのクレームに対して完了する。
混合繊維は配置情報の欠如を露呈し、完成曲線はあいまいさを解決するのに必要な証拠を定量化する。
論文 参考訳（メタデータ） (2026-05-25T16:15:22Z) - Adaptive Consensus in LLM Ensembles via Sequential Evidence Accumulation: Automatic Budget Identification and Calibrated Commit Signals [0.0]
DASEは、ベンチマークをまたいで一般化するコミット型ルーティングパーティションを生成する。
インジェクション帯域ではなく、適応的な停止が正確さを駆動する。
インジェクションベースの手法は、逆Uの精度-vs-推論軌道を示す。
論文 参考訳（メタデータ） (2026-05-05T19:24:10Z) - HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。
HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。
我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7～10ポイントの絶対精度を観測した。
論文 参考訳（メタデータ） (2026-02-15T02:50:15Z) - CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
隠れアクティベーションの軌跡内の幾何的に分離可能なシグネチャとして解の正しさが符号化されていることを示す。
ClUE は LLM-as-a-judge ベースラインを一貫して上回り、候補者の再選において近代的な信頼に基づく手法に適合または超えている。
論文 参考訳（メタデータ） (2025-10-02T02:14:33Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - Exploring Response Uncertainty in MLLMs: An Empirical Evaluation under Misleading Scenarios [49.53589774730807]
マルチモーダル大規模言語モデル(MLLM)は近年,視覚的質問応答から映像理解に至るまでのタスクにおいて,最先端のパフォーマンスを実現している。
12件のオープンソースMLLMが, 単一の偽装キューを受けた65%の症例において, 既往の正解を覆した。
論文 参考訳（メタデータ） (2024-11-05T01:11:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。