权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Machine Learning in Automated Theorem Proving

自动定理证明中的机器学习

基本信息

批准号：
2119928
负责人：
金额：
--
依托单位：
University of Cambridge
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2019
资助国家：
英国
起止时间：
2019 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=studentship-2119928
关键词：
Machine Learning Automated Theorem Proving

项目摘要

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.

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