論文の概要: HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2412.20735v2
• Date: Tue, 31 Dec 2024 10:48:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-03 11:36:45.902303
• Title: HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
• Title（参考訳）: HUNYUANPROVER: 自動定理証明のためのスケーラブルなデータ合成フレームワークとガイドツリー検索
• Authors: Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, Haitao Mi,
• Abstract要約: Hunyuan Proverは、LEAN4で証明された対話型自動定理のためにHunyuan 7Bから微調整された言語モデルである。 これは、現在のSOTA結果である65.9%と比較して、ミニF2Fテストで68.4%のパスを達成している。 私たちは30kの合成インスタンスのデータセットをオープンソースとして公開します。各インスタンスには、自然言語における元の質問、自動形式化による変換されたステートメント、HunyuanProverによる証明が含まれています。
• 参考スコア（独自算出の注目度）: 25.24149680681184
• License:
• Abstract: We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesize data with low cost. Besides, guided tree search algorithms are designed to enable effective ``system 2 thinking`` of the prover. HunyuanProver achieves state-of-the-art (SOTA) performances on major benchmarks. Specifically, it achieves a pass of 68.4% on the miniF2F-test compared to 65.9%, the current SOTA results. It proves 4 IMO statements (imo_1960_p2, imo_1962_p2}, imo_1964_p2 and imo_1983_p6) in miniF2F-test. To benefit the community, we will open-source a dataset of 30k synthesized instances, where each instance contains the original question in natural language, the converted statement by autoformalization, and the proof by HunyuanProver.
• Abstract（参考訳）: Hunyuan Proverは,LEAN4で証明された対話型自動定理に対して,Hunyuan 7Bから微調整された言語モデルである。 データ空間の問題を軽減するため、我々は低コストでデータを反復的に合成するスケーラブルなフレームワークを設計する。 さらに、誘導木探索アルゴリズムは、証明者の効果的な「システム2思考」を可能にするように設計されている。 HunyuanProverは、主要なベンチマークで最先端(SOTA)のパフォーマンスを達成する。 特に、現在のSOTAの結果である65.9%と比較して、miniF2F-testでは68.4%のパスを達成している。 4つのIMO文(imo_ 1960_p2, imo_ 1962_p2}, imo_ 1964_p2, imo_ 1983_p6)をminiF2F-testで証明する。 コミュニティの利益のために、私たちは30kの合成インスタンスのデータセットをオープンソース化します。各インスタンスには、自然言語での元の質問、自動形式化による変換されたステートメント、HunyuanProverによる証明が含まれています。

関連論文リスト

• EquiBench: Benchmarking Code Reasoning Capabilities of Large Language Models via Equivalence Checking [54.354203142828084]
  本稿では,大規模言語モデルのコード推論能力を評価する新しい手法として等価チェックの課題を提案する。 EquiBenchは、4つのプログラミング言語と6つの等価カテゴリにまたがる2400のプログラムペアのデータセットである。 その結果,OpenAI o3-miniの精度は78.0%と高いことがわかった。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification [11.115201117143929]
  本稿では,Coq用の完全自動合成証明ツールであるRangoを紹介する。 Rangoは関連する前提と、それに類似した証明を現在のプロジェクトから特定し、合成時にそれらを使用する。 評価の結果, Rangoが文脈に関連付けると, 証明された定理の数が47%増加することがわかった。
  論文  参考訳（メタデータ） (2024-12-18T17:08:42Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Source2Synth: Synthetic Data Generation and Curation Grounded in Real Data Sources [38.30192495271699]
  我々は、コストのかかる人的アノテーションに頼ることなく、LLMに新しいスキルを教えるために使用できる新しい方法、Source2 Synthを提案する。 Source2 Synthはカスタムデータソースを入力として、実世界のソースをベースとした中間的推論ステップを備えた合成データポイントを生成する。 マルチホップ質問応答(MHQA)とツール質問応答(TQA)の推論能力をテストする。
  論文  参考訳（メタデータ） (2024-09-12T17:39:08Z)
• 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)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Engineering an Efficient Boolean Functional Synthesis Engine [22.075107339383255]
  入力と出力の集合間のブール仕様が与えられたとき、関数合成の問題は、各出力を仕様が満たされるような入力の関数として合成することである。 関数合成のためのデータ駆動型フレームワークに対して,4つのアルゴリズム改良を提案する。 Manthan2はManthanに比べて実行時のパフォーマンスが大幅に向上した。
  論文  参考訳（メタデータ） (2021-08-12T13:01:49Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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