Sep, 2020

用于自动定理证明的生成语言建模

PDF
TL;DR本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。
transformer-based language modelsautomated theorem provingproof assistantgpt-fmetamath
发现论文，激发创造
  • 自然证明器：基于语言模型的数学证明生成

    通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。

    May, 2022

  • 将 GPT-4 应用于未发表的正式语言的实验结果

    使用最新系统 GPT-4，完善的自然语言规范指定先前未发布的形式系统的几项任务，如说明函数和类型定义，证明简单定理和验证用户提供的证明，并显示出域知识，发明了有用的新语法和语义，以及表现出泛化和推理能力，因此答案似乎是：是。

    May, 2023

  • GPT 语言模型在大学教学创新中的应用

    GPT (Generative Pre-trained Transformer) 是一种人工智能和自然语言处理技术，能够自动生成文本。本文主要研究了将 GPT 语言模型应用于大学教学的各个方面，包括学生和教师活动的创新、内容理解与生成、问题解决、个性化和试卷批改等。同时，作者还在软件工程等领域进行了详细实验，评估了 ChatGPT 作为助理工具在理论活动、习题和实验实践中的潜在应用价值。

    Mar, 2024

  • 学习生成定理以证明定理

    为了解决自动定理证明中有限的人工编写定理和证明的问题，我们提出了一种学习神经生成器自动生成定理和证明来训练定理证明器的方法，并通过实验验证，证明该方法的合理性，并成功推动了 Metamath 自动定理证明的发展。

    Feb, 2020

  • 探索大型语言模型用于实现人机协作的可变自主性

    该论文探讨了将大型语言模型（如生成式预训练变换器 GPT）整合到人机合作环境中，通过口头人机交流手段促进可变自主性的快速发展的数字景观中，介绍了一种基于 Unity 虚拟现实（VR）环境的 GPT 驱动多机器人测试平台的创新框架。用户研究表明，用户对于与机器人对话的预设期望较高，却很少尝试探索机器人合作伙伴的实际语言和认知能力，但那些进行探索的用户能从更自然的沟通和人类式的双向交流中受益。我们提供了一组对未来研究和类似系统的技术实施的经验教训。

    Dec, 2023

  • 大型语言模型对数学的理解：源批评和推演

    GPT-4 的研究调查发现，尽管该模型可以重复、改编和润色其之前见过的数学证明，然而它并未实际理解基本数学概念，而在形式语言中证明数学定理的任务与搜索引擎如 Google 的方法相当，而预测句子中的下一个词可能是一种错误的方法，往往会导致过度推断和最终失败。

    Nov, 2023

  • ATG：基于生成式语言模型的自动定理生成基准测试

    自动生成定理是一个挑战，本文提出了一个基于自动化定理生成（ATG）的评估基准，以探究当前生成性语言模型（LMs）在生成新定理和可重复定理方面的能力，结果表明当前 LMs 仍有改进空间。

    May, 2024

  • 使用语言模型从数学问题中生成 Prolog 谓词

    最近，ChatGPT 在 NLP 领域引起了广泛关注。ChatGPT 是一种基于 Transformer 的大规模生成式语言模型，在自然语言处理的各种任务中表现出多样性。然而，大型语言模型在解决需要推理能力的数学问题时往往表现较差。先前的研究表明，借助思维链提示可以增强推理能力。现在，我们旨在探讨是否通过对生成 Prolog 代码进行微调，进而将这些代码传递给编译器可以进一步提高准确性。结果显示，Prolog 生成模型在性能上超过了基准模型，而组合生成模型并未显著提高。基于 GSM8K 的 Prolog 语料库和相应微调的基于 LLaMA7B 的 Prolog 生成模型已经发布给研究社区。

    Sep, 2023

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

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

    Jun, 2024

  • 使用 Transformer 测量神经证明生成中的系统化概括能力

    研究 Transformer 语言模型在自然语言中进行基于逻辑推理的任务，探究它们的系统泛化能力，发现其在逆向推理证明方面表现更优，并且发现没有经过证明生成训练的模型更适合处理长证明的问题。研究结果强调了 TLM 在逻辑推理中的系统泛化行为，并且对其核心推理策略的深入研究提出了启示。

    Sep, 2020