Towards Machine Learning Induction
This work addresses a bottleneck in automated theorem proving for researchers and practitioners in formal verification, but it appears incremental as it focuses on suggestion rather than full automation.
The paper tackles the challenge of automating inductive theorem proving in Isabelle/HOL by introducing MeLoId, an approach that suggests promising applications of induction without requiring full proof search, though no concrete performance numbers are provided.
Induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle/HOL. Then, we present MeLoId, our approach to suggesting promising applications of induction without completing a proof search.