A Survey on Deep Learning for Theorem Proving
- URL: http://arxiv.org/abs/2404.09939v1
- Date: Mon, 15 Apr 2024 17:07:55 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 mathematical language to rigorous derivations in formal systems.
In recent years, the advancement of deep learning has sparked a surge of research exploring these techniques to enhance the process of theorem proving.
Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, seeking to catalyze further research endeavors in this rapidly growing field.
- 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 mathematical 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 pioneering 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) a meticulous summary of available datasets and strategies for data generation; iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art; 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, seeking to catalyze further research endeavors in this rapidly growing field.
Related papers
- 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) - Machine learning assisted exploration for affine Deligne-Lusztig
varieties [3.7863170254779335]
This paper presents a novel, interdisciplinary study that leverages a Machine Learning (ML) assisted framework to explore the geometry of affine Deligne-Lusztig varieties (ADLV)
The primary objective is to investigate the nonemptiness pattern, dimension and enumeration of irreducible components of ADLV.
We provide a full mathematical proof of a newly identified problem concerning a certain lower bound of dimension.
arXiv Detail & Related papers (2023-08-22T11:12:53Z) - A Systematic Survey in Geometric Deep Learning for Structure-based Drug
Design [63.30166298698985]
Structure-based drug design (SBDD) utilizes the three-dimensional geometry of proteins to identify potential drug candidates.
Recent developments in geometric deep learning, focusing on the integration and processing of 3D geometric data, have greatly advanced the field of structure-based drug design.
arXiv Detail & Related papers (2023-06-20T14:21:58Z) - Rethinking Complex Queries on Knowledge Graphs with Neural Link
Predictors [65.56849255423866]
We propose a new neural-symbolic method to support end-to-end learning using complex queries with provable reasoning capability.
We develop a new dataset containing ten new types of queries with features that have never been considered.
Our method outperforms previous methods significantly in the new dataset and also surpasses previous methods in the existing dataset at the same time.
arXiv Detail & Related papers (2023-04-14T11:35:35Z) - Causal Reasoning Meets Visual Representation Learning: A Prospective
Study [117.08431221482638]
Lack of interpretability, robustness, and out-of-distribution generalization are becoming the challenges of the existing visual models.
Inspired by the strong inference ability of human-level agents, recent years have witnessed great effort in developing causal reasoning paradigms.
This paper aims to provide a comprehensive overview of this emerging field, attract attention, encourage discussions, bring to the forefront the urgency of developing novel causal reasoning methods.
arXiv Detail & Related papers (2022-04-26T02:22:28Z) - 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) - Deep Learning for Road Traffic Forecasting: Does it Make a Difference? [6.220008946076208]
This paper focuses on critically analyzing the state of the art in what refers to the use of Deep Learning for this particular ITS research area.
A posterior critical analysis is held to formulate questions and trigger a necessary debate about the issues of Deep Learning for traffic forecasting.
arXiv Detail & Related papers (2020-12-02T15:56:11Z) - 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.