Papers › Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
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
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.
In Syntology Open this paper in Syntology's Atlas, the map of the papers in Syntology's graph and their citations.
Code
No code repository is listed for this paper in the archive or in Syntology's graph.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Tasks
Results from the paper archive 2025-07-28
| Task | Dataset | Model | Metric | Value | Rank at snapshot | Leaderboard | Report |
|---|---|---|---|---|---|---|---|
| Automated Theorem Proving | miniF2F-test | Thor | ITP | Isabelle | #17 of 29 | Archive leaderboard | report |
| Automated Theorem Proving | miniF2F-test | Thor | Pass@1 | 29.9 | #17 of 29 | Archive leaderboard | report |
| Automated Theorem Proving | miniF2F-test | Thor | cumulative | 29.9 | #17 of 29 | Archive leaderboard | report |
| Automated Theorem Proving | miniF2F-test | Sledgehammer | ITP | Isabelle | #28 of 29 | Archive leaderboard | report |
| Automated Theorem Proving | miniF2F-test | Sledgehammer | Pass@1 | 10.4 | #28 of 29 | Archive leaderboard | report |
| Automated Theorem Proving | miniF2F-test | Sledgehammer | cumulative | 10.4 | #28 of 29 | Archive leaderboard | report |
Ranks are positions in the archive's leaderboards as they stood at the 2025-07-28 snapshot. Results published since then are not among these rows, so a rank here is not a current standing.
Methods
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections