Timezone: »

 
Poster
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
Albert Q. Jiang · Wenda Li · Szymon Tworkowski · Konrad Czechowski · Tomasz Odrzygóźdź · Piotr Miłoś · Yuhuai Wu · Mateja Jamnik

Thu Dec 01 09:00 AM -- 11:00 AM (PST) @ Hall J #639
in Poster Session 5 »
In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important. This presents a challenge for all theorem provers, especially the ones based on language models, due to their relative inability to reason over huge volumes of premises in text form. This paper introduces Thor, a framework integrating language models and automated theorem provers to overcome this difficulty. In Thor, a class of methods called hammers that leverage the power of automated theorem provers are used for premise selection, while all other tasks are designated to language models. Thor increases a language model's success rate on the PISA dataset from $39\%$ to $57\%$, while solving $8.2\%$ of problems neither language models nor automated theorem provers are able to solve on their own. Furthermore, with a significantly smaller computational budget, Thor can achieve a success rate on the MiniF2F dataset that is on par with the best existing methods. Thor can be instantiated for the majority of popular interactive theorem provers via a straightforward protocol we provide.
Keywords: language models · theorem proving · MiniF2F · automated theorem provers · neuro-symbolic method · PISA
[ Paper]  [ Poster]  [ OpenReview] 

Author Information

Albert Q. Jiang (University of Cambridge)
Wenda Li (University of Cambridge)
Szymon Tworkowski (University of Warsaw)
Szymon Tworkowski

Machine Learning Master’s student at the University of Warsaw, advised by Yuhuai Wu and Piotr Miłoś Interested in improving language models (efficient Transformers) and investigating their implications via topics like in-context learning or OOD generalization in reasoning tasks.

Konrad Czechowski (Uniwersytet Warszawski, ul. Krakowskie Przedmieście 26/28, 00-927 Warszawa, NIP 525-001-12-66)
Tomasz Odrzygóźdź (IDEAS NCBR Sp. z o.o. ul. Nowogrodzka 47A 00-695 Warszawa VAT Number: PL 7011017605)
Piotr Miłoś (Ideas NCBR, Polish Academy of Sciences)
Yuhuai Wu (Google)
Mateja Jamnik (University of Cambridge)

More from the Same Authors