論文の概要: Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
- arxiv url: http://arxiv.org/abs/2606.12594v1
- Date: Wed, 10 Jun 2026 18:43:11 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-12 15:55:27.412167
- Title: Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
- Title（参考訳）: Pythagoras-Prover: 拡張されたリーン形式化による効率的な形式証明の促進
- Authors: Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia,
- Abstract要約: Pythagoras-Prover(ピタゴラス・プロバー)は、実用的な計算予算のために開発された、リーンの定理プローバーの計算効率のよいファミリーである。
学習効率を向上させるために、カリキュラムSFTの簡単で中堅な問題に階層化されたリーン検証コーパスを構築します。
Augmented Lean Formalisation (ALF)も導入しています。
- 参考スコア（独自算出の注目度）: 27.324913853284404
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.
- Abstract（参考訳）: 現代のリーンの定理プローバーは、厳密なトレーニングと推論計算でのみ強力な性能を達成し、部分的には証明データ不足と公式な証明探索の長い推論トレースによって駆動され、教師付き微調整(SFT)とサンプリングコストの両方を発生させる。
我々はPythagoras-Proverを紹介した。Pythagoras-Proverは、実用的な計算予算のために構築された、計算効率のよいLean定理プローバーのオープンソースファミリである。
4Bおよび32Bパラメータの自己回帰モデルと、推論時にリーン証明を反復的に洗練する最初の概念拡散ベースの証明器(4B)である。
学習効率を向上させるために、我々は、カリキュラムSFTの簡単で中堅な問題に階層化されたリーン検証コーパスを構築します。
SFT中、動的証明推論フィルタリングスキームは、各インスタンスを8kのコンテキスト予算内に保持しながら、情報的証明トレースを保存する。
また、Augmented Lean Formalisation (ALF)を導入し、未確認のコーパスをフォーマルなステートメントの変種に拡張します。
形式的な文字を保存しながら既知の問題を摂動することで、ALFはステートメントの表面形式への依存を減らす。
実証的には、Pythagoras-Prover-4BはMiniF2F-Testのパス@32(86.1%対82.4%)でDeepSeek-Prover-V2-671Bを上回り、167倍のパラメータを持つ。
我々の32Bは依然として最強であり、4Bは最先端のGoedel-Prover-V2-32Bと一致します。
関連論文リスト
- OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。
エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。
OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
論文 参考訳（メタデータ） (2026-05-17T06:39:05Z) - LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning [46.294745464571456]
LongCat-Flash-Proverはエージェントツール統合推論のためのオープンソースのMoEモデルである。
これは、自己形式化と定理証明の両方において、オープンウェイトモデルのための新しい最先端状態を設定する。
MiniF2F-Testのパスレートは97.1%で、72の推論予算しか使用していない。
論文 参考訳（メタデータ） (2026-03-22T05:16:09Z) - ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。
中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。
我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
論文 参考訳（メタデータ） (2025-10-17T14:20:50Z) - Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction [95.91743732150233]
一連のオープンソースの言語モデルであるGoedel-Prover-V2は、自動定理の新たな最先端を証明した。
我々は、より複雑な定理をマスターするためにモデルを訓練することの困難さを増す合成タスクを生成する。
Goedel-Prover-V2-32Bは、標準モードのpass@32でMiniF2Fの88.1%、自己補正モードの90.4%を達成する。
論文 参考訳（メタデータ） (2025-08-05T16:28:22Z) - 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) - STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。
STPは同時に、予想と証明という2つの役割を担っている。
私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
論文 参考訳（メタデータ） (2025-01-31T23:01:48Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。
我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。
我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-04T05:57:40Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。