Machine Learning in Automated Theorem Proving

推理是一般智能的重要组成部分，但事实证明很难完全自动化。帮助人类专家的交互式证明器仍然比成功的全自动证明搜索更普遍。然而，在过去的几年中，全自动机器学习方法在过去需要人类监督和手工特征工程的几个推理挑战中设置了最先进的结果，例如机器翻译（Wu等人，2016）、视觉问答（Kahou等人，2017），算法任务的推理（Zaremba等人，2014），并擅长抽象战略游戏（银et al.，2016年）。其中一些任务与ATP中的主要瓶颈相似。例如，在游戏中获胜策略的选择以及证明定理所需的决策可以类似地建模为搜索问题。我的目标将是通过开发新的方法来解决这些挑战，以填补ATP中使用机器学习的空白。ATP中传统上需要人类监督的挑战，例如，通过选择最有用的数学陈述来证明猜想（前提选择），证明搜索的最佳策略的选择（启发式选择），或者将数学内容（例如，用LaTeX表示）语义相关地翻译成证明器的形式语言（自动形式化）。现代机器学习方法最近已经应用于所有提到的问题，并产生了有希望的结果，例如（Alemi et al.，2017）和（Bridge等人，2014年）。基于最先进的研究，我想探索使用强化学习方法来指导证明搜索，以及强大的学习算法（如深度神经网络）来提取最相关的特征，并限制决策过程的搜索空间。数学语句的语义精确表示研究有可能取得重大进展。我想通过在神经网络和自然语言处理的接口上开发新方法来为ATP的前景做出贡献，包括图形嵌入，这是表示数学公式的最自然的方式。特别是，我想研究更有表现力的高阶逻辑，使用开源数据集来评估新的基于机器学习的定理证明方法（Kaliszyk等人，2017）.总之，我努力通过使用机器学习中最有前途的进步来提高定理证明的自动化。由于EPSRC的学生身份，执行拟议的研究将使我能够为人工智能的关键方面做出贡献，以及使用ATP的应用领域，特别是安全关键的软件和硬件设计。此外，本研究旨在展示更好地理解和开发普遍适用的机器学习方法的步骤。

Reasoning is an essential component of a general intelligence, but has proven difficult to fully automate. Interactive provers that assist a human expert are still more prevalent than a successful fully-automated proof search. However, in the last years fully-automated Machine Learning methods set state-of-the-art results in several reasoning challenges that used to require human supervision and handcrafted feature engineering, e.g. machine translation (Wu et al., 2016), visual question answering (Kahou et al., 2017), reasoning on algorithmic tasks (Zaremba et al., 2014), and excelling at abstract strategy games (Silver et al., 2016). Some of these tasks draw similarities to the main bottlenecks in the ATP. For instance, the choice of the winning strategy in a game as well as decisions required to prove a theorem can be similarly modelled as search problems. My goal will be to address these challenges by developing new approaches to fill the gaps in ATP using Machine Learning.The challenges in ATP that traditionally require human supervision are posed, for instance, by selection of the most useful mathematical statements to prove a conjecture (premise selection), the choice of an optimal strategy for a proof search (heuristic selection), or semantically relevant translation of a mathematical content (e.g. expressed in LaTeX) to the formal language of a prover (auto-formalization). Modern Machine Learning methods have been recently applied to all of the problems mentioned, and yielded promising results, for instance (Alemi et al., 2017) and (Bridge et al., 2014). Based on the state-of-the-art research, I would like to explore the combination of employing Reinforcement Learning methods to guide a proof search, and powerful learning algorithms such as Deep Neural Networks to extract the most relevant features, and to restrict the search space for the decision process. There is a potential to make a significant progress in the research on semantically accurate representations of the mathematical statements. I would like to contribute to the ATP landscape by developing new methods at the interface of Neural Networks and Natural Language Processing, including graph embeddings that are the most natural way of representing mathematical formulae. In particular, I would like to investigate the more expressive Higher-order logic, using an open-source dataset released for the evaluation of new Machine Learning-based theorem proving methods (Kaliszyk et al., 2017).In conclusion, I strive to improve the automation of theorem proving by using the most promising advances in Machine Learning. Performing the proposed research thanks to the EPSRC studentship will allow me to contribute to the key aspect of artificial intelligence, as well as to the applied fields that employ ATP, notably to the safety-critical software and hardware design. Moreover, this research aims at showing steps towards a better understanding and development of generally applicable Machine Learning methods.