Mining State-Based Models from Proof Corpora

TL;DR

This paper introduces an automated method to infer extended finite state machines from proof corpora, aiding in automating and guiding proofs in interactive theorem proving with promising preliminary results.

Contribution

It presents a novel technique to extract state-based models from proof data, improving automation and guidance in theorem proving processes.

Findings

Inferred models are generally accurate with few false positives.

Representing proofs as state models helps guide new proofs effectively.

Preliminary experiments show promising results in proof automation.

Abstract

Interactive theorem provers have been used extensively to reason about various software/hardware systems and mathematical theorems. The key challenge when using an interactive prover is finding a suitable sequence of proof steps that will lead to a successful proof requires a significant amount of human intervention. This paper presents an automated technique that takes as input examples of successful proofs and infers an Extended Finite State Machine as output. This can in turn be used to generate proofs of new conjectures. Our preliminary experiments show that the inferred models are generally accurate (contain few false-positive sequences) and that representing existing proofs in such a way can be very useful when guiding new ones.