Machine Learning to Support an Interactive Theorem Prover

Authors

Salman Haider, DePauw University
Andy Le, DePauw University
Echo Wu, DePauw University
Brian T. Howard, DePauw UniversityFollow

Files

Document Type

Poster

Publication Date

Fall 10-2-2019

Abstract

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.

Funding and Acknowledgements

Fellows Program, J. William Asher and Melanie J. Norton Endowed Fund in the Sciences

Recommended Citation

Haider, Salman, Andy Le, Echo Wu and Brian Howard. "Machine Learning to Support an Interactive Theorem Prover." Poster presented at the DePauw University Science Research Fellows Poster Session, Greencastle, IN, October 2019.