Proof completion in the formal verification language - Coq

Formal verification is an important field in Software Engineering and in Computer Science in general. With increasingly complex algorithms and models being implemented in today’s world, verifying their correctness has become that much more important. Formal languages like Coq help us achieve this task by providing us a framework to write proofs. However, the learning curve for these kinds of functional languages is steep since it involves rigorous proofs and the languages have a unique syntax structure. Programmers can use helpful suggestions about what tactics to use while writing their proofs.

The aim of this project is build models that can learn to automatically prove theorems in Coq. We explored techniques from language modeling literature, and automatic theorem provers, such as hammers, to build a hybrid model to predict the next tactic in a proof and eventually try to complete the proof.