DEEPER
A Deep Exploratory Engine for Precise Expert Reasoning
The Project
The "DEEPER" project aims to revolutionize automated theorem proving by integrating advanced machine learning techniques as guides to state-of-the-art automatic theorem provers (ATPs). By combining neural and symbolic learning methods, the team seeks to enhance proof guidance, particularly for higher-order and dependently typed calculi, which are crucial for formalizing complex mathematical problems. The project focuses on developing AI-based guidance for automated reasoning systems, designing efficient proof automation, and integrating these advancements into modern proof assistants.
The Team
Cezary Kaliszyk is a Professor at the University of Melbourne specializing in automated reasoning, proof assistant automation, and interactive theorem proving. After completing his PhD at Radboud University in the Netherlands, he held a tenured Associate Professorship at the University of Innsbruck. His research includes learning-guided proof search, nominal logic, and the development of hammer systems for Coq and formal set theory.
Martin Suda leads the Automated Reasoning Group at the Czech Institute of Informatics, Robotics, and Cybernetics (CIIRC), part of Czech Technical University in Prague. His research explores the intersection of machine learning and automated theorem proving, with a focus on enhancing systems like the Vampire prover. He earned his PhD from Saarland University and has held postdoctoral posts in Manchester and Vienna.
Jan Jakubův is a senior researcher at CIIRC, Czech Technical University in Prague, with expertise in automated reasoning and formal verification. He received his PhD from Heriot-Watt University, where he studied process calculi and type systems. His recent work emphasizes machine learning techniques for theorem proving, and he is the principal developer of ENIGMA.