論文の概要: 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で公開されている。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - Machine learning assisted exploration for affine Deligne-Lusztig
varieties [3.7863170254779335]
本稿では,ADLV(Affine Deligne-Lusztig variety)の幾何学を探索するために,機械学習支援フレームワークを活用した学際研究を提案する。
主な目的は, ADLVの既約成分の空白パターン, 寸法, 列挙について検討することである。
我々は、ある下界の次元に関する新たに特定された問題の完全な数学的証明を提供する。
論文 参考訳(メタデータ) (2023-08-22T11:12:53Z) - A Systematic Survey in Geometric Deep Learning for Structure-based Drug
Design [63.30166298698985]
構造に基づく薬物設計(SBDD)は、タンパク質の3次元幾何学を利用して、潜在的な薬物候補を特定する。
幾何学的深層学習の最近の進歩は、3次元幾何データの統合と処理に焦点をあてて、構造に基づく薬物設計の分野を大いに進歩させてきた。
論文 参考訳(メタデータ) (2023-06-20T14:21:58Z) - Rethinking Complex Queries on Knowledge Graphs with Neural Link
Predictors [65.56849255423866]
本稿では,証明可能な推論能力を備えた複雑なクエリを用いたエンドツーエンド学習を支援するニューラルシンボリック手法を提案する。
これまでに検討されていない10種類の新しいクエリを含む新しいデータセットを開発する。
提案手法は,新しいデータセットにおいて先行手法を著しく上回り,既存データセットにおける先行手法を同時に上回っている。
論文 参考訳(メタデータ) (2023-04-14T11:35:35Z) - Causal Reasoning Meets Visual Representation Learning: A Prospective
Study [117.08431221482638]
解釈可能性の欠如、堅牢性、分布外一般化が、既存の視覚モデルの課題となっている。
人間レベルのエージェントの強い推論能力にインスパイアされた近年では、因果推論パラダイムの開発に多大な努力が注がれている。
本稿では,この新興分野を包括的に概観し,注目し,議論を奨励し,新たな因果推論手法の開発の急激さを先導することを目的とする。
論文 参考訳(メタデータ) (2022-04-26T02:22:28Z) - 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) - Deep Learning for Road Traffic Forecasting: Does it Make a Difference? [6.220008946076208]
本稿では,このITS研究領域におけるDeep Learningの活用に言及した技術の現状を批判的に分析することに焦点を当てる。
後続の批判分析は、交通予測のためのディープラーニングの問題について、質問を定式化し、必要な議論を引き起こす。
論文 参考訳(メタデータ) (2020-12-02T15:56:11Z) - A Survey on Text Classification: From Shallow to Deep Learning [83.47804123133719]
過去10年は、ディープラーニングが前例のない成功を収めたために、この分野の研究が急増している。
本稿では,1961年から2021年までの最先端のアプローチを見直し,そのギャップを埋める。
特徴抽出と分類に使用されるテキストとモデルに基づいて,テキスト分類のための分類を作成する。
論文 参考訳(メタデータ) (2020-08-02T00:09:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。