論文の概要: Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

• arxiv url: http://arxiv.org/abs/2410.15748v1
• Date: Mon, 21 Oct 2024 08:04:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-22 13:12:40.499705
• Title: Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
• Title（参考訳）: Alchemy: シンボリック変異による理論実証能力の増幅
• Authors: Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, Ping Wei,
• Abstract要約: この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
• 参考スコア（独自算出の注目度）: 71.32761934724867
• License:
• Abstract: Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 5% absolute performance improvement on Leandojo benchmark. Additionally, our synthetic data achieve a 2.5% absolute performance gain on the out-of-distribution miniF2F benchmark. To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.
• Abstract（参考訳）: 経験豊富な専門家でさえ、形式的な証明を書くことは難しい。 ニューラル定理証明(NTP)の最近の進歩は、このプロセスの迅速化に有望であることを示している。 しかし、インターネット上で利用できる公式コーパスは一般的なテキストに比べて限られており、NTPにとって重大なデータ不足を招いている。 この問題に対処するために、この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成の一般的なフレームワークであるAlchemyを提案する。 具体的には、Mathlib 内の各候補定理に対して、書き直しや適用に使用できるすべてのイベーシブルな定理を識別する。 その後、文中の対応する項を同値な形式または先行形に置き換えることで、候補定理を変異させる。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。 さらに,大規模言語モデルのための拡張コーパスに対して,継続事前学習と教師付き微調整を行う。 実験の結果、Leandojoベンチマークで5%の絶対的なパフォーマンス改善を実現し、このアプローチの有効性を実証した。 さらに、我々の合成データは、アウト・オブ・ディストリビューションのminiF2Fベンチマークで2.5%の絶対的な性能向上を達成した。 さらなる知見を得るため、我々は合成データ合成と訓練パラダイムを総合的に分析し、強力な定理証明器を開発する上で貴重なガイダンスを提供する。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
  SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。 SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
  論文  参考訳（メタデータ） (2024-08-20T20:10:53Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35: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)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
  自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。 本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。 私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
  論文  参考訳（メタデータ） (2021-03-05T17:01:34Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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