arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1909.09137cs.AIcs.LG
收藏

基于高斯过程的贝叶斯最优决策

Bayesian Optimisation with Gaussian Processes for Premise Selection

University of Cambridge(剑桥大学)

Agnieszka Słowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson

摘要:

定理证明器中的启发式通常是参数化的。现代的定理证明器,如Vampire,利用了大量的算法来控制搜索空间的爆炸,从而需要优化大量的参数。在这个多维参数空间中的穷举搜索在大多数情况下是棘手的,然而证明器的性能高度依赖于参数分配。在这项工作中,我们引入了一个原则性的概率框架,在定理证明优化。我们目前的结果使用启发式的前提选择和正式证明(AFP)的档案作为案例研究。

英文摘要:

Heuristics in theorem provers are often parameterised. Modern theorem provers such as Vampire utilise a wide array of heuristics to control the search space explosion, thereby requiring optimisation of a large set of parameters. An exhaustive search in this multi-dimensional parameter space is intractable in most cases, yet the performance of the provers is highly dependent on the parameter assignment. In this work, we introduce a principled probablistic framework for heuristics optimisation in theorem provers. We present results using a heuristic for premise selection and The Archive of Formal Proofs (AFP) as a case study.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑