Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers

TL;DR

This paper analyzes the limitations of current automated proof synthesis techniques in interactive theorem proving and introduces a pattern-guided tactic search method that improves proof success rates and proof script quality.

Contribution

It identifies key factors affecting proof success and proposes PGTS, a heuristic method inspired by human proof patterns, to enhance existing proof synthesis tools.

Findings

PGTS increases the number of proved theorems by 8.05% on average.

PGTS achieves a 20% increase in previously unproven theorems.

PGTS produces more concise and complex theorems.

Abstract

Formal verification using interactive theorem provers ensures high-quality software. However, writing proof scripts for interactive theorem provers is labor-intensive and requires deep expertise. Recent studies have leveraged deep learning to automate theorem proving by learning from manually written proof corpora. Nevertheless, these techniques still achieve limited success rates in proof synthesis. This paper investigates the theorems that current proof synthesis techniques are unable to prove and analyzes their characteristics. Through an in-depth analysis of the proven theorems, proof scripts, and the proof search process, we identify the limitations of existing tools and summarize the key factors influencing proof success rates. Our research provides valuable insights for the future optimization of automated proof tools. Based on our empirical study, we discover that tactic selections conforming to human expert proof patterns are more likely to lead to successful proofs. Inspired by this finding, we propose a pattern-guided tactic search (PGTS) method to heuristically enhance the search process of existing proof synthesis tools. Our evaluation experiments demonstrate that PGTS improves the number of theorems proved by existing proof synthesis tools by an average of 8.05\%, while also achieving an average 20\% increase in previously unproven theorems. Furthermore, PGTS enhances the capability of proof synthesis tools to prove complex theorems and generates more concise proof scripts.