論文の概要: 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% に改善します。
関連論文リスト
- LOT: Layer-wise Orthogonal Training on Improving $\ell_2$ Certified
Robustness [14.206377940235091]
近年の研究では、リプシッツ制約によるディープニューラルネットワーク(DNN)のトレーニングは、対向的ロバスト性や安定性などのモデル特性を高めることができることが示されている。
本研究では,1-Lipschitz畳み込み層を効果的に学習するための層ワイド直交訓練法(LOT)を提案する。
LOTは、決定論的l2証明されたロバスト性に関して、ベースラインを著しく上回り、より深いニューラルネットワークにスケールすることを示す。
論文 参考訳(メタデータ) (2022-10-20T22:31:26Z) - DeBERTaV3: Improving DeBERTa using ELECTRA-Style Pre-Training with
Gradient-Disentangled Embedding Sharing [117.41016786835452]
本稿では,DeBERTaモデルの改良を目的とした,事前学習型言語モデルDeBERTaV3を提案する。
ELECTRAでのバニラ埋め込み共有は、トレーニング効率とモデルパフォーマンスを損なう。
そこで本研究では、タグ・オブ・ウォーのダイナミクスを回避するために、新しい勾配距離の埋め込み方式を提案する。
論文 参考訳(メタデータ) (2021-11-18T06:48:00Z) - LGD: Label-guided Self-distillation for Object Detection [59.9972914042281]
我々はLGD(Label-Guided Self-Distillation)と呼ばれる汎用物体検出のための最初の自己蒸留フレームワークを提案する。
本フレームワークは, 学習知識を得るために, スパースラベル-外観符号化, オブジェクト間関係適応, オブジェクト内知識マッピングを含む。
従来の教師ベースのFGFIと比較すると、LGDは予習された教師を必要とせず、本質的な学生学習よりも51%低い訓練コストで性能が向上する。
論文 参考訳(メタデータ) (2021-09-23T16:55:01Z) - Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。
我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
論文 参考訳(メタデータ) (2021-06-07T18:35:57Z) - 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) - Towards Practical Lipreading with Distilled and Efficient Models [57.41253104365274]
ニューラルネットワークの復活により、リリーディングは多くの進歩を目の当たりにした。
最近の研究は、最適なアーキテクチャを見つけるか、一般化を改善することで、パフォーマンスを改善するといった側面に重点を置いている。
現在の方法論と、実践的なシナリオにおける効果的なリップリーディングのデプロイ要件との間には、依然として大きなギャップがあります。
まず, LRW と LRW-1000 をそれぞれ 88.5% と 46.6% に比例して, 最先端の性能を高めることを提案する。
論文 参考訳(メタデータ) (2020-07-13T16:56:27Z) - DrNAS: Dirichlet Neural Architecture Search [88.56953713817545]
ディリクレ分布をモデルとした連続緩和型混合重みをランダム変数として扱う。
最近開発されたパスワイズ微分により、ディリクレパラメータは勾配に基づく一般化で容易に最適化できる。
微分可能なNASの大きなメモリ消費を軽減するために, 単純かつ効果的な進行学習方式を提案する。
論文 参考訳(メタデータ) (2020-06-18T08:23:02Z) - Compounding the Performance Improvements of Assembled Techniques in a
Convolutional Neural Network [6.938261599173859]
基本CNNモデルの精度とロバスト性を改善する方法について述べる。
提案したResNet-50は、トップ1の精度を76.3%から82.78%、mCEを76.0%から48.9%、mFRを57.7%から32.3%に改善した。
CVPR 2019でiFood Competition Fine-Grained Visual Recognitionで1位を獲得した。
論文 参考訳(メタデータ) (2020-01-17T12:42:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。