論文の概要: HyperTree Proof Search for Neural Theorem Proving

• arxiv url: http://arxiv.org/abs/2205.11491v1
• Date: Mon, 23 May 2022 17:49:55 GMT
• ステータス: 処理完了
• システム内更新日: 2022-05-24 18:04:54.952533
• Title: HyperTree Proof Search for Neural Theorem Proving
• Title（参考訳）: ニューラル定理証明のためのハイパートレー証明
• Authors: Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aur\'elien Rodriguez, Timoth\'ee Lacroix
• Abstract要約: 本稿では,変圧器を用いた自動定理証明のためのオンライン学習手順を提案する。 我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。 HTPSだけでは、アノテートされた証明に基づいて訓練されたモデルがメタマス定理の65.4%を証明し、GPT-fにより56.5%の先行状態を著しく上回ることを示した。
• 参考スコア（独自算出の注目度）: 14.677400513932852
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by the recent success of AlphaZero. Our model learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.
• Abstract（参考訳）: 本稿では,変圧器を用いた自動定理証明器のオンライン学習手順を提案する。 我々の手法は、最近AlphaZeroの成功に触発された新しい検索アルゴリズムHyperTree Proof Search (HTPS)を活用する。 我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。 本稿では,複雑性が増大する3つの環境において,パイプラインの主なコンポーネントの詳細な改善について報告する。 特に、HTPSだけでは、注釈付き証明に基づいて訓練されたモデルがメタマス定理の保留集合の65.4%を証明し、GPT-fにより56.5%の先行状態よりも著しく優れていることを示す。 これらの証明されていない定理のオンライントレーニングは精度を82.6%に向上させる。 同様の計算予算で、リーンベースの miniF2F-curriculum データセットの精度を 31% から 42% に改善します。

関連論文リスト

• The Surprising Effectiveness of Test-Time Training for Abstract Reasoning [64.36534512742736]
  モデル推論能力向上のためのメカニズムとして,テストタイムトレーニング(TTT)の有効性を検討する。 TTTはARCタスクのパフォーマンスを大幅に改善し、ベースとなる微調整モデルと比較して最大6倍の精度向上を実現した。 本研究は,ニューラルネットワークモデルにおける抽象的推論改善の道筋として,明示的な記号探索が唯一の道ではないことを示唆している。
  論文  参考訳（メタデータ） (2024-11-11T18:59:45Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• 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)
• LOT: Layer-wise Orthogonal Training on Improving $\ell_2$ Certified Robustness [14.206377940235091]
  近年の研究では、リプシッツ制約によるディープニューラルネットワーク(DNN)のトレーニングは、対向的ロバスト性や安定性などのモデル特性を高めることができることが示されている。 本研究では,1-Lipschitz畳み込み層を効果的に学習するための層ワイド直交訓練法(LOT)を提案する。 LOTは、決定論的l2証明されたロバスト性に関して、ベースラインを著しく上回り、より深いニューラルネットワークにスケールすることを示す。
  論文  参考訳（メタデータ） (2022-10-20T22:31:26Z)
• 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)

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

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