Learning from Multiple Proofs: First Experiments
Learning from Multiple Proofs: First Experiments
复制标题
从多重证明中学习：第一次实验
DOI：
10.29007/nb2g
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
J. Urban
中科院分区：
文献类型：
--
作者：
D. Kühlwein;J. Urban
数学教科书通常仅在大多数定理中提供一个证明。但是，对于第阶逻辑，每个定理都有一定的证据，数学家经常意识到（甚至发明新的）重要的替代证明，并将此类知识用于（横向）思考新问题。在本文中，我们开始探讨如何将多个（人类和ATP）证明的明确知识用于大理论数学中的基于学习的前提选择算法。几种方法及其组合被否定，并且在MPTP2078大理论基准上评估了ATP性能的ECT。我们的第一个信息是，用于学习解决的问题的数量，用于学习的证据，证明的质量比数量更重要。
Mathematical textbooks typically present only one proof for most of the theorems. However, there are innitely many proofs for each theorem in rst-order logic, and mathematicians are often aware of (and even invent new) important alternative proofs and use such knowledge for (lateral) thinking about new problems. In this paper we start exploring how the explicit knowledge of multiple (human and ATP) proofs of the same theorem can be used in learning-based premise selection algorithms in large-theory mathematics. Several methods and their combinations are dened, and their eect on the ATP performance is evaluated on the MPTP2078 large-theory benchmark. Our rst ndings are that the proofs used for learning signicantly inuence the number of problems solved, and that the quality of the proofs is more important than the quantity.