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

Jun, 2024

该研究通过扰动问题和生成数据集，评估大型语言模型在数学推理任务中的能力，结果表明现有模型在扰动问题上性能显著下降，缺乏深度推理能力。

Jan, 2024

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

May, 2022

通过定义单位并确保在数学运算过程中单位的一致性，我们提出了一种系统的方法来解决大规模语言模型在解决涉及跨多种类型或单位的数量的数学问题时面临的挑战。我们使用 Unit Consistency Programs（UCPs）为每个问题开发了一个带有单位规范和单位验证程序的数据集，并借助 UCPs 对 Code Llama（7B）模型进行了微调，从而产生了 VerityMath，并展示了我们的初步研究结果。

Nov, 2023

提出了一种名为自验证的方法，该方法使用推理链的结论作为条件建立新的样本，并要求大型语言模型重新预测原始条件，从而降低了多任务精度误差。经过大量实验验证，此方法可以使大型语言模型避免出现不正确的推理链干扰，并实现具有竞争力的推理性能，可用于算术和逻辑推理数据集的有限次学习。

Dec, 2022

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

Nov, 2023

本文提出了一种神经符号方法，将大型语言模型和答案集编程的优势相结合，以将逻辑谜题的自然语言描述转化为答案集程序。

Jul, 2023

我们介绍并开源了我们的数学推理 LLMs InternLM-Math，它是从 InternLM2 继续预训练的，将序列到序列格式中的思维链推理、奖励建模、形式推理、数据增强和代码解释器统一起来，监督我们的模型成为一个多功能的数学推理者、验证者、证明者和扩充器。我们的预训练模型在各种非正式和正式基准测试中，包括 GSM8K、MATH、匈牙利数学考试、MathBench-ZH 和 MiniF2F，在即时学习、监督微调和代码辅助推理的环境设置下，取得了最先进的性能，MiniF2F 测试集上实现了 30.3 的成绩。我们进一步探索了如何使用 LEAN 解决数学问题，并研究了在多任务学习的环境设置下的性能，这表明了使用 LEAN 作为数学问题求解和证明的统一平台的可能性。我们的模型、代码和数据已在 https://github.com/InternLM/InternLM-Math 上发布。

Feb, 2024

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

Jun, 2024

LLMs tend to generate lengthy and unnecessary calculations on the math QA dataset GSM8K-Zero, even though the questions can be answered without any calculations.

Jan, 2024