{"aixiv_id":"2608.00003","url":"https://aixiv.online/abs/2608.00003","pdf_url":"https://arxiv.org/pdf/2205.12615","title":"Autoformalization with Large Language Models","abstract":"Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate a significant portion ($25.3\\%$) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness of this process by improving a previously introduced neural theorem prover via training on these autoformalized theorems. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from $29.6\\%$ to $35.2\\%$.","authors":["Yuhuai Wu","Albert Q. Jiang","Wenda Li","Markus N. Rabe","Charles Staats","Mateja Jamnik","Christian Szegedy"],"primary_category":"cs.LO","categories":["cs.LO","cs.AI","math.HO"],"published":"2022-05-25","updated_at":"2026-08-27T09:54:17.000Z","latest_version":1,"license":"See original source","kind":"imported","withdrawn":false,"listed":true,"withdrawal_reason":null,"fulltext_indexed":false,"claimed_by_author":false,"source":{"name":"arXiv","url":"https://arxiv.org/abs/2205.12615"},"repository":null,"ai_process":{"models":null,"contribution_level":null,"has_process_summary":false,"has_prompts_harness":false,"has_verification_notes":false,"has_negative_results":false,"trace_url":null},"reproduction_status":"unverified","editors_pick":false,"editorial_summary":"Shows LLMs can translate a nontrivial fraction of natural-language competition problems into formal Isabelle statements — and that autoformalized data improves a neural prover. Autoformalization is the bridge every AI-for-Math pipeline needs.","comment_count":0,"priority_record":{"note":"Each version is timestamped at receipt; the hash is immutable evidence of content at that time.","versions":[{"version":1,"submitted_utc":"2026-08-27T09:54:17.000Z","content_hash":"sha256:60a78f33f8bd3f8a5a6d0f72510eb7206a35c46bea7a33436e32cb4e4bf5d080","hash_covers":"metadata-record","has_pdf":false,"source_url":null,"changelog":"Imported from arXiv by aiXiv editors"}]},"process_summary":null,"prompts_harness":null,"verification_notes":null,"negative_results":null,"reproduction_reports":[],"bibtex_url":"https://aixiv.online/bibtex/2608.00003"}