TY - JOUR AU - SÅ‚owik, Agnieszka AU - Mangla, Chaitanya AU - Jamnik, Mateja AU - Holden, Sean B. AU - Paulson, Lawrence C. PY - 2020/04/03 Y2 - 2024/03/29 TI - Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract) JF - Proceedings of the AAAI Conference on Artificial Intelligence JA - AAAI VL - 34 IS - 10 SE - Student Abstract Track DO - 10.1609/aaai.v34i10.7232 UR - https://ojs.aaai.org/index.php/AAAI/article/view/7232 SP - 13919-13920 AB - <p>Modern theorem provers 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 probabilistic framework for heuristic optimisation in theorem provers. We present results using a heuristic for premise selection and the Archive of Formal Proofs (AFP) as a case study.</p> ER -