PaMpeR: Proof Method Recommendation System for Isabelle/HOL

TL;DR

PaMpeR is an intelligent recommendation system for Isabelle/HOL that suggests proof methods based on proof states, helping users choose appropriate tactics by leveraging expert knowledge and providing explanations.

Contribution

It introduces a novel proof method recommendation system that transfers expert knowledge to new users through analysis of proof corpora and offers qualitative explanations.

Findings

PaMpeR accurately predicts proof methods used by experienced users.

It performs especially well with special purpose proof methods.

The system enhances user guidance in proof development.

Abstract

Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users' expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users' proof methods invocation especially when it comes to special purpose proof methods.