利用大型语言模型（LLMs）加速研究理论计算机科学和数学中最重要的开放性问题之一 P 与 NP 问题的一项工作，提出了一种名为苏格拉底推理的广义框架，通过 LLMs 促进复杂问题解决的深度思考。实验证明 GPT-4 在 97 次对话中通过苛刻的推理得出结论 “P≠NP”，从而揭示了 LLMs 广泛解空间中的新见解，为科学中的 LLMs 提供了启示。

Sep, 2023

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

Nov, 2023

近年来，在数学领域中，利用语言模型（LMs）取得了显著进展，本文从任务和方法论两个不同的角度对数学 LMs 进行了全面的调查和分类，揭示出大量的数学 LLMs 和超过 60 个数学数据集的应用和研究。

Dec, 2023

通过创建 MathVista 基准测试，研究提出了对于大型语言模型和大型多模态模型在数学推理和视觉背景下的能力的正式研究，并详细评估了 11 种不同模型的性能，为未来的通用 AI 代理的发展提出了挑战。

Oct, 2023

数学推理是评估人类智能基本认知能力的基石。该研究调查了大型语言模型在解决数学问题方面的真正进展、障碍、数学问题类型和相关数据集、解决数学问题的 LLM 技术范围、影响 LLMs 解决数学问题的因素和问题，并提供了这一快速发展领域中的现状、成就和未来挑战的整体观点。

Jan, 2024

自主规划和调度是人工智能中增长最快的领域之一，本研究通过对 126 篇论文进行全面检视，调查了 LLMs 在地址规划问题的各个方面时的独特应用，并提出了八个类别：语言翻译、计划生成、模型构建、多智能体规划、交互规划、启发式优化、工具集成以及脑启发式规划，强调 LLMs 与传统符号规划器的结合展示出潜力，揭示出一种有前景的神经符号化方法。

Jan, 2024

通过评估最先进的大型视觉和语言模型在儿童奥林匹克数学竞赛中的数学推理能力，我们填补了当前科学文献中缺少的有关联合视觉和文本推理的系统分析，结果显示现代大型视觉和语言模型在高年级的问题解决能力越来越强，但缺乏解答针对年幼儿童设计的问题的基础知识，而且它们的能力似乎基于与儿童的数学和逻辑技能不同的推理类型。

Jun, 2024

大语言模型在多步数学推理方面表现出色，但包含文字和图像的数学推理问题需要评估视觉语言模型的推理能力。通过几何问题的镜头，我们通过多个角度评估视觉语言模型的推理能力。我们创建了一个合成的几何问题数据集，具有可控的难度级别，从而进行系统评估。我们的基准测试结果表明，这些模型在几何等主题的推理能力上并不如先前的基准测试所暗示的那样出色，特别是通过我们基准测试的多个深度级别构建，因为解决更深的问题需要更长的推理链而不是额外的记忆知识。我们释放这个数据集供进一步研究使用。

Dec, 2023

该论文研究了大型语言模型在数学问题推理方面的能力，特别关注符号推理在数值问题中的准确性，并通过自提示的方法提高了符号准确性，为模型提供了简洁可验证的推理能力。

Aug, 2023

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

Jun, 2024