Nov, 2022

利用大型语言模型实现数学形式化辅助工具

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

    本文研究了自动形式化的过程，并发现大型语言模型可用于将自然语言的数学问题翻译为 Isabelle/HOL 的形式化说明，证明了这种方法的实用性，并通过训练预先介绍的神经定理证明器使改进了 MiniF2F 定理证明基准的证明率从 29.6% 提高到 35.2%。

    May, 2022

  • 基于自动正式化的数学和代码正确性研究：基础证明实验

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

    Jan, 2023

  • 精益练习册：从自然语言数学问题转化而成的大规模精益问题集

    通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。

    Jun, 2024

  • 一种新的自动形式化方法

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

    Oct, 2023

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

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

    Jun, 2024

  • 可信的正式自然语言规范

    该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

    Oct, 2023

  • 朝着大型语言模型辅助的程序优化

    使用 GPT4、Coq 和 Coqhammer 实现的 LLM4PR 工具将正式程序细化技术与非正式 LLM 方法相结合，通过将规范转换为前置条件和后置条件，基于细化演算自动生成提示，并与 LLM 进行交互以生成代码，最后验证生成的代码是否符合细化演算的条件，从而确保代码的正确性。

    Jun, 2024

  • 不要相信：验证 - 用自动形式化证明 LLM 定量推理的基础

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

    Mar, 2024

  • 多语种数学自动形式化

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

    Nov, 2023

  • DeepSeek-Prover: 通过大规模合成数据推进 LLMs 中的定理证明

    基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

    May, 2024