Large Language Models (LLMs) hold the potential to revolutionize
autoformalization. The introduction of Lean4, a mathematical programming
language, presents an unprecedented opportunity to rigorously assess the
autoformalization capabilities of LLMs. This paper introduces a novel
evaluation benchmark designed for Lean4, applying it to test the abilities of
state-of-the-art LLMs, including GPT-3.5, GPT-4, and Gemini Pro. Our
comprehensive analysis reveals that, despite recent advancements, these LLMs
still exhibit limitations in autoformalization, particularly in more complex
areas of mathematics. These findings underscore the need for further
development in LLMs to fully harness their potential in scientific research and
development. This study not only benchmarks current LLM capabilities but also
sets the stage for future enhancements in autoformalization.

大型语言模型 (LLMs) 具有彻底改变自动形式化的潜力。引入数学编程语言 Lean4 为评估 LLMs 的自动形式化能力提供了前所未有的机会。本文介绍了一种专为 Lean4 设计的新型评估基准，将其应用于测试包括 GPT-3.5、GPT-4 和 Gemini Pro 在内的最先进的 LLMs 的能力。我们全面的分析发现，尽管最近有所进展，这些 LLMs 在自动形式化方面仍存在局限性，尤其是在更复杂的数学领域。这些发现强调了需要进一步发展 LLMs，以充分发挥它们在科学研究和开发中的潜力。本研究不仅为当前的 LLM 能力设立了基准，还为自动形式化的未来增强奠定了基础。