摘要翻译：
当使用自动推理作为大理论形式证明开发的工具时，聪明的前提选择是必不可少的。在复杂数学库中进行前提选择的一个很好的方法是将机器学习应用于大型证明语料库。这项工作在两个方面发展了基于学习的前提选择。首先，对现有的高层形式化数学证明进行了最小依赖分析，建立了大量的证明依赖知识库，为基于ATP的再验证和训练前提选择算法提供了精确的数据。其次，提出并实现了一种基于核方法的前提选择机器学习算法。为了评估这两种技术的影响，我们构建了一个由2078个大理论数学问题组成的基准，扩展了旧的MPTP挑战基准。这些技术的综合效果导致在基准上比吸血鬼/正弦最先进的大型理论自动推理系统提高了50%。
---
英文标题：
《Premise Selection for Mathematics by Corpus Analysis and Kernel Methods》
---
作者：
Jesse Alama, Tom Heskes, Daniel K\"uhlwein, Evgeni Tsivtsivadze, and
  Josef Urban
---
最新提交年份：
2012
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Machine Learning        机器学习
分类描述：Papers on all aspects of machine learning research (supervised, unsupervised, reinforcement learning, bandit problems, and so on) including also robustness, explanation, fairness, and methodology. cs.LG is also an appropriate primary category for applications of machine learning methods.
关于机器学习研究的所有方面的论文（有监督的，无监督的，强化学习，强盗问题，等等），包括健壮性，解释性，公平性和方法论。对于机器学习方法的应用，CS.LG也是一个合适的主要类别。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. A good method for premise selection in complex mathematical libraries is the application of machine learning to large corpora of proofs. This work develops learning-based premise selection in two ways. First, a newly available minimal dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed,extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50% improvement on the benchmark over the Vampire/SInE state-of-the-art system for automated reasoning in large theories.
---
PDF链接：
https://arxiv.org/pdf/1108.3446