Stream: General

Topic: New paper on machine learning for Isabelle

view this post on Zulip Albert Jiang (May 26 2022 at 10:01):

We have a preprint for our paper Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers:!

We increased the proportion of solvable problems in the Archive of Formal Proofs for a language model from 39% to 57%, with the help of Sledgehammer. We also have a head-to-head comparison with OpenAI's IMO solver in Lean and slightly increased the success rate from 29.6% to 29.9%.

Last updated: Dec 07 2023 at 08:19 UTC