DeepIsaHOL
Financiado
Reinforcement learning to improve proof-automation in theorem proving
Developing generic proof automation methods for interactive theorem provers (ITPs) is challenging but valuable. Applications range from performance improvements in the verification of safety-critical systems to the certification o...
Developing generic proof automation methods for interactive theorem provers (ITPs) is challenging but valuable. Applications range from performance improvements in the verification of safety-critical systems to the certification of famous, long, and hard-to-prove theorems. We propose using recently successful reinforcement learning (RL) algorithms to learn proof strategies employed in vast ITP libraries and use them as generic methods to automate the ITP proving process. Specifically, the project aims to create a tactic for one of the most popular and automated ITPs, Isabelle/HOL, and train the RL algorithms with theorems from the two largest Isabelle libraries: HOL-Library and the Archive of Formal Proofs (AFP). We identify three gaps in the state of the art that such an RL-and-Isabelle approach would close and describe the work packages that will achieve the corresponding three research objectives. The project will be done under the guidance of Dr Josef Urban, who holds a Distinguished Researcher position at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) within the Czech Technical University (CTU) in Prague. Dr Urban and the CIIRC group are experts in integrating machine learning (ML) and interactive theorem proving. Their infrastructure and expertise targeted to ML and ITPs provide the best research environment for this project. Jonathan Julián Huerta y Munive, the researcher carrying out the project, complements this expertise with his Isabelle/HOL experience and knowledge of ITP applications.
ver más
Duración del proyecto: 27 meses
Fecha Inicio: 2023-03-09
Fecha Fin: 2025-06-30
Fecha Fin: 2025-06-30
Línea de financiación: concedida
El organismo HORIZON EUROPE notifico la concesión del proyecto el día 2023-03-09
Línea de financiación objetivo
El proyecto se financió a través de la siguiente ayuda:
HORIZON-MSCA-2022-PF-01-01:
MSCA Postdoctoral Fellowships 2022
Cerrada
hace 2 años
Presupuesto
El presupuesto total del proyecto asciende a
166K€
Líder del proyecto
CESKE VYSOKE UCENI TECHNICKE V PRAZE
No se ha especificado una descripción o un objeto social para esta compañía.
Perfil tecnológico
TRL
4-5
Perfil tecnológico
TRL
4-5