Learning Guided Automated Reasoning: A Brief Survey

TL;DR

This survey reviews how machine learning techniques are integrated into automated reasoning systems to improve proof search, guidance, and learning from large corpora of formal proofs, highlighting recent advances and challenges.

Contribution

It provides a comprehensive overview of the intersection of machine learning and automated reasoning, emphasizing new methods for proof guidance and large-scale proof corpus training.

Findings

Machine learning enhances proof guidance in automated theorem proving.

Large proof corpora can be used to bootstrap more advanced reasoning systems.

AI methods improve premise selection and symbolic classification in reasoning tasks.

Abstract

Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported by the notion of logically valid proof allows one to train machine learning systems on large reasoning corpora. Such bodies of proof are usually correct by construction and when combined with more and more precise trained guidance they can be boostrapped into very large corpora, with increasingly long reasoning chains and possibly novel proof ideas. In this paper we provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them. These include premise selection, proof guidance in several settings, AI systems and feedback loops iterating between reasoning and learning, and symbolic classification problems.