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.

翻译：自动定理证明器和形式化证明助手是通用的推理系统，理论上能够证明任意难度的定理，从而解决可归约为数学和逻辑推理的任意问题。然而在实践中，这类系统面临巨大的组合爆炸问题，因此包含大量启发式算法和决策点，这些因素显著影响其性能。这为训练有素的机器学习预测器提供了机遇——它们可以引导此类推理系统的工作。反之，基于逻辑有效证明概念的演绎搜索，使得我们能够在大型推理语料库上训练机器学习系统。这类证明语料库通常由构造保证其正确性，当与日益精准的训练引导相结合时，可自举生成超大规模语料库，其中包含不断增长的推理链以及可能全新的证明思路。本文概述了多个自动化推理与定理证明领域，以及迄今为其开发的相应学习与人工智能方法，包括前提选择、多场景下的证明引导、人工智能系统及其在推理与学习之间迭代的反馈回路，以及符号分类问题。