論文の概要: Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
- arxiv url: http://arxiv.org/abs/2606.31002v1
- Date: Tue, 30 Jun 2026 00:27:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-01 18:27:19.034497
- Title: Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
- Title（参考訳）: コンパイルを超えて: 忠実な自然言語とリーンのステートメントの形式化を評価する
- Abstract要約: 本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。
ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
- 参考スコア（独自算出の注目度）: 10.775710068605006
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check while omitting hypotheses, changing domains, or expressing a vacuous claim. We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem. On a 400-entry graduate-level benchmark spanning real analysis, complex analysis, topology, and algebra, our protocol combines Lean compilation, cross-model semantic judging, and human expert calibration. The resulting picture is different from compile-rate evaluation: a full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap. Targeted human audits support the metric as a conservative decision boundary: across available case-level audits, 96.0% of consensus-positive outputs are human-confirmed faithful, while 82.4% of compile-pass consensus-negative outputs are human-confirmed semantic failures. Under this metric, existing one-shot formalizer models and prover-oriented Lean models remain low, suggesting that formal validity, proof-oriented Lean competence, and faithful statement generation should be reported separately. We then use a full $2^3$ factorial design to decompose three recurring interventions in formalization pipelines: parametric expert drafting, Mathlib/context search, and Lean elaboration feedback. Elaboration feedback is the largest validity intervention, but it also exposes a larger compile-pass semantic-failure bucket; search mainly improves grounding and selectivity; and fine-tuned drafting is largely substitutable in this tool stack once feedback and grounding are available.
- Abstract（参考訳）: Theorem-proving benchmarks evaluate proof search against fixed formal statement, but natural- language-to-Lean formalization they generate the formal statement itself。
この設定では、コンパイルは妥当性チェックに過ぎず、リーン宣言は仮説を省略したり、ドメインを変更したり、空白のクレームを表現したりしながら型チェックを行うことができる。
本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。
実解析、複素解析、トポロジ、代数にまたがる400エントリーレベルのベンチマークにおいて、我々のプロトコルはリーンコンパイル、クロスモデルセマンティック判断、および人間の専門家の校正を組み合わせたものである。
完全なツール拡張エージェントは89.5%のコンパイルに到達したが、60.5%のコンセンサス忠実さしか示さず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
利用可能なケースレベルの監査において、コンセンサス陽性のアウトプットの96.0%は人間に忠実であり、コンパイルパスのコンセンサス陰性なアウトプットの82.4%は人間に確認されたセマンティック障害である。
この測定基準の下では、既存のワンショットフォーマライザモデルと証明者指向のリーンモデルは依然として低く保たれており、形式的妥当性、証明指向のリーン能力、忠実なステートメント生成を別々に報告すべきであることを示唆している。
次に、パラメトリックのエキスパートドラフト、Mathlib/context Search、Lean Elaborationのフィードバックという、3つの反復的な介入をフォーマル化パイプラインで分解するために、フル2^3$のファクタアル設計を使用します。
評価フィードバックは最大の妥当性の介入であるが、さらに大きなコンパイルパスのセマンティック障害バケットを公開し、検索は主にグラウンドと選択性を改善し、フィードバックとグラウンドが利用可能になったら、微調整のドラフトは、このツールスタックでほぼ置換可能である。
関連論文リスト
- Autoformalizing Argumentative Material Inferences [26.35292656634472]
我々は、ガード補完として議論材料推論のための自己形式化を開発する。
GUARDは、証明された信条を大幅に改善する。
シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
論文 参考訳（メタデータ） (2026-09-15T11:05:26Z) - 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) - 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) - Faithful Autoformalization via Roundtrip Verification and Repair [0.4403025166321017]
そこで本研究では,地平線アノテーションを必要としないラウンドトリップ検証手法を提案する。
2つの形式化が一致するとき、これは忠実な形式化の証拠となる。
我々はClaude Opus 4.6 と GPT-5.2 を用いて150のトラフィックルールに対するアプローチを評価した。
論文 参考訳（メタデータ） (2026-04-27T22:26:01Z) - Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。
HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。
我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7～10ポイントの絶対精度を観測した。
論文 参考訳（メタデータ） (2026-02-15T02:50:15Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。