该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助和自动化程度的有效性。

Apr, 2024

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

Sep, 2020

本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。

May, 2019

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

Feb, 2021

基于大型语言模型的基于规划的对话代理框架（PCA）能通过离线制定核心和必要的 SOP，实现在线规划最佳行动路径以实现对话的可控性和前瞻性。实验证明，经过细调的 LLMs 在 PCA-D 上可以显著提高性能并具备广泛的泛化能力，而 PCA-M 则在对话的可控性、前瞻性、任务成功率和整体逻辑连贯性方面优于其他基准，并适用于工业对话场景。

Jul, 2024

本文介绍了基于 Monte Carlo 搜索算法的新型大语言模型推理框架 RAP，利用其上的世界模型进行计划生成和复杂推理。从多个任务测试中，RAP 在效率和准确率上都超过了 Chain-of-Thought 等现有方案。

May, 2023

在全面自主的机器人系统领域，本研究通过提出系统架构来解决复杂开放世界环境中任务与动作规划的挑战，核心是处理生成计划中的物理、逻辑和语义错误的重规划策略。通过在仿真和两个复杂的现实场景中进行实证评估，我们展示了所提出的反馈架构对可执行性、正确性和时间复杂性的有效性。

Oct, 2023

这篇研究论文探索了大型语言模型在用户指令理解和决策方面的潜力，并提出了一种新的任务，即主动性代理规划。通过建立一个新的基准数据集和提出一个多代理框架，研究者验证了所提出框架的有效性。

Jun, 2024

建立具有适应性行为的人工智能在人工智能与人类合作中具有重要的研究焦点。本研究提出了一种名为 ProAgent 的新框架，利用大型语言模型来预测合作伙伴的决策并改进自身计划。实验证明，ProAgent 在与人工智能代理和人类合作中表现出显著优越性能，为人类与机器人协作的未来研究提供了启示。

Aug, 2023

LogicLLaMA 是一种基于 LLaMA-7B 模型的、使用 LoRA 进行 NL-FOL 翻译的算法，通过新颖的 SFT+RLHF 框架进行调整，能够将自然语言直接翻译为一阶逻辑规则，并具有对 GPT-3.5 生成的规则进行校正的能力。

May, 2023