Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).
| cam.depositDate | 2022-01-19 | |
| cam.issuedOnline | 2020-04-03 | |
| cam.orpheus.success | Tue Feb 01 19:02:45 GMT 2022 - Embargo updated | |
| dc.contributor.author | Slowik, Agnieszka | |
| dc.contributor.author | Mangla, Chaitanya | |
| dc.contributor.author | Jamnik, Mateja | |
| dc.contributor.author | Holden, Sean B | |
| dc.contributor.author | Paulson, Lawrence C | |
| dc.contributor.orcid | Jamnik, Mateja [0000-0003-2772-2532] | |
| dc.contributor.orcid | Holden, Sean [0000-0001-7979-1148] | |
| dc.contributor.orcid | Paulson, Lawrence [0000-0003-0288-4279] | |
| dc.date.accessioned | 2022-01-21T00:31:28Z | |
| dc.date.available | 2022-01-21T00:31:28Z | |
| dc.date.issued | 2020 | |
| dc.date.updated | 2022-01-19T17:49:31Z | |
| dc.description.abstract | 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. | |
| dc.identifier.doi | 10.17863/CAM.80261 | |
| dc.identifier.isbn | 978-1-57735-823-7 | |
| dc.identifier.uri | https://www.repository.cam.ac.uk/handle/1810/332827 | |
| dc.language.iso | eng | |
| dc.publisher | AAAI Press | |
| dc.publisher.department | Department of Computer Science And Technology | |
| dc.publisher.url | https://www.aaai.org/Library/AAAI/aaai20contents.php | |
| dc.rights | Publisher's own licence | |
| dc.title | Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). | |
| dc.type | Conference Object | |
| dcterms.dateAccepted | 2019-12-04 | |
| prism.endingPage | 13920 | |
| prism.publicationDate | 2020 | |
| prism.publicationName | Proceedings of the AAAI Conference on Artificial Intelligence, 34(10) | |
| prism.startingPage | 13919 | |
| pubs.conference-name | AAAI 2020 | |
| pubs.licence-display-name | Apollo Repository Deposit Licence Agreement | |
| pubs.licence-identifier | apollo-deposit-licence-2-1 | |
| rioxxterms.version | AM | |
| rioxxterms.versionofrecord | 10.1609/aaai.v34i10.7232 |
Files
Original bundle
1 - 1 of 1
Loading...
- Name:
- 7232-Article Text-10461-1-10-20200526.pdf
- Size:
- 426.55 KB
- Format:
- Adobe Portable Document Format
- Description:
- Accepted version