ProofNet：本科数学的自动形式化和形式化证明
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
摘要：
我们介绍ProofNet，一个基准的自动形式化和正式证明的本科层次的数学。ProofNet基准测试由371个示例组成，每个示例由Lean 3中的正式定理语句、自然语言定理语句和自然语言证明组成。这些问题主要来自流行的本科纯数学教科书，涵盖了诸如实分析和复分析、线性代数、抽象代数和拓扑学等主题。我们打算让ProofNet成为一个具有挑战性的基准，它将推动自动形式化和自动定理证明的进展。我们通过上下文学习报告了语句自动形式化的基线结果。此外，我们介绍了两个新的语句自动形式化方法：即时检索和蒸馏回译。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
