A Survey on Deep Learning for Theorem Proving

• URL: http://arxiv.org/abs/2404.09939v3
• Date: Thu, 22 Aug 2024 03:56:45 GMT
• Title: A Survey on Deep Learning for Theorem Proving
• Authors: Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si,
• Abstract summary: Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. 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.
• Score: 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.

Related papers

• A Controlled Study on Long Context Extension and Generalization in LLMs [85.4758128256142]
  Broad textual understanding and in-context learning require language models that utilize full document contexts. Due to the implementation challenges associated with directly training long-context models, many methods have been proposed for extending models to handle long contexts. We implement a controlled protocol for extension methods with a standardized evaluation, utilizing consistent base models and extension data.
  arXiv  Detail & Related papers  (2024-09-18T17:53:17Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Embedding Knowledge for Document Summarization: A Survey [66.76415502727802]
  Previous works proved that knowledge-embedded document summarizers excel at generating superior digests. We propose novel to recapitulate knowledge and knowledge embeddings under the document summarization view.
  arXiv  Detail & Related papers  (2022-04-24T04:36:07Z)
• Faithfulness in Natural Language Generation: A Systematic Survey of Analysis, Evaluation and Optimization Methods [48.47413103662829]
  Natural Language Generation (NLG) has made great progress in recent years due to the development of deep learning techniques such as pre-trained language models. However, the faithfulness problem that the generated text usually contains unfaithful or non-factual information has become the biggest challenge.
  arXiv  Detail & Related papers  (2022-03-10T08:28:32Z)
• Learning Topic Models: Identifiability and Finite-Sample Analysis [6.181048261489101]
  We propose a maximum likelihood estimator (MLE) of latent topics based on a specific integrated likelihood. We conclude with empirical studies on both simulated and real datasets.
  arXiv  Detail & Related papers  (2021-10-08T16:35:42Z)
• Deep Learning Schema-based Event Extraction: Literature Review and Current Trends [60.29289298349322]
  Event extraction technology based on deep learning has become a research hotspot. This paper fills the gap by reviewing the state-of-the-art approaches, focusing on deep learning-based models.
  arXiv  Detail & Related papers  (2021-07-05T16:32:45Z)
• Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version) [4.111899441919164]
  This paper studies global features in selected problems and their proofs. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)"
  arXiv  Detail & Related papers  (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) is a general methodology for extracting self-supervised data from kernel-level proof terms for co-training. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.
  arXiv  Detail & Related papers  (2021-02-11T18:59:24Z)
• A Survey on Text Classification: From Shallow to Deep Learning [83.47804123133719]
  The last decade has seen a surge of research in this area due to the unprecedented success of deep learning. This paper fills the gap by reviewing the state-of-the-art approaches from 1961 to 2021. We create a taxonomy for text classification according to the text involved and the models used for feature extraction and classification.
  arXiv  Detail & Related papers  (2020-08-02T00:09:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.