Machine Learning to Support an Interactive Theorem Prover
Salman Haider, Andy Le, Echo Wu, Brian Howard · Scholarly and Creative Works from DePauw University (DePauw University) · 2019
An Interactive Theorem Prover (ITP) is a computer program that can assist a human in creating a proof of a mathematical theorem or the correctness of a piece of software. At each step in the proof, the human has the computer apply a chosen "tactic" to attempt to make progress toward the goal. We are exploring the possibility of using Machine Learning (ML) to assist in this tactic selection. Building on recent work at UC Berkeley and Princeton, where they adapted the Coq ITP so that it could interface with ML libraries via the Python scripting language, we have been evaluating strategies to encode the current proof state to try to improve the accuracy of tactic prediction.