論文の概要: 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が新たな定理を証明できることを示す。

関連論文リスト

• 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)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Representer Theorems for Metric and Preference Learning: A Geometric Perspective [0.0]
  計量学習と選好学習を同時に行うための新しい代表者定理を得る。 本稿では,三重項比較によるメートル法学習の課題に対して,本フレームワークが適用可能であることを示す。 カーネル・ヒルベルト・スペースを再現する場合、学習問題の解をカーネル用語で表現できることを実証する。
  論文  参考訳（メタデータ） (2023-04-07T16:34:25Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。 我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
  論文  参考訳（メタデータ） (2021-06-07T18:35:57Z)
• 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)

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

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