論文の概要: Aligning Faithfulness for Theory-Scale Autoformalization

• arxiv url: http://arxiv.org/abs/2610.18498v1
• Date: Tue, 13 Oct 2026 14:53:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.646272
• Title: Aligning Faithfulness for Theory-Scale Autoformalization
• Title（参考訳）: 理論スケールオートフォーマライゼーションのための忠実さの調整
• Abstract要約: 最初の理論スケールの忠実度ベンチマークであるFaithAlignを紹介する。 また、非公式な文脈と仮定が持たない146項目からなる同伴集合であるFaithAlign-Gapを提示する。 8モデル全体では、GPT-6 Astra は 47.8% で最大の欠陥 F1 を達成し、2つ以上の欠陥を持つ項目の4.5% で全ての欠陥を識別する。
• 参考スコア（独自算出の注目度）: 17.298425520643438
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier is the automated evaluation of this property, yet most existing methods operate at the statement level and produce whole-item verdicts, failing to reveal how individual expressions correspond or which contextual interpretations support the judgment. This omission is consequential because AF is inherently theory-scale: target statements derive their meaning from surrounding mathematical material and unstated conventions. We formulate faithfulness evaluation as a context-aware align-then-label problem: identifying phrase-level correspondences between informal and formal statements and assigning a faithfulness label to each under explicitly specified contextual interpretations and assumptions. We also introduce FaithAlign, the first theory-scale faithfulness benchmark comprising 460 items and 4,982 annotated phrase-level links, alongside FaithAlign-Gap, a companion set of 146 items with informal context and assumptions withheld. Each FaithAlign item includes the target statement pair, relevant context, formal dependencies, and, where needed, assumptions specifying one given interpretation. Across 8 models, GPT-6 Astra achieves the highest defect F1 at 47.8% and identifies all defects in only 4.5% of items with two or more defects. On FaithAlign-Gap, Astra identifies only 28.2% of undecidable items as such. These results show the difficulty of recovering context-dependent correspondences, establishing FaithAlign as a testbed for fine-grained, context-aware faithfulness evaluation.
• Abstract（参考訳）: オートフォーマル化(AF)はコンパイル以上のものを必要とする: フォーマルなステートメントは、彼らの非公式なソースの意味、すなわち忠実さを保たなければならない。 新たなフロンティアは、この特性を自動評価するものであるが、既存のほとんどのメソッドはステートメントレベルで動作し、個々の表現がどのように対応するか、どの文脈解釈が判断を支持するかを明らかにするのに失敗し、全体的評決を生成する。 AFは本質的に理論スケールであり、ターゲットステートメントは、周囲の数学的材料や未定の慣習からその意味を導き出す。 本研究では, 文脈対応型アライメント・アライメント・ラベル問題として, 形式文と形式文の句レベルの対応を識別し, 明示された文脈解釈と仮定の下でそれぞれに忠実度ラベルを割り当てることにより, 忠実度の評価を定式化する。 また、460項目と4,982項目の注釈付きフレーズレベルのリンクからなる最初の理論スケール忠実度ベンチマークであるFaithAlign-Gapを紹介した。 FaithAlignの各項目は、対象のステートメントペア、関連するコンテキスト、形式的依存関係、必要に応じて、与えられた解釈を指定する仮定を含む。 8モデル全体では、GPT-6 Astra は 47.8% で最大の欠陥 F1 を達成し、2つ以上の欠陥を持つ項目の4.5% で全ての欠陥を識別する。 FaithAlign-Gapでは、アストラは決定不能なアイテムの28.2%しか特定していない。 これらの結果は,文脈依存的対応の回復が困難であることを示し,よりきめ細かな文脈認識忠実度評価のためのテストベッドとしてFaithAlignを確立した。

関連論文リスト

• Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization [10.295359122542969]
  FYANは仕様、検証計画、論理的レビュー、リーン実証の構築、知識のキュレーション、検証にまたがるエンドツーエンドのワークフローをコーディネートする。 中心的なコンポーネントはエビデンスに基づくセマンティック監査(semantic auditing)であり、形式的なステートメントが彼らの非公式な仕様を忠実に保持するかどうかを評価する。 FYANはまた、通常の微分方程式の数値解析のための9,355行のリーンライブラリODENumLibも開発した。
  論文  参考訳（メタデータ） (2026-09-30T08:02:51Z)
• Truth for Believable AI: Expressed Doubt, Provenance, and Belief Revision as an Engineerable Stance [0.0]
  定型言語モデル上での動作層として,不確実性,先入観を意識したアサーション,明示的信念のリビジョンを実装できるかどうかを検証した。 合成モデルとQwen2.5-0.5B-インストラクタを用いて,機械的に評価したマルチセッションベンチマークを用いて評価を行った。
  論文  参考訳（メタデータ） (2026-09-22T11:34:53Z)
• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieveは、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークである。 証明段階を局所的推論単位に分解し、型付き証明義務を抽出し、検証する。 350-problemのOlympiadデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を実現している。
  論文  参考訳（メタデータ） (2026-08-26T18:43:30Z)
• ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
  ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。 itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
  論文  参考訳（メタデータ） (2026-07-07T22:05:55Z)
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。 ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
  論文  参考訳（メタデータ） (2026-06-30T00:27:53Z)
• Faithful Autoformalization via Roundtrip Verification and Repair [0.4403025166321017]
  そこで本研究では,地平線アノテーションを必要としないラウンドトリップ検証手法を提案する。 2つの形式化が一致するとき、これは忠実な形式化の証拠となる。 我々はClaude Opus 4.6 と GPT-5.2 を用いて150のトラフィックルールに対するアプローチを評価した。
  論文  参考訳（メタデータ） (2026-04-27T22:26:01Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)
• AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
  実世界の情報ニーズから10kクレームを抽出したファクトチェックデータセットであるAmbiFCを提示する。 アンビFCの証拠に対する主張を比較する際に,曖昧さから生じる不一致を分析した。 我々は,このあいまいさをソフトラベルで予測するモデルを開発した。
  論文  参考訳（メタデータ） (2021-04-01T17:40:08Z)

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

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