自动形式化研究级数学的一个方法是将任务分解为更容易和可接近的子任务：未链接的形式化、实体链接和类型调整。同时，本文还提出了一个用于未链接的形式化的基准数据集 arXiv2Formal，其中包含了从 arXiv.org 的论文中选取的 50 个定理的 Lean 定理证明器的形式化。欢迎社区为该数据集的未来版本做出贡献。

Oct, 2023

通过使用语言模型将正式数学陈述翻译为相应的非正式陈述，我们创建了一个大型、灵活、多语言和多领域的非正式 - 正式对数据集 MMA，实验证明在 MMA 上对语言模型进行微调可以产生 16-18％的陈述，仅需进行最小的修正即可达到 miniF2F 和 ProofNet 标准，这也证明了在单语言任务中部署多语言正式数据进行微调可以得到更有能力的自动形式化模型。

Nov, 2023

本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

Jan, 2023

我们提出了一个新的用于评估大型语言模型自动形式化能力的基准测试 Formalization for Lean 4（ ame），其中引入了一个基于过程监督的验证器（PSV）模型，通过利用 Lean 4 编译器的精确反馈来提高自动形式化，并展示了 PSV 方法在使用更详细的过程信息进行微调时，可更有效地利用数据，进一步提高了 Lean 4 的自动形式化。

Jun, 2024

本文介绍了一种自动形式化欧几里得几何的神经符号框架，该框架结合了领域知识、SMT 求解器和大型语言模型，这一框架的挑战之一在于通过定理证明器自动填充图形信息以简化模型，实验结果展示了自动形式化几何问题时最新的语言模型的能力和局限性。

May, 2024

本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex 可以以自然语言形式翻译本科水平的 13 个定理的证明，这些具有两到三自然段长度的证明可以在 12 次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。

Nov, 2022

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

Jun, 2024

本文旨在通过实验探讨利用神经网络自动将 LaTeX 格式的非正式数学语句翻译成 Mizar 语言中的正式数学陈述。研究通过监督和非监督方法训练了三个基于神经网络的机器翻译模型，并开发了自定义的类型详细说明机制来优化结果。

Dec, 2019

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

Jun, 2024

通过自动生成验证的形式化 Isabelle 代码，我们的方法能够自动排除具有内在一致性问题或与形式化问题陈述不一致的解，并在多个数据集和模型大小上比以前最佳方法 — 普通多数投票 — 提高了 12% 以上的准确性。

Mar, 2024