Large language models show promise for autoformalization, the task of
automatically translating natural language into formal languages. However,
current autoformalization methods remain limited. The last reported
state-of-the-art performance on the ProofNet formalization benchmark for the
Lean proof assistant, achieved using Codex for Lean 3, only showed successful
formalization of 16.1% of informal statements. Similarly, our evaluation of
GPT-4o for Lean 4 only produces successful translations 34.9% of the time. Our
analysis shows that the performance of these models is largely limited by their
inability to generate formal statements that successfully type-check (i.e., are
syntactically correct and consistent with types) - with a whopping 86.6% of
GPT-4o errors starting from a type-check failure. In this work, we propose a
method to fix this issue through decoding with type-check filtering, where we
initially sample a diverse set of candidate formalizations for an informal
statement, then use the Lean proof assistant to filter out candidates that do
not type-check. Using GPT-4o as a base model, and combining our method with
self-consistency, we obtain a +18.3% absolute increase in formalization
accuracy, and achieve a new state-of-the-art of 53.2% on ProofNet with Lean 4.

通过与类型检查筛选相结合，我们使用自一致性方法对基于 GPT-4o 模型的 GPT-4o 型进行解码，使得自然语言能够更准确地转化为形式语言，并在 Lean 4 的 ProofNet 中实现 53.2% 的新的最优效果。

提升自动形式化的使用通过类型检查

Improving Autoformalization using Type Checking

We introduce ProofNet, a benchmark for autoformalization and formal proving
of undergraduate-level mathematics. The ProofNet benchmarks consists of 371
examples, each consisting of a formal theorem statement in Lean 3, a natural
language theorem statement, and a natural language proof. The problems are
primarily drawn from popular undergraduate pure mathematics textbooks and cover
topics such as real and complex analysis, linear algebra, abstract algebra, and
topology. We intend for ProofNet to be a challenging benchmark that will drive
progress in autoformalization and automatic theorem proving. We report baseline
results on statement autoformalization via in-context learning. Moreover, we
introduce two novel statement autoformalization methods: prompt retrieval and
distilled backtranslation.

ProofNet 是一个面向本科级数学自动形式化和形式证明的基准，包括 371 个例子，目的在于推动自动形式化和自动定理证明的进步。 通过上下文学习实现了对陈述自动形式化的基线结果。同时，引入了两种新的陈述自动形式化方法：提示检索和精炼反向翻译。该基准主要涵盖了实数和复数分析，线性代数，抽象代数和拓扑等主题。