論文の概要: 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（参考訳）: ラウンドトリップ検証と修復による忠実な自己形式化
- Authors: Daneshvar Amrollahi, Jerry Lopez, Clark Barrett,
- 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分析により、形式的同値性は意味的ドリフトの少ないものと相関していることを確認した。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。