Conference
Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).
| العنوان: | Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). |
|---|---|
| المؤلفون: | Slowik, Agnieszka, Mangla, Chaitanya, Jamnik, Mateja, Holden, Sean B, Paulson, Lawrence C |
| بيانات النشر: | AAAI Press Department of Computer Science And Technology //www.aaai.org/Library/AAAI/aaai20contents.php Proceedings of the AAAI Conference on Artificial Intelligence, 34(10) |
| سنة النشر: | 2022 |
| المجموعة: | Apollo - University of Cambridge Repository |
| الوصف: | 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. |
| نوع الوثيقة: | conference object |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | https://www.repository.cam.ac.uk/handle/1810/332827 |
| DOI: | 10.17863/CAM.80261 |
| الاتاحة: | https://www.repository.cam.ac.uk/handle/1810/332827 https://doi.org/10.17863/CAM.80261 |
| Rights: | Publisher's own licence |
| رقم الانضمام: | edsbas.94D1ADAB |
| قاعدة البيانات: | BASE |
| DOI: | 10.17863/CAM.80261 |
|---|