論文の概要: Faithful Autoformalization via Roundtrip Verification and Repair
- arxiv url: http://arxiv.org/abs/2604.25031v1
- Date: Mon, 27 Apr 2026 22:26:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-29 16:49:17.617412
- Title: Faithful Autoformalization via Roundtrip Verification and Repair
- Title（参考訳）: ラウンドトリップ検証と修復による忠実な自己形式化
- Abstract要約: そこで本研究では,地平線アノテーションを必要としないラウンドトリップ検証手法を提案する。
2つの形式化が一致するとき、これは忠実な形式化の証拠となる。
我々はClaude Opus 4.6 と GPT-5.2 を用いて150のトラフィックルールに対するアプローチを評価した。
- 参考スコア（独自算出の注目度）: 0.4403025166321017
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural language, re-formalize, and use a formal tool to check logical equivalence. When the two formalizations agree, this provides evidence of a faithful formalization. When they disagree, a diagnosis step identifies which translation stage failed, and a targeted repair operator attempts to correct that stage. We evaluate our approach on 150 traffic rules using Claude Opus 4.6 and GPT-5.2. Diagnosis-guided repair raises formal equivalence from 45--61% to 83--85% for both models, outperforming a random-repair baseline. An independent NLI analysis confirms that formal equivalence is correlated with less semantic drift.
- Abstract（参考訳）: LLMが自然言語を形式化するとき、アウトプットが忠実であることをどうやって知るのか?
文を形式化し、結果を自然言語に翻訳し、再形式化し、論理的等価性をチェックするための形式ツールを使用する。
2つの形式化が一致するとき、これは忠実な形式化の証拠となる。
それらが一致しない場合、診断ステップは、どの翻訳段階が失敗したかを識別し、ターゲットの修復作業者は、そのステージを修正しようとする。
我々はClaude Opus 4.6 と GPT-5.2 を用いて150のトラフィックルールに対するアプローチを評価した。
診断誘導修復は、両方のモデルで45～61%から83～85%に正式な等価性を高め、ランダムに修復されたベースラインを上回っている。
独立したNLI分析により、形式的同値性は意味的ドリフトの少ないものと相関していることを確認した。
関連論文リスト
- 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) - Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
Monty: アサーションのための自動形式化フレームワークを紹介します。
本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。
提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
論文 参考訳（メタデータ） (2026-07-14T22:12:14Z) - 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) - Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
我々は、厳密な証明オートフォーマライザは、理想化された証明から分岐する非公式な証明であっても忠実でなければならないと論じる。
ミニF2FとMATH-500の両摂動によるベンチマークを構築した。
我々は,近年の7つのモデルを評価する。これらはいずれもグローバルな摂動に敏感であり,局地的な摂動の下では忠実に保たない。
論文 参考訳（メタデータ） (2026-06-12T18:10:21Z) - Retrieval-Augmented Linguistic Calibration [57.41519309308438]
我々は,言語的信頼度を,文が正しいと認識される確率値の分布としてモデル化する。
Retrieval-Augmented Linguistic truth (RALC)は、信頼性信号を自然言語に伝達する軽量なポストホックパイプラインである。
論文 参考訳（メタデータ） (2026-05-19T04:31:38Z) - Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning [20.336209492846752]
形式検証は証明の正当性を保証するが、形式化の忠実性は保証しない。
私たちは、Lean 4の証明を生成する際に、フロンティアモデルがこのギャップを利用するかどうかを調査します。
統一世代における体系的なゲーミングの証拠は見つからない。
論文 参考訳（メタデータ） (2026-04-21T13:37:49Z) - miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward [16.8655558789989]
ミニF2Fベンチマークの形式的および非公式なステートメントは、ミニF2Fの問題からなる数学オリンピアードに参加するように命じられたAIシステムの観点から分析する。
評価結果から,本論文の論文では,SoTAモデルを用いて,これらのパイプラインの最適精度が約36%であることが判明した。
本報告では, miniF2F-v2 を形式的および非公式な文と証明で完全検証した。
論文 参考訳（メタデータ） (2025-11-05T01:27:49Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion [30.51794514312176]
効果的な自己形式化のための2つの重要な能力を特定する。
我々は、両方の能力を改善するデータ合成およびトレーニングパイプラインであるThinkingFを紹介します。
結果の7Bと32Bモデルは、包括的な形式的知識と強い形式的・形式的推論の両方を示す。
論文 参考訳（メタデータ） (2025-08-06T13:28:22Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。