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% 的新的最优效果。