論文の概要: INT: An Inequality Benchmark for Evaluating Generalization in Theorem
Proving
- arxiv url: http://arxiv.org/abs/2007.02924v2
- Date: Sat, 3 Apr 2021 16:21:59 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-13 01:06:59.195377
- Title: INT: An Inequality Benchmark for Evaluating Generalization in Theorem
Proving
- Title(参考訳): INT: 定理証明の一般化を評価するための不等式ベンチマーク
- Authors: Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, Roger Grosse
- Abstract要約: 本稿では,エージェントの一般化能力をテストするために,INequality Theorem Proving benchmarkを提案する。
Int は定理と証明を生成する手順に基づいており、この手順のノブは6つの異なる種類の一般化を測ることができる。
次に,モンテカルロ木探索(MCTS)で拡張したエージェントを試験時に評価し,MCTSが新たな定理を証明できることを示す。
- 参考スコア(独自算出の注目度): 36.194330645092634
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In learning-assisted theorem proving, one of the most critical challenges is
to generalize to theorems unlike those seen at training time. In this paper, we
introduce INT, an INequality Theorem proving benchmark, specifically designed
to test agents' generalization ability. INT is based on a procedure for
generating theorems and proofs; this procedure's knobs allow us to measure 6
different types of generalization, each reflecting a distinct challenge
characteristic to automated theorem proving. In addition, unlike prior
benchmarks for learning-assisted theorem proving, INT provides a lightweight
and user-friendly theorem proving environment with fast simulations, conducive
to performing learning-based and search-based research. We introduce
learning-based baselines and evaluate them across 6 dimensions of
generalization with the benchmark. We then evaluate the same agents augmented
with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help
to prove new theorems.
- Abstract(参考訳): 学習支援定理証明において、最も重要な課題の1つは、訓練時に見られるものとは異なり、定理に一般化することである。
本稿では,エージェントの一般化能力をテストするために特別に設計されたINequality Theorem Proving benchmarkであるINTを紹介する。
INT は定理と証明を生成する手順に基づいており、この手順のノブは6つの異なる種類の一般化を測ることができる。
さらに、学習支援定理証明の以前のベンチマークとは異なり、INTは高速なシミュレーションを備えた軽量でユーザフレンドリな定理証明環境を提供する。
学習ベースラインを導入し、6次元の一般化をベンチマークで評価する。
次に,モンテカルロ木探索(MCTS)で拡張したエージェントを試験時に評価し,MCTSが新たな定理を証明できることを示す。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳(メタデータ) (2023-05-21T17:51:35Z) - Representer Theorems for Metric and Preference Learning: A Geometric
Perspective [0.0]
計量学習と選好学習を同時に行うための新しい代表者定理を得る。
本稿では,三重項比較によるメートル法学習の課題に対して,本フレームワークが適用可能であることを示す。
カーネル・ヒルベルト・スペースを再現する場合、学習問題の解をカーネル用語で表現できることを実証する。
論文 参考訳(メタデータ) (2023-04-07T16:34:25Z) - Synergies between Disentanglement and Sparsity: Generalization and
Identifiability in Multi-Task Learning [79.83792914684985]
我々は,最大スパース基底予測器が不整合表現をもたらす条件を提供する新しい識別可能性の結果を証明した。
この理論的な結果から,両レベル最適化問題に基づくアンタングル表現学習の実践的アプローチを提案する。
論文 参考訳(メタデータ) (2022-11-26T21:02:09Z) - Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。
我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
論文 参考訳(メタデータ) (2021-06-07T18:35:57Z) - TacticZero: Learning to Prove Theorems from Scratch with Deep
Reinforcement Learning [6.764610878007278]
深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。
我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。
このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
論文 参考訳(メタデータ) (2021-02-19T06:08:39Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z) - An Experimental Study of Formula Embeddings for Automated Theorem
Proving in First-Order Logic [13.633012068936894]
本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。
実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
論文 参考訳(メタデータ) (2020-02-02T16:07:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。