Formal Premise Selection With Language Models
Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Czechowski, Konrad, Szymon Antoniak, Albert Qiaochu Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, Yuhuai Wu · Zenodo (CERN European Organization for Nuclear Research) · 2022
Premise selection, the problem of selecting a useful premise to prove a new theorem, is an essential part of theorem proving. Existing language models cannot access knowledge beyond a small context window, and therefore are unsatisfactory at retrieving useful premises (i.e., premise selection) from large databases for theorem proving. In this work, we provide a solution to this problem, by combining a premise selection model with a language model. We first select a handful (e.g., 8) of premises from a large theorem database consisting of 100K premises, and present them in the context along with proof states. The language model then utilizes these premises to construct a proof step. We show that this retrieval-augmented prover achieves significant improvements in proof rates compared to the language model alone.