論文の概要: A Survey on Deep Learning for Theorem Proving

• arxiv url: http://arxiv.org/abs/2404.09939v2
• Date: Tue, 6 Aug 2024 14:30:11 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-07 19:02:36.757600
• Title: A Survey on Deep Learning for Theorem Proving
• Title（参考訳）: 定理証明のための深層学習に関する調査研究
• Authors: Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si,
• Abstract要約: 定理証明は数学の基本的な側面であり、自然言語における非公式な推論から形式体系における厳密な導出にまで及ぶ。 ディープラーニング、特に大きな言語モデルの出現は、定理証明のプロセスを強化するためにこれらの技術を探究する研究の顕著な急増を引き起こした。
• 参考スコア（独自算出の注目度）: 16.28502772608166
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a comprehensive survey of deep learning for theorem proving by offering (i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; (ii) an extensive summary of curated datasets and strategies for synthetic data generation; (iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art methods; and (iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, inspiring and catalyzing further research endeavors in this rapidly growing field. A curated list of papers is available at https://github.com/zhaoyu-li/DL4TP.
• Abstract（参考訳）: 定理証明は数学の基本的な側面であり、自然言語における非公式な推論から形式体系における厳密な導出にまで及ぶ。 近年、ディープラーニングの進歩、特に大規模言語モデルの台頭は、これらの手法を探求し、定理証明のプロセスを強化する顕著な研究の急増を引き起こしている。 本稿では,提案する定理証明のためのディープラーニングに関する包括的調査について述べる。 一 自己書式化、前提選択、証明工程生成、証明探索等の様々な業務における既存のアプローチの徹底的な見直し (二 合成データ生成のためのキュレートされたデータセット及び戦略の広範な概要 三 評価指標の詳細な分析及び最先端手法の性能 (四)持続的課題と今後の探査への有望な道についての批判的議論。 我々の調査は、この急速に成長する分野におけるさらなる研究の成果を実証し、刺激し、触媒する深層学習アプローチの基盤となる基準として機能することを目的としている。 キュレートされた論文のリストはhttps://github.com/zhaoyu-li/DL4TPで公開されている。

関連論文リスト

• A Controlled Study on Long Context Extension and Generalization in LLMs [85.4758128256142]
  広義のテキスト理解とテキスト内学習は、完全な文書コンテキストを利用する言語モデルを必要とする。 長期コンテキストモデルを直接訓練する際の実装上の課題のため、長期コンテキストを扱うためにモデルを拡張する多くの方法が提案されている。 我々は,一貫したベースモデルと拡張データを利用して,標準化された評価による拡張メソッドの制御プロトコルを実装した。
  論文  参考訳（メタデータ） (2024-09-18T17:53:17Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Geometric Deep Learning for Structure-Based Drug Design: A Survey [83.87489798671155]
  構造に基づく薬物設計(SBDD)は、タンパク質の3次元幾何学を利用して、潜在的な薬物候補を特定する。 近年の幾何学的深層学習の進歩は、3次元幾何学的データを効果的に統合・処理し、この分野を前進させてきた。
  論文  参考訳（メタデータ） (2023-06-20T14:21:58Z)
• Embedding Knowledge for Document Summarization: A Survey [66.76415502727802]
  従来の研究は、知識を組み込んだ文書要約器が優れた消化器を生成するのに優れていたことを証明した。 本稿では,文書要約ビューに基づいて,知識と知識の埋め込みを再カプセル化する手法を提案する。
  論文  参考訳（メタデータ） (2022-04-24T04:36:07Z)
• Learning Topic Models: Identifiability and Finite-Sample Analysis [6.181048261489101]
  本稿では,特定の統合可能性に基づく潜在トピックの最大確率推定器(MLE)を提案する。 シミュレーションと実データの両方について実証的研究を行った。
  論文  参考訳（メタデータ） (2021-10-08T16:35:42Z)
• Deep Learning Schema-based Event Extraction: Literature Review and Current Trends [60.29289298349322]
  ディープラーニングに基づくイベント抽出技術が研究ホットスポットとなっている。 本稿では,ディープラーニングモデルに焦点をあて,最先端のアプローチを見直し,そのギャップを埋める。
  論文  参考訳（メタデータ） (2021-07-05T16:32:45Z)
• Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version) [4.111899441919164]
  本稿では,選択問題におけるグローバル特徴とその証明について検討する。 研究対象の課題は"axiom(s)"と" rule(s) imply goal(s)"の広義の形式である。
  論文  参考訳（メタデータ） (2021-04-28T09:09:20Z)
• 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)
• A Survey on Text Classification: From Shallow to Deep Learning [83.47804123133719]
  過去10年は、ディープラーニングが前例のない成功を収めたために、この分野の研究が急増している。 本稿では,1961年から2021年までの最先端のアプローチを見直し,そのギャップを埋める。 特徴抽出と分類に使用されるテキストとモデルに基づいて,テキスト分類のための分類を作成する。
  論文  参考訳（メタデータ） (2020-08-02T00:09:03Z)

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

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