論文の概要: ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

• arxiv url: http://arxiv.org/abs/2510.15681v1
• Date: Fri, 17 Oct 2025 14:20:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-20 20:17:34.650968
• Title: ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
• Title（参考訳）: ProofBridge: リーンにおける自然言語証明の自動形式化
• Authors: Prithwish Jana, Kaan Kale, Ahmet Ege Tanriverdi, Cruise Song, Sriram Vishwanath, Vijay Ganesh,
• Abstract要約: ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。 中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。 我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
• 参考スコア（独自算出の注目度）: 9.764411884491052
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Translating human-written mathematical theorems and proofs from natural language (NL) into formal languages (FLs) like Lean 4 has long been a significant challenge for AI. Most state-of-the-art methods address this separately, first translating theorems and then generating proofs, creating a fundamental disconnect vis-a-vis true proof auto-formalization. This two-step process and its limitations were evident even in AlphaProof's silver-medal performance at the 2024 IMO, where problem statements needed manual translation before automated proof synthesis. We present ProofBridge, a unified framework for automatically translating entire NL theorems and proofs into Lean 4. At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem-proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant FL examples to guide translation. Our training ensures that NL-FL theorems (and their proofs) are mapped close together in this space if and only if the NL-FL pairs are semantically equivalent. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean's type checker and semantic equivalence feedback to ensure both syntactic correctness and semantic fidelity. Experiments show substantial improvements in proof auto-formalization over strong baselines (including GPT-5, Gemini-2.5, Kimina-Prover, DeepSeek-Prover), with our retrieval-augmented approach yielding significant gains in semantic correctness (SC, via proving bi-directional equivalence) and type correctness (TC, via type-checking theorem+proof) across pass@k metrics on miniF2F-Test-PF, a dataset we curated. In particular, ProofBridge improves cross-modal retrieval quality by up to 3.28x Recall@1 over all-MiniLM-L6-v2, and achieves +31.14% SC and +1.64% TC (pass@32) compared to the baseline Kimina-Prover-RL-1.7B.
• Abstract（参考訳）: 人間による数学的定理と証明を自然言語(NL)からLean 4のような形式言語(FL)に変換することは、AIにとって長年、重要な課題だった。 ほとんどの最先端の手法は、これを別々に扱い、まずは定理を翻訳し、次に証明を生成し、基本的な解離(vis-a-vis true proof auto-formalization)を生成する。 この2段階のプロセスとその制限は2024 IMOにおけるAlphaProofの銀製医療性能においても明らかであり、問題文は自動証明合成の前に手動翻訳が必要であった。 ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳する統合フレームワークです。 中心となるのは、NL と FL (NL-FL) の定理保護対を共有意味空間に整列させ、意味論的に関連する FL の例を相互に検索し、翻訳をガイドする共同埋め込みモデルである。 我々のトレーニングは、NL-FL対が意味論的に同値である場合に限り、NL-FL定理(およびそれらの証明)がこの空間において密接にマッピングされることを保証する。 ProofBridgeは、検索強化された微調整と反復的証明修復を統合し、Leanの型チェッカーとセマンティック等価フィードバックを活用して、構文的正当性とセマンティック忠実性の両方を保証する。 GPT-5、Gemini-2.5、Kimina-Prover、DeepSeek-Proverを含む)による証明の自己形式化の大幅な改善が示され、我々の検索によるアプローチは、私たちがキュレートしたminiF2F-Test-PF上のpass@kメトリクスで、意味的正当性(SC、双方向同値証明)と型正当性(TC、型チェック定理+保護)を著しく向上させた。 特にProofBridgeは、すべてのMiniLM-L6-v2上で最大3.28倍のリコール@1を達成し、ベースラインのKimina-Prover-RL-1.7Bに比べて+31.14%のSCと+1.64%のTC(pass@32)を達成した。

関連論文リスト

• Hierarchical Attention Generates Better Proofs [8.676187819105298]
  注意機構を数学的推論構造に整合させる正規化手法であるtextbfHierarchical Attention を導入する。 提案手法は,基礎要素から高レベル概念への5段階階層を確立し,証明生成における構造化情報の流れを確実にする。
  論文  参考訳（メタデータ） (2025-04-27T10:35:05Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (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)

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

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