TITLE: Machine learning automated proofs.
SPEAKER: Ekaterina Komendantskaya (School of Computing, University of Dundee)

ABSTRACT:

Automated provers (also interactive provers, or ITPs) based on first-order or higher-order logics have become a major tool in software verification. Programs in ITPs may contain thousands of lemmas and theorems of variable sizes and complexities; each proof is constructed by combining a finite number of tactics. Some proofs may yield the same pattern of tactics, and can be fully automated, and others may require programmer's intervention. In this case, a manually found proof for one problematic lemma may serve as a template for several other lemmas needing a manual proof.

Can these proof patterns be discovered using statistical machine learning methods, and can this help to optimize the current practice of programming in ITPs?  In this talk, I will propose a new interdisciplinary method that can be used for this purpose.