Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

TL;DR

This paper introduces a novel approach using Inductive Logic Programming to learn rules that explain tactic applicability in interactive theorem proving, enhancing existing tactic selection methods with rule-based filtering.

Contribution

The paper presents a new ILP-based method to learn symbolic rules for tactic prediction, improving guidance in interactive theorem proving systems.

Findings

Learned rules improve tactic prediction accuracy

Filtering tactic suggestions with rules enhances proof success rates

Enriched feature space captures complex proof state relationships

Abstract

Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.