論文の概要: REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

• arxiv url: http://arxiv.org/abs/2505.20613v1
• Date: Tue, 27 May 2025 01:26:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-28 17:05:58.335587
• Title: REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
• Title（参考訳）: REAL-Prover: 数学的推論のための検索可能なリーンプロバー
• Authors: Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai, Bin Dong,
• Abstract要約: 私たちはREAL-Proverという,Lean 4.0用の新たなオープンソースステップワイドな定理証明ツールを紹介します。 我々の証明者は、特に大学レベルの数学問題の解法における性能を高める。 実験では、教師付き微チューン定理のみを用いた証明器は23.7%の成功率で競合する結果が得られる。
• 参考スコア（独自算出の注目度）: 12.343823629674368
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL-Prover, a new open-source stepwise theorem prover for Lean 4 to push this boundary. This prover, based on our fine-tuned large language model (REAL-Prover-v1) and integrated with a retrieval system (Leansearch-PS), notably boosts performance on solving college-level mathematics problems. To train REAL-Prover-v1, we developed HERALD-AF, a data extraction pipeline that converts natural language math problems into formal statements, and a new open-source Lean 4 interactive environment (Jixia-interactive) to facilitate synthesis data collection. In our experiments, our prover using only supervised fine-tune achieves competitive results with a 23.7% success rate (Pass@64) on the ProofNet dataset-comparable to state-of-the-art (SOTA) models. To further evaluate our approach, we introduce FATE-M, a new benchmark focused on algebraic problems, where our prover achieves a SOTA success rate of 56.7% (Pass@64).
• Abstract（参考訳）: 今日では、フォーマルな定理の証明者は、高校や競技レベルの数学において顕著な進歩を遂げているが、より高度な数学に一般化するものはほとんどない。 本稿では,Lean 4の新たなステップワイズ定理証明ツールであるREAL-Proverを紹介し,その境界線を推し進める。 この証明は、我々の微調整された大言語モデル(REAL-Prover-v1)に基づいており、検索システム(Leansearch-PS)と統合されている。 REAL-Prover-v1をトレーニングするために,自然言語の数学問題を形式文に変換するデータ抽出パイプラインであるHERALD-AFと,合成データ収集を容易にするオープンソースのLean 4インタラクティブ環境(Jixia-Interactive)を開発した。 実験では,教師付きファインチューンのみを用いて,ProofNetデータセットとSOTA(State-of-the-art)モデルで23.7%の成功率(Pass@64)で競合する結果を得た。 提案手法を更に評価するため,代数問題に着目した新しいベンチマークであるFATE-Mを導入し,提案手法がSOTA成功率56.7%(Pass@64)を達成した。

関連論文リスト

• 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)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Teaching-Inspired Integrated Prompting Framework: A Novel Approach for Enhancing Reasoning in Large Language Models [8.370453544530914]
  大規模言語モデル(LLM)は、様々な領域で優れたパフォーマンスを示すが、算術的推論タスクに苦戦している。 近年の研究では,推理能力向上における迅速な設計手法の有効性が示されている。 本稿では,教師が指導する指導過程をエミュレートした,新しい効果的な指導インスパイアされた統合フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-10-10T16:02:36Z)
• 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)
• MathGenie: Generating Synthetic Data with Question Back-translation for Enhancing Mathematical Reasoning of LLMs [38.127313175508746]
  MathGenieは、小規模の問題解決データセットから多様で信頼性の高い数学問題を生成する新しい方法である。 7Bから70Bまでの各種事前学習モデルについて, 提案手法の有効性を検証するために, 新たなキュレートデータを用いて訓練を行った。 MathGenieLM-InternLM2はGSM8Kで87.7%、MATHで55.7%の精度を達成し、オープンソース言語モデルで最高のスコアを確保している。
  論文  参考訳（メタデータ） (2024-02-26T07:17:25Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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