Lyra: Orchestrating Dual Correction in Automated Theorem Proving

Open paper
Benchmark Model Rank Results
automated-theorem-proving-on-minif2f-testLyra + GPT-4#5cumulative: 47.1Pass@100: 47.1ITP: Isabelle
automated-theorem-proving-on-minif2f-validLyra + GPT-4#5Pass@100: 52.0

Rank counts only results with a code link.