論文の概要: Evaluating the Robustness of Proof Autoformalization in Lean 4

• arxiv url: http://arxiv.org/abs/2606.14867v1
• Date: Fri, 12 Jun 2026 18:10:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 16:21:32.350345
• Title: Evaluating the Robustness of Proof Autoformalization in Lean 4
• Title（参考訳）: リーン4における証明オートフォーマル化のロバストさの評価
• Authors: Zhengtao Gui, Sheng Yang, Zhouxing Shi,
• Abstract要約: 我々は、厳密な証明オートフォーマライザは、理想化された証明から分岐する非公式な証明であっても忠実でなければならないと論じる。 ミニF2FとMATH-500の両摂動によるベンチマークを構築した。 我々は,近年の7つのモデルを評価する。これらはいずれもグローバルな摂動に敏感であり,局地的な摂動の下では忠実に保たない。
• 参考スコア（独自算出の注目度）: 8.029528831501514
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have developed LLM-based models for proof autoformalization. However, existing evaluations have typically focused on translating well-formed informal proofs from curated datasets. We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from these idealized ones, and we present the first study on the robustness of proof autoformalization models. We formulate two categories of perturbations and evaluate robustness under each: a global perturbation paraphrases the informal proof in a different style, under which the formalization should remain consistent; a local perturbation alters a value, symbol, or proof step, possibly in a counterfactual way, and a robust formalization should faithfully reflect the perturbation rather than reverting to the original one or inferring a different one on its own. We build a benchmark with both perturbations on miniF2F and MATH-500, and automatically measure how stable a proof autoformalization's correctness is under global perturbations and how faithfully its output reflects local perturbations. We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations. Code and data are available via https://github.com/ucr-rai/robust-proof-autoformalization.
• Abstract（参考訳）: Proof Autoformalization は、自然言語で書かれた数学的非公式な証明を、Lean -4 のような形式的な言語の形式的な証明に変換することを目的としている。 いくつかの研究が、証明オートフォーマル化のためのLSMベースのモデルを開発した。 しかしながら、既存の評価は典型的には、キュレートされたデータセットから、よく形成された非公式な証明を翻訳することに重点を置いている。 我々は、これらの理想化されたものから分岐する非公式な証明であっても、ロバストな証明オートフォーマライザは忠実でなければならないと論じ、証明オートフォーマライゼーションモデルのロバスト性に関する最初の研究を示す。 我々は摂動の2つのカテゴリを定式化し、それぞれの下で頑健さを評価する: グローバル摂動は、形式化が整ったままでなければならない、非公式な証明を異なるスタイルで言い換える; 局所摂動は、おそらく反ファクト的な方法で値、記号、証明のステップを変化させる; 頑健な形式化は、元のものへの回帰や別のものへの推論よりも、忠実に摂動を反映すべきである。 我々は,MiniF2FとMATH-500の両方の摂動を用いたベンチマークを構築し,証明の自己形式化の正しさがグローバルな摂動の下でどの程度安定であるか,その出力が局所摂動を忠実に反映しているかを自動的に測定する。 我々は,近年の7つのモデルを評価する。これらはいずれもグローバルな摂動に敏感であり,局地的な摂動の下では忠実に保たない。 コードとデータはhttps://github.com/ucr-rai/robust-proof-autoformalizationを通じて入手できる。

関連論文リスト

• Casual as an Anchor: Resolving Supervision Misalignment in Formality Transfer Dataset [22.0608497133374]
  形式的転送は、通常、形式的レジスタと形式的レジスタの間の対称的な双方向タスクとしてフレーム化される。 このフレーミングは、GYAFCのような既存のベンチマークにおいて、監督設計上の欠陥を隠蔽していると論じる。 人間の整合性の定義の下で、ベンチマーク形式ラベルを再評価することで、このミスアライメントを定量化する。
  論文  参考訳（メタデータ） (2026-05-28T05:07:02Z)
• 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)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。 まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。 ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)

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

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