論文の概要: NanoProof: Open and Efficient Automated Theorem Proving in Lean 4

• arxiv url: http://arxiv.org/abs/2610.11605v1
• Date: Thu, 08 Oct 2026 09:49:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-10 02:36:53.936605
• Title: NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
• Title（参考訳）: NanoProof: リーン4で証明されたオープンで効率的な自動理論
• Abstract要約: NanoProofはLean 4.0の最初の分解された実行誘導定理証明である。 構造化された証明ツリーのデータセットを構築してリリースし、Lean 4の形式検証ツール内でプログラムによるインタラクションとデータ抽出を行うツールを提供しています。 NanoProofはMiniF2F-Testで50.8%のpass@16を達成した。
• 参考スコア（独自算出の注目度）: 0.5647577824219207
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof trees, as well as a tool for programmatic interaction and data extraction within the Lean 4 formal verifier. To support sustainable research, we focus on compute efficiency to facilitate accessible training and evaluation. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, exceeding the two closest systems of its class, HyperTree Proof Search and ABEL, at roughly 90x and 7x less compute, and using more than four orders of magnitude less compute than AlphaProof. Stronger open-weight provers exist, but they are fine-tuned from large pretrained language models and release neither training data nor pipeline; NanoProof shows that the factorized execution-guided class of provers can be rebuilt from scratch with modest resources.
• Abstract（参考訳）: トレーニングデータ、抽出ツール、トレーニングパイプライン、ウェイトがすべてリリースされ、オープンソースリソースを使ってエンドツーエンドで再現可能になります。 この目的のために、構造化された証明ツリーのデータセットを構築し、リリースし、Lean 4の形式検証ツール内でプログラムによるインタラクションとデータ抽出を行うツールを提供しています。 持続可能な研究を支援するため,我々は,アクセス可能なトレーニングと評価を容易にする計算効率に重点を置いている。 NanoProofはMiniF2F-Testで50.8%のpass@16を達成し、クラスの最も近い2つのシステムであるHyperTree Proof SearchとABELを約90倍、7倍の計算で上回り、AlphaProofより4桁以上少ない計算を使用する。 より強力なオープンウェイトプローバーは存在するが、それらは大きな事前訓練された言語モデルから微調整され、トレーニングデータもパイプラインもリリースしない。

関連論文リスト

• Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
  Pythagoras-Prover(ピタゴラス・プロバー)は、実用的な計算予算のために開発された、リーンの定理プローバーの計算効率のよいファミリーである。 学習効率を向上させるために、カリキュラムSFTの簡単で中堅な問題に階層化されたリーン検証コーパスを構築します。 Augmented Lean Formalisation (ALF)も導入しています。
  論文  参考訳（メタデータ） (2026-06-10T18:43:11Z)
• 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)
• MiniCPM4: Ultra-Efficient LLMs on End Devices [126.22958722174583]
  MiniCPM4は、エンドサイドデバイス向けに明示的に設計された高効率な大規模言語モデル(LLM)である。 この効率性は、モデルアーキテクチャ、トレーニングデータ、トレーニングアルゴリズム、推論システムという4つの重要な側面において、体系的な革新を通じて達成します。
  論文  参考訳（メタデータ） (2025-06-09T16:16:50Z)
• Leanabell-Prover: Posttraining Scaling in Formal Reasoning [26.534511088861446]
  本稿では, 自然言語の推論モデルにおけるブレークスルーと整合性を持たせることを目的として, ATPのポストトレーニング全体について検討する。 我々は,DeepSeek-Prover-v1.5やGoedel-Proverなど,既存のフォーマルプロバーの改良に成功した。
  論文  参考訳（メタデータ） (2025-04-08T15:15:26Z)
• 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)
• 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)
• 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)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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