論文の概要: REFACTOR: Learning to Extract Theorems from Proofs

• arxiv url: http://arxiv.org/abs/2402.17032v1
• Date: Mon, 26 Feb 2024 21:21:30 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-28 18:34:38.456226
• Title: REFACTOR: Learning to Extract Theorems from Proofs
• Title（参考訳）: REFACTOR: 証明から理論を抽出する学習
• Authors: Jin Peng Zhou, Yuhuai Wu, Qiyang Li, Roger Grosse
• Abstract要約: 我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。 新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。 また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
• 参考スコア（独自算出の注目度）: 29.44286369265644
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Human mathematicians are often good at recognizing modular and reusable theorems that make complex mathematical results within reach. In this paper, we propose a novel method called theoREm-from-prooF extrACTOR (REFACTOR) for training neural networks to mimic this ability in formal mathematical theorem proving. We show on a set of unseen proofs, REFACTOR is able to extract 19.6% of the theorems that humans would use to write the proofs. When applying the model to the existing Metamath library, REFACTOR extracted 16 new theorems. With newly extracted theorems, we show that the existing proofs in the MetaMath database can be refactored. The new theorems are used very frequently after refactoring, with an average usage of 733.5 times, and help shorten the proof lengths. Lastly, we demonstrate that the prover trained on the new-theorem refactored dataset proves more test theorems and outperforms state-of-the-art baselines by frequently leveraging a diverse set of newly extracted theorems. Code can be found at https://github.com/jinpz/refactor.
• Abstract（参考訳）: 人間の数学者は、しばしば複雑な数学的結果をもたらすモジュラーで再利用可能な定理を認識するのが得意である。 本稿では,形式的数理定理証明において,ニューラルネットワークを訓練し,その能力を模倣する新しい手法である theorem-from-proof extractor (refactor) を提案する。 未確認の証明のセットで、REFACTORは人間が証明を書くのに使用する定理の19.6%を抽出することができる。 このモデルを既存のMetamathライブラリに適用する際、REFACTORは16の新しい定理を抽出した。 新たに抽出された定理により,MetaMathデータベースの既存の証明がリファクタリング可能であることを示す。 新しい定理は、リファクタリング後に733.5回の平均使用量で非常に頻繁に使用され、証明の長さの短縮に役立つ。 最後に,新理論リファクターデータセットでトレーニングされた証明者は,新たに抽出された様々な定理を頻繁に活用することにより,より多くのテスト定理を証明し,最先端のベースラインを上回ることを実証する。 コードはhttps://github.com/jinpz/refactor.orgにある。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• miniCTX: Neural Theorem Proving with (Long-)Contexts [19.51651334079961]
  miniCTXは、トレーニング中に見えない新しい文脈に依存する形式的な数学的定理を証明するモデルの能力をテストする。 miniCTXには、実際のリーンプロジェクトと教科書に由来する定理が含まれており、それぞれに数万のトークンにまたがるコンテキストが関連付けられています。
  論文  参考訳（メタデータ） (2024-08-05T20:19:18Z)
• 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)
• LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
  LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。 LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。 我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
  論文  参考訳（メタデータ） (2023-10-01T12:47:59Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。 TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
  論文  参考訳（メタデータ） (2023-05-21T17:51:35Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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