Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies

EasyChair Preprint 3334

Abstract

Proof assistants offer a formal language to write mathematical definitions, executable algorithms, and theorems together with an environment for interactive development of machine-checked proofs. Developers manually construct definitions and lemmas on proof assistants to prove the theorems. However, the time and labor costs of manually proving theorems in proof assistants remain prohibitively high. Therefore, proving the theorem automatically for the sizeable formal project becomes significant. In this paper, we propose SmartCoq, a proof search system that uses a dynamic strategy to solve the problem of automating the interaction with proof assistants. The design of our dynamic strategy is flexible and straightforward: it can automatically optimize itself based on theorems without manual intervention. SmartCoq uses dynamic strategies to learn from the wrong paths in the past and find a correct path to complete the proof. We demonstrate SmartCoq on the proof obligations from a large practical proof project, the CompCert verified C compiler, and the result shows that it can automatically solve 14.5% of proofs in our test dataset.

Keyphrases: interactive theorem proving, machine learning, proof assistants

@booklet{EasyChair:3334,
  author    = {Guangshuai Mo and Yan Xiong and Wenchao Huang and Lu Ma},
  title     = {Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies},
  howpublished = {EasyChair Preprint 3334},
  year      = {EasyChair, 2020}}