Toggle navigation OpenReview .net Login Open Peer Review. Open Publishing. Open Access. Open Discussion. Open Recommendations. Open Directory. Open API. Open Source. × Yuhuai Wu , Albert Qiaochu Jiang , Wenda Li , Markus Norman Rabe , Charles E Staats , Mateja Jamnik , Christian Szegedy Published: 31 Oct 2022, 18:00, Last Modified: 12 Jan 2023, 12:12 NeurIPS 2022 Accept Readers: Everyone Keywords : Large language models, Autoformalization, Formal Math, miniF2F. TL;DR : Large language models can be used to do autoformalization, allowing us to achieve in a new SOTA on miniF2F benchmark. 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-t...