論文の概要: Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization

• arxiv url: http://arxiv.org/abs/2606.09449v1
• Date: Mon, 08 Jun 2026 12:57:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-09 14:42:07.074662
• Title: Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization
• Title（参考訳）: 金本位制のない推論:オートフォーマル化のプロキシ・ジャッジ理論
• Authors: Lei Xu, Xin Quan, André Freitas,
• Abstract要約: 自動形式化(AF)は、非公式な数学的または論理的推論を形式的に検証可能なオブジェクトに変換するようモデルに求める。 我々は、金標準マッチングを軸ごとのプロパティチェックのベクトルに置き換える、AFのための参照フリープロキシ・ジャッジフレームワークを導入する。 miniF2F、ProofNet、e-SNLI、ProntoQAの7つの形式化バックボーンで、改良はシングルショットのICLベースラインよりもパスレートを一貫して引き上げる。
• 参考スコア（独自算出の注目度）: 25.540859911959885
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Complex reasoning tasks increasingly require systems to produce outputs whose correctness cannot be judged by exact match against a single reference. Autoformalization (AF) is a representative example; it asks a model to translate informal mathematical or logical reasoning into a formally checkable object, yet expert-validated formalizations do not scale beyond toy cases and a single informal argument can admit many valid formal renderings. Progress therefore depends on whether partial, structured proxies can substitute for exact references. We introduce a reference-free proxy-judge framework for AF that replaces gold-standard matching with a vector of per-axis property checks. The framework organizes the proxy along three structural scopes that cover global properties of the elicited object, per-module properties internal to its sub-components, and cross-domain properties that re-align it to the informal source, and aggregates each axis into a verdict vector. The vector drives a reflective refinement loop in which a violated coordinate routes the controller to a matching repair target, so each iteration changes only what is judged wrong. Under bounded judge noise, the expected intrinsic gap contracts geometrically to a noise-dependent plateau. Across seven formalization backbones on miniF2F, ProofNet, e-SNLI, and ProntoQA, refinement consistently lifts Pass Rate over the single-shot ICL baseline, and the per-axis proxy outperforms a matched scalar proxy on benchmarks where the baseline has room to improve. Structured proxy judgments therefore provide both a practical refinement signal and a theoretical handle on convergence when exact references are unavailable.
• Abstract（参考訳）: 複雑な推論タスクは、単一の参照に対して正確な一致によって正当性を判断できない出力を生成するシステムを必要とする。 オートフォーマル化(AF)は代表的な例であり、非公式な数学的推論や論理的推論を形式的に検証可能なオブジェクトに変換するようモデルに求めるが、専門家が検証した形式化はおもちゃのケースを超えてスケールせず、単一の非公式な引数は多くの有効な形式的レンダリングを許容することができる。 したがって、プログレッシブは、部分的に構造化されたプロキシが正確な参照を代用できるかどうかに依存する。 我々は、金標準マッチングを軸ごとのプロパティチェックのベクトルに置き換える、AFのための参照フリープロキシ・ジャッジフレームワークを導入する。 このフレームワークは、ライセンスされたオブジェクトのグローバルプロパティ、サブコンポーネントの内部にあるモジュールごとのプロパティ、非公式なソースに再アライメントするクロスドメインプロパティを含む3つの構造的スコープに沿ってプロキシを編成し、各軸を検証ベクトルに集約する。 ベクトルは、違反した座標がコントローラを一致した修理ターゲットにルーティングする反射リファインメントループを駆動するので、各イテレーションは、誤判定されたもののみを変更する。 有界判定ノイズの下では、予測固有ギャップは、雑音依存プラトーと幾何学的に収縮する。 miniF2F、ProofNet、e-SNLI、ProntoQAの7つの形式化バックボーンを通じて、改良は一貫して、シングルショットのICLベースラインよりもパスレートを上昇させ、アクセントプロキシは、ベースラインが改善の余地のあるベンチマークでマッチしたスカラープロキシよりも優れています。 したがって、構造化されたプロキシ判断は、正確な参照が利用できない場合に、実用的な洗練された信号と収束に関する理論的ハンドリングの両方を提供する。

関連論文リスト

• Citation-Closure Retrieval and Per-Rule Attribution for Real-World Regulatory Compliance Question Answering [54.97384993676565]
  複雑な国内R&D規制から派生した運用知識グラフを特徴とする,新たなベンチマークであるRegOps-Benchを用いて,レギュレーションコンプライアンスQAを形式化する。 RefWalkはクロスドキュメントの引用を横切り、マックスベースのアグリゲーションを通じてマルチビュー候補を融合させ、ソースへのクレームを明示的にマッピングするためにルールごとの属性を強制する。
  論文  参考訳（メタデータ） (2026-05-28T10:38:38Z)
• A Controlled Counterexample to Strong Proxy-Based Explanations of OOD Performance: in a Fixed Pretraining-and-Probing Setup [0.9805949492148788]
  タスクに依存しない構造プロキシは、ある事前学習コーパスが他のコーパスよりも優れている理由を解釈するためにしばしば使用される。 我々は,この要件を,学習構造の計算的有界概念に動機づけられた,定型事前学習・探索設定で検証する。 総合的な学習構造のためのプロキシは、制御された設定であっても、OODパフォーマンスを駆動するタスク関連構造を追跡することができません。
  論文  参考訳（メタデータ） (2026-05-12T05:36:46Z)
• CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
  VCM(Virtual Cell Modeling)は、摂動応答を予測できるだけでなく、予測が失敗した場合にターゲットリビジョンをサポートするモデルを必要とする。 現在のLCM支援モデリングでは、予測誤差が実行可能実装を通して観測されるという改善ルーティング問題に直面している。 提案するCellScientistは,高レベル仮説空間と低レベル実行可能実装空間を結合した,二重空間階層型フレームワークである。
  論文  参考訳（メタデータ） (2026-05-08T06:40:24Z)
• IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
  既存のパイプラインは不透明でエンドツーエンドの出力を生成し、検査の中間状態は公開しない。 IMPACT-Cycleは,マルチモーダル反復クレームレベルのメンテナンスとして,長時間ビデオ理解を再構築するマルチエージェントシステムである。
  論文  参考訳（メタデータ） (2026-04-22T03:03:33Z)
• From Perception to Autonomous Computational Modeling: A Multi-Agent Approach [0.0]
  本稿では,協調型大言語モデル(LLM)エージェントが完全計算力学ワークフローを自律的に実行する,解法に依存しないフレームワークを提案する。 エージェントは、パイプライン層間の条件付きイテレーションを導入する品質ゲートを備えた共有コンテキスト空間上の条件付き演算子として形式化される。
  論文  参考訳（メタデータ） (2026-04-08T07:56:34Z)
• Reasoning Provenance for Autonomous AI Agents: Structured Behavioral Analytics Beyond State Checkpoints and Execution Traces [0.0]
  Agent Execution Record (AER) は構造化された推論プリミティブであり、すべてのステップで第一級クエリ可能なフィールドとしてインテント、観察、推論をキャプチャする。 AERが集団レベルの行動分析を可能にする方法を示す: 推論パターンマイニング、信頼度校正、クロスエージェント比較、モックリプレイによる反事実回帰テスト。
  論文  参考訳（メタデータ） (2026-03-23T08:27:54Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  本稿では,大規模言語モデルとSMTソルバを組み合わせたニューロシンボリック・フレームワークを提案する。 本稿では,(1)形式的意味的等価性チェックによるマルチモデルコンセンサス,(2)適切な検証戦略に異なるクレーム型を指示するセマンティックルーティング,(3)最小補正サブセットによる正確な論理的エラーローカライゼーション,の3点を紹介する。 GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
  論文  参考訳（メタデータ） (2026-01-27T20:59:11Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Retrieval is Not Enough: Enhancing RAG Reasoning through Test-Time Critique and Optimization [58.390885294401066]
  Retrieval-augmented Generation (RAG) は知識基底型大規模言語モデル(LLM)を実現するためのパラダイムとして広く採用されている。 RAGパイプラインは、モデル推論が得られた証拠と整合性を維持するのに失敗することが多く、事実上の矛盾や否定的な結論につながる。 批判駆動アライメント(CDA)に基づく新しい反復的枠組みであるAlignRAGを提案する。 AlignRAG-autoは、動的に洗練を終了し、批判的な反復回数を事前に指定する必要がなくなる自律的な変種である。
  論文  参考訳（メタデータ） (2025-04-21T04:56:47Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。