Researchers used few-shot prompting to ask large language models to translate informal mathematical statements into Isabelle/HOL. The generated formalizations were then used as additional training data for a neural theorem prover, linking informal-language translation with formal proof search in…
The paper reported that large language models correctly translated 25.3% of sampled mathematical competition problems into Isabelle/HOL formal specifications, and that training a neural theorem prover on autoformalized theorems increased its miniF2F proof rate from 29.6% to 35.2%.
Researchers used few-shot prompting to ask large language models to translate informal mathematical statements into Isabelle/HOL. The generated formalizations were then used as additional training data for a neural theorem prover, linking informal-language translation with formal proof search in one pipeline.
The result provided an early empirical bridge between modern language models and proof assistants: autoformalization was not only evaluated as translation accuracy, but also shown to create training data that improved a downstream prover. This became an important precursor to later autoformalization benchmarks and synthetic formal-mathematics pipelines.
Significance rationale: The work established an early large-language-model route from informal competition mathematics to proof-assistant specifications and showed that generated formal statements could improve downstream theorem proving, helping make autoformalization a concrete AI4Math research direction.
The research paper publicly reported the Isabelle/HOL autoformalization and miniF2F results. E2 records a public research record and does not imply independent reproduction or verification.
No corrections recorded.
