Fugu-MT 論文翻訳(概要): Sage: Formalization with Semantic Correction

論文の概要: Sage: Formalization with Semantic Correction

arxiv url: http://arxiv.org/abs/2609.35790v2
Date: Wed, 30 Sep 2026 11:57:05 GMT
ステータス: 翻訳完了
システム内更新日: 2026-10-05 14:48:16.25763
Title: Sage: Formalization with Semantic Correction
Title（参考訳）: セージ:意味的補正による形式化
Abstract要約: モノリシック翻訳を4段階の分解生成パイプラインで置き換えるエージェントフレームワークであるSageを紹介する。 Sageは、73.3%パス@4の共同コンパイルとOmni-MATHのセマンティック忠実性を証明なしで達成しながら、漏洩を2.7%まで抑制する。 IMO-Unformalizedは175の非形式化国際数理オリンピック問題のフロンティアであり、Sageは87.4%のパス@4の正当性を持つ効果的なゼロショット一般化を示す。
参考スコア（独自算出の注目度）: 4.478157375638768
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided. Translating informal natural language into a formal language is a critical data bottleneck plagued by an "illusion of rigor": standard type-checkers accept statements that compile but drop hypotheses, introduce vacuous truths, or subtly alter mathematical bounds. To resolve this, we introduce Sage (Semantic Agent-Guided Formalization Engine), an agentic framework that replaces monolithic translation with a four-stage decomposed generation pipeline coupled with a dual-signal semantic correction loop. By pairing Lean 4 compiler diagnostics with multi-dimensional semantic feedback, our correction loop enforces mathematical fidelity alongside syntactic validity. By explicitly accounting for the gap between open-ended queries and declarative formal targets, our pipeline prevents models from achieving high formalization rates by guessing unverified answers (exhibiting a 70.9% answer leakage rate in monolithic baselines). Consequently, Sage suppresses leakage to 2.7% while achieving 73.3% pass@4 joint compilation and semantic fidelity on the Omni-MATH without proofs (compared to 42.0% for a fine-tuned Goedel-Formalizer-V2 baseline). Finally, on IMO-Unformalized, a novel frontier of 175 unformalized International Mathematical Olympiad problems, Sage demonstrates effective zero-shot generalization with 87.4% pass@4 verified fidelity compared to just 19.4% for the baseline, winning over 79% of blind pairwise evaluations.
Abstract（参考訳）: ニューラル定理の証明者は形式数学において印象的なマイルストーンを達成したが、彼らは主に忠実なリーン4の形式文がすでに提供されているという仮定に基づいて運営されている。フォーマルな自然言語を形式的な言語に翻訳することは、「厳密さのイリュージョン」に悩まされる重要なデータボトルネックである。そこで本研究では,モノリシック翻訳を4段階の分解生成パイプラインに置き換えるエージェントフレームワークであるSage(Semantic Agent-Guided Formalization Engine)と,二重信号の意味的補正ループを結合したSage(Semantic Agent-Guided Formalization Engine)を紹介する。多次元のセマンティックフィードバックとLean 4コンパイラの診断を組み合わせることで、我々の補正ループは、構文的妥当性とともに数学的忠実さを強制する。オープンエンドクエリと宣言的形式的ターゲットのギャップを明示的に考慮することにより,未検証の回答(モノリシックベースラインにおける70.9%の回答リーク率)を推測することで,モデルが高い形式化率を達成するのを防ぐことができる。その結果、Sageは73.3%パス@4の共同コンパイルとOmni-MATHのセマンティックフィリティを証明なしで達成し、リークを2.7%まで抑制した(細調整されたGoedel-Formalizer-V2ベースラインでは42.0%)。最後に、175の非形式化国際数理オリンピック問題のフロンティアであるIMO-Unformalizedにおいて、セージは87.4%のパス@4の正当性で効果的なゼロショット一般化を示し、ベースラインの19.4%に過ぎず、盲対評価の79%以上を獲得した。

関連論文リスト

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)
ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文参考訳（メタデータ） (2025-10-28T16:22:54Z)
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph [7.606625807305093]
リーンの予想レベルの形式化のためのシステムであるAriaを紹介します。 Ariaは、2フェーズのGraph-of-Thoughtプロセスを通じて、人間の専門家による推論をエミュレートする。 AriaScorerは、用語レベルの接地のためにMathlibから定義を検索する。
論文参考訳（メタデータ） (2025-10-06T06:25:11Z)
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)
Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。 ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
論文参考訳（メタデータ） (2024-06-11T13:01:50Z)
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。この合成データセットでDeepSeekMath 7Bモデルを微調整します。我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文参考訳（メタデータ） (2024-05-23T09:03:42Z)

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

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