slideshow 3

Logic seminar

Integrating Machine Learning into Saturation-based ATPs

Martin Suda
CVUT

 

Monday, 14. November 2022 - 16:00 to 17:30
Large lecture room at Zitna and online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join online
Applying the techniques of machine learning (ML) promises to dramatically improve the performance of modern automatic theorem provers (ATPs) and thus to positively impact their applications. The most successful avenue in this direction explored so far is machine-learned clause selection guidance, where we learn to recognize and prefer for selection clauses that look like those that contributed to a proof in past successful runs. In this talk I present Deepire, an extension of the ATP Vampire where clause selection is guided by a recursive neural network (RvNN) for classifying clauses based solely on their derivation history.