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.

自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。

学习引导的自动推理：简要调查

Learning Guided Automated Reasoning: A Brief Survey

Techniques combining machine learning with translation to automated reasoning
have recently become an important component of formal proof assistants. Such
"hammer" tech- niques complement traditional proof assistant automation as
implemented by tactics and decision procedures. In this paper we present a
unified proof assistant automation approach which attempts to automate the
selection of appropriate tactics and tactic-sequences com- bined with an
optimized small-scale hammering approach. We implement the technique as a
tactic-level automation for HOL4: TacticToe. It implements a modified
A*-algorithm directly in HOL4 that explores different tactic-level proof paths,
guiding their selection by learning from a large number of previous
tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids
translation to FOL, working directly on the HOL level. By combining tactic
prediction and premise selection, TacticToe is able to re-prove 39 percent of
7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy
solves 32 percent in the same amount of time.

本文介绍了一种用于 HOL4 TacticToe 的策略级自动化方法，将机器学习和翻译技术与自动定理证明辅助工具相结合，以探索不同的策略级证明路径，并且通过组合策略预测和前提选择，在 5 秒内重新证明了 7902 个 HOL4 定理中的 39％，效果显著。