Process-Driven Autoformalization in Lean 4

自动形式化，即将自然语言数学转化为形式语言，为推进数学推理提供了重要的潜力。然而，现有的努力仅限于具有大量在线语料库的形式语言，并且难以跟上快速发展的语言，如Lean 4。为了弥补这一差距，我们提出了一个新的基准\textbf{Form}alization for \textbf{L}ean~\textbf{4}（\textbf{\name}），旨在评估大型语言模型（LLM）的自动形式化能力。该基准包括对问题、答案、形式陈述和证明的全面评估。此外，我们还引入了一个\textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier（\textbf{PSV}）模型，利用Lean 4编译器的精确反馈来增强自动形式化。我们的实验表明，PSV方法改善了自动形式化，使用较少的过滤训练数据即可实现更高的准确性。此外，当使用包含详细过程信息的数据进行微调时，PSV可以更有效地利用数据，从而在Lean 4的自动形式化方面实现更大的改进。我们的数据集和代码可在\url{https://github.com/rookie-joe/PDA}上获得。

本论文旨在解决自然语言数学转化为形式语言的问题，提出了一个新的基于Lean 4的自动形式化评估基准，并且引入了一个基于过程监督的验证模型来提高自动形式化的准确性。

论文提出了一个新的基于Lean 4的自动形式化评估基准，同时引入了一个基于过程监督的验证模型来提高自动形式化的准确性。

论文的亮点包括：提出了一个新的基于Lean 4的自动形式化评估基准，引入了一个基于过程监督的验证模型来提高自动形式化的准确性；实验结果表明，PSV方法可以提高自动形式化的准确性，使用更详细的过程信息的数据可以更有效地提高自动形式化的准确性；数据集和代码已经公开发布。

近期在这个领域的相关研究包括：AutoMizar、MathLang、和GPT-3等。