Room 206 (2nd floor, badged access)
30 novembre 2023 - 14h00
AI-Enhanced Theorem Proving: Tactical Approaches for Induction Problems
par Yutaka Nagashima de Huawei Technologies R&D (UK)
Abstract: The realm of formal verification, particularly when engaging with proof assistants built on expressive logics, has consistently grappled with limited automation in proof search. This limitation becomes even more pronounced when addressing inductive problems, which are integral to the verification of both software and hardware systems.
To confront this challenge head-on, we have developed the Abduction Prover for Isabelle/HOL. This tool represents a significant advancement in achieving more robust proof automation specifically tailored to inductive problems. A demonstration of the Abduction Prover's capabilities is available on YouTube:
https://youtu.be/rXU-lJxP_GI
During this presentation, I will delve into:
- The application of abductive reasoning to discern valuable intermediate lemmas.
- The precise representations chosen to encapsulate human expertise, formulating them as heuristic guidelines.
- The demarcation between heuristic-driven processes and those reliant on search algorithms.
- Strategies developed to optimize the utilization of parallelism.
- Our approach to amalgamating a spectrum of automation tools within a singular, integrated framework.
- Recognizing and addressing the limitations inherent in our current methodologies.
- Insights from eight years of exploration: Recognizing negative findings and trade-offs in AI for theorem proving.
I will conclude the presentation by outlining the future directions of our research, highlighting potential areas of exploration, and the envisioned next steps to further advance the field of AI-enhanced theorem proving.
