Apr, 2024

迈向在 Lean 中进行定理证明的大型语言模型作为副驾驶

PDF
TL;DR该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助和自动化程度的有效性。
theorem provinglarge language modelslean copilotproof automationpretrained models
发现论文，激发创造
  • LeanDojo：具备检索增强语言模型的定理证明

    本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从 Lean 中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于 LLM 的证明程序。其成本低廉，只需要一台 GPU 进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含 96962 个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和 GPT-4，ReProver 非常有效。我们发布了代码和数据集，以促进进一步的研究。

    Jun, 2023

  • MLCopilot: 大型语言模型在解决机器学习任务中的应用

    本文介绍了一种利用 LLMs 自动学习生成机器学习解决方案的框架 MLCopilot，旨在将机器智能与人类知识相结合来提高解决新任务的能力，生成的解决方案可以直接应用于实际环境中。

    Apr, 2023

  • LeanReasoner: 用 Lean 增强复杂逻辑推理

    利用 Lean 框架，将复杂的逻辑推理问题形式化为定理后进行求解，以减少逻辑不一致性的风险并提升处理复杂推理任务的能力，取得了在 FOLIO 数据集上的最先进表现，并在 ProofWriter 上接近该水平的成果。值得注意的是，这些结果是在每个数据集的不到 100 个领域内样本进行微调实现的。

    Mar, 2024

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

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

    May, 2024

  • TheoremLlama: 通用 LLM 转换为 Lean4 专家

    使用 Lean 等计算机可验证形式语言来证明数学定理具有重大影响，本文提出了 TheoremLlama 框架，通过生成对齐的数据集和训练方法，使大型语言模型成为 Lean4 专家，实现了高于 GPT-4 基准的累积准确率。

    Jul, 2024

  • 利用语言模型进行定理证明的证明工件协同训练

    本文介绍了 PACT 的一般方法，通过自我监督学习从内核级证明术语中提取丰富的数据，以协同常规战术预测目标，以提高定理证明的成功率。

    Feb, 2021

  • LLMSTEP: Lean 中的 LLM 证明步骤建议

    LLMSTEP 是将语言模型整合到 Lean 证明助手中的工具，它将用户的证明状态发送到托管语言模型的服务器，语言模型生成建议并在 Lean 中检查后显示给用户在其开发环境中。我们提供了基准语言模型，以及用于微调和评估的代码，以支持进一步的开发。我们提供了在 CPU、CUDA GPU 或 Google Colab 笔记本上运行的服务器实现，这是快速有效的语言模型建议的一小步。

    Oct, 2023

  • Copilot 评估系统：评估 LLM 指导的软件编程

    利用 Large Language Models（LLMs）提高开发人员在开发环境（IDEs）中的生产力是现代软件开发的重点。本文介绍了 Copilot 评估工具，用于评估 LLM 引导的 IDE 交互，在不同编程场景和语言中提供了更稳健和信息丰富的评估指标。通过这些指标，我们评估了三种常见 LLMs 的性能，为未来的 LLM 引导 IDE 场景的开发和验证提供了经验教训。

    Feb, 2024

  • 一种语言代理方法用于形式证明

    使用大型语言模型和 COPRA 方法进行定理证明中的策略选择和反馈建议，相较于 GPT-4 和现有模型，在快速找到正确证明方面取得显著好处。

    Oct, 2023

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

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

    Jun, 2024