Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
Open paper
Benchmark
Model
Rank
Results
automated-theorem-proving-on-minif2f-test
Sledgehammer
–
cumulative: 10.4
Pass@1: 10.4
ITP: Isabelle
automated-theorem-proving-on-minif2f-test
Thor
–
cumulative: 29.9
Pass@1: 29.9
ITP: Isabelle
Rank counts only results with a code link.