MaLeCoP Machine Learning Connection Prover
MaLeCoP Machine Learning Connection Prover
复制标题
MaLeCoP 机器学习连接证明器
DOI：
10.1007/978-3-642-22119-4_21
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
P. Štěpánek
中科院分区：
文献类型：
--
作者：
J. Urban;J. Vyskočil;P. Štěpánek
基于所学知识的概率指导被添加到连接表演算中，并在精益 CoP 定理证明器之上实施，将其链接到外部顾问系统。在解决大型复杂理论中的许多问题的典型数学环境中，从成功的解决方案中学习可以本着 MaLARea 系统的精神指导定理证明尝试。在 MaLARea 中，基于学习的公理选择是在未经修改的定理证明器外部完成的，而在 MaLeCoP 中，基于学习的选择是在证明器内部完成的，并且知识学习与其应用之间的交互可以更加精细。这为在大型数学库上进一步构建和培训自学人工智能数学专家带来了有趣的可能性，其中一些是讨论的。初步实施是在 MPTP Challenge 大型理论基准上进行评估的。
Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the lean-CoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems in a large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLARea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP the learning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark.