ICLRJun, 2024

Lean4 中自动形式化的评估基准

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

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

    Jun, 2024

  • 利用大型语言模型进行自动形式化

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

    May, 2022

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

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

    Jun, 2024

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

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

    Mar, 2024

  • LLM4PLC：工控系统中基于大型语言模型的可验证 PLC 编程

    提出 LLM4PLC 的用户引导迭代流程，通过用户反馈和外部验证工具来改善大型语言模型（LLM）生成的代码的可验证性，提高成功生成的比例并提高代码质量。

    Jan, 2024

  • 大型语言模型作为自动标定器用于基准测试视觉语言模型

    通过自动数据整理和评估，利用优秀的语言模型和视觉语言模型衡量对齐 VLMs 与人类智能的能力，我们提出了 Auto-Bench 作为一个灵活、可扩展和全面的评估 benchmark。

    Nov, 2023

  • LLM 能够正式对话吗？自动评估 LLM 在翻译和解释正式规范中的表现

    利用大型语言模型 (LLMs) 将自然语言描述转换为形式化规范的能力进行了评估，提出了一种使用两个 LLMs 与现成验证程序结合的方法来自动评估其翻译能力，结果显示目前最先进的 LLMs 无法充分解决这个任务，限制了它们在复杂系统设计中的实用性。

    Mar, 2024

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

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

    Jun, 2024

  • 在 Rust 中利用大型语言模型进行自动证明合成

    基于大型语言模型（LLMs）和静态分析相结合，开发了一个基于 Rust 的形式验证框架 Verus 的原型。通过将验证任务分解为多个较小的任务，迭代地查询 GPT-4，并将其输出与轻量级静态分析相结合，这个原型显著减少了编写入门级证明代码的人力工作。

    Nov, 2023

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

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

    Jun, 2024