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

Sep, 2020

我们提出了 TRIGO，一个自动定理证明基准测试，要求模型能够逐步证明简化三角表达式，并评估生成型语言模型在公式推理、数字项操作、分组和因式分解方面的推理能力。我们从互联网收集三角表达式及其简化形式，并用 ``Lean'' 形式语言系统注释简化过程，然后自动从标注样本中生成额外的示例来扩充数据集。通过基于 Lean-Gym 的自动生成器创建不同难度和分布的数据集来全面分析模型的泛化能力。我们的广泛实验显示，TRIGO 对于包括在大量开源形式定理证明语言数据上预训练的 GPT-4 在内的先进生成型语言模型提出了新的挑战，并为研究生成型语言模型在形式和数学推理上的能力提供了新工具。

Oct, 2023

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

Feb, 2020

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

May, 2022

通过使用自动化问题生成的方法，我们实现了针对每个学生的定制问题，研究了针对离散数学的逻辑等价问题的自动问题生成方法，并证实了该方法在教育中自动化问题生成方面的实用性。

May, 2024

本文介绍了一个以定理驱动的问答数据集 TheoremQA，用于评估人工智能模型应用定理解决具有挑战性的科学问题的能力。研究人员使用 16 个大型语言和代码模型评估 TheoremQA，并发现 GPT-4 在 Program-of-Thoughts Prompting 的帮助下解决这些问题的能力是无与伦比的，达到了 51％，而现有的所有开放源代码模型都低于 15％，仅仅超过了随机猜测的基线。

May, 2023

利用迭代式多智能体对抗调整，通过 ATM 系统，大型语言模型 (LMM) 可以区分真假相关文件，并且在 RAG 管道中实现更好的性能表现。

May, 2024

提出基于深度学习技术的 OLGA 系统，其中利用领域知识以检查算术单词问题的一致性，使用 LSTM 模型生成语言变化的文本，结合 TC 本体论扩展 2 人 TC 问题生成符合要求的 3 人 TC 问题，能够生成大量一致的 TC 类型算术单词问题。

Nov, 2022

这项研究介绍了一个专门用于评估大型语言模型在多主体环境中能力的基准测试框架，通过游戏和博弈论场景来创建不同的测试环境，并利用概率图模型方法增强模型的导航能力，最终量化评估了七种不同大型语言模型的能力，发现最强模型 GPT-4 和最弱模型 Llama-2-70B 之间存在三倍的能力差距，同时证实了概率图模型增强了所有模型的能力，平均提高了 50%。

Nov, 2023

我们提出了一种基于动态任务分解和代理生成（TDAG）的多代理框架，该框架将复杂任务动态分解为较小的子任务，并将每个子任务分配给生成的特定子代理，在增强多样且不可预测的真实世界任务中提高适应性。同时，我们引入了 ItineraryBench 作为旅行规划领域的评估系统来评估智能体在记忆、规划和工具使用等不同复杂性任务中的能力，实验结果表明 TDAG 在复杂任务场景中展现出卓越的适应性和上下文感知能力。

Feb, 2024