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\%$.

翻译：自动正规化是一个从自然语言数学自动转换成正式规格和证明的过程。一个成功的自动化正规化系统可以推进正式验证、程序合成和人工智能领域。虽然长期而言自动化正规化的长期目标似乎难以实现,但我们展示了大型语言模型为实现这一目标提供了新的前景。我们惊讶地发现,LLMS可以将数学竞争问题的很大一部分(25.3美元)完美地转换为伊莎贝尔/HOL的正式规格。我们通过对这些自动正规化的理论进行的培训,改进了以前引入的神经理论验证,从而证明了这一过程的效用。我们的方法使得MiniF2F理论检验基准取得了新的最新结果,将验证率从29.6美元提高到35.2美元。