数据库中的溯源问题已经针对正查询和递归查询进行了深入研究，随后又针对一阶（FO）查询进行了研究，即包含否定但没有递归的查询。查询评估可以理解为一个双人博弈，其中对手争论一个元组是否在查询答案中。这种博弈论方法为 FO 查询提供了一个自然的溯源模型，统一了如何溯源和为什么不溯源。本文研究了博弈溯源的精细结构。一个博弈 $G=(V,E)$ 由位置 $V$ 和移动 $E$ 组成，可以通过计算单个非分层规则的良基模型来求解： \[ \text{win}(X) \leftarrow \text{move}(X, Y), \neg \, \text{win}(Y). \] 在求解后的博弈 $G^{\lambda}$ 中，位置 $x\,{\in}\,V$ 的值要么是赢，要么是输，要么是平局。这个值由溯源 $\mathscr{P}$(x) 解释，即从 $x$ 可达的某些（带注释的）边。我们识别了七种边类型，它们产生了新的溯源类型，即潜在的、实际的和主要的，并证明了“并非所有移动都一样”。我们描述了新的溯源类型，展示了如何在求解博弈的同时计算它们，并讨论了应用，例如，用于抽象论证框架。
大型语言模型 (LLM) 在自然语言处理、数学问题求解和程序合成相关任务中展现出非凡的能力。然而，人们注意到它们在长期规划和高阶推理方面的有效性有限且脆弱。本文探讨了一种通过整合求解器生成的反馈来增强 LLM 在解决经典机器人规划任务中的性能的方法。我们探索了四种不同的反馈提供策略，包括视觉反馈，我们利用微调，并在 10 个标准问题和 100 个随机生成的规划问题上评估了三种不同 LLM 的性能。我们的结果表明，求解器生成的反馈提高了 LLM 解决中等难度问题的的能力，但更难的问题仍然无法触及。该研究详细分析了不同提示策略的影响以及评估的 LLM 的不同规划倾向。
尽管现有的神经网络车辆路径规划问题 (VRP) 方法在效率和减少对领域专业知识的依赖方面具有优势，但它们存在严重的鲁棒性问题——其性能在经过精心设计的扰动处理的干净实例上会显著下降。为了增强鲁棒性，我们针对神经网络 VRP 方法的防御，提出了一种基于集成协作神经框架 (CNF) 的方法，该方法在文献中至关重要，但尚未得到充分探索。给定一种神经网络 VRP 方法，我们以协作方式对抗性地训练多个模型，以协同促进对攻击的鲁棒性，同时提高干净实例上的标准泛化能力。设计了一个神经路由器，可以熟练地将训练实例分配到各个模型中，从而增强整体负载平衡和协作效率。大量实验验证了 CNF 在防御不同神经网络 VRP 方法中的各种攻击方面的有效性和通用性。值得注意的是，我们的方法还在基准实例上实现了令人印象深刻的分布外泛化能力。
在竞技游戏领域，3D第一人称射击（FPS）游戏已经获得了巨大的普及，促使人们开发游戏AI系统来增强游戏体验。然而，在实际场景中部署游戏AI仍然存在挑战，特别是在大型复杂FPS游戏中。本文重点研究了游戏AI在腾讯游戏开发的在线多人竞技3D FPS游戏《Arena Breakout》中的实际部署。我们提出了一种名为“私人军事公司代理”（PMCA）的新型游戏AI系统，该系统可以在大型游戏地图中互动，与玩家进行战斗，同时利用周围地形提供的战术优势。
为了解决现代3D FPS游戏中导航和战斗的挑战，我们引入了一种将导航网格（Navmesh）和射击规则与深度强化学习（NSRL）相结合的方法。Navmesh的整合增强了代理的全局导航能力，而基于规则的方法控制射击行为，以确保可控性。NSRL采用DRL模型来预测何时启用导航网格，从而为游戏AI带来多种行为。还采用了针对类人行为的定制奖励，使PMCA的行为与人类玩家的行为保持一致。
这项工作提出了一种可解释的自动驾驶决策框架，该框架全面整合了交通法规、规范和安全准则，并能够无缝适应不同地区。虽然传统的基于规则的方法难以包含交通规则的全部范围，但我们开发了一种基于检索增强生成 (RAG) 的交通法规检索 (TRR) 代理，以根据自车情况从大量法规文件和相关记录中自动检索相关的交通规则和指南。鉴于检索到的规则的语义复杂性，我们还设计了一个由大型语言模型 (LLM) 支持的推理模块，以解释这些规则，区分强制性规则和安全指南，并评估行动的法律合规性和安全性。此外，推理的设计是可解释的，从而增强了透明度和可靠性。该框架在各种场景中对假设情况和现实情况都展现出强大的性能，并且能够轻松地适应不同的地区。
大型语言模型（LLMs）已被用于在 Lean 等证明助手中生成数学定理的形式化证明。然而，我们经常希望根据证明的后续用途，针对各种标准优化形式化证明。例如，我们可能希望证明符合某种风格，或者易于阅读、简洁或模块化结构。拥有适当优化的证明对于学习任务也很重要，尤其是因为人类编写的证明可能不适合该目的。为此，我们研究了一种新的自动证明优化问题：重写证明，使其正确并针对长度或可读性等任意标准进行优化。作为第一个自动证明优化方法，我们提出了 ImProver，这是一个大型语言模型代理，它重写证明以优化 Lean 中任意用户定义的指标。我们发现，将 LLMs 朴素地应用于证明优化效果不佳，我们在 ImProver 中加入了各种改进，例如在一种新颖的链式状态技术中使用符号 Lean 上下文，以及错误校正和检索。我们测试了 ImProver 对真实世界的本科、竞赛和研究级数学定理的重写，发现 ImProver 能够重写证明，使其更短、更模块化、更易读。
生物医学知识具有独特的复杂性和结构性，与物理学或化学等其他科学学科相比，需要不同的推理策略。生物医学科学家并不依赖于单一的推理方法；相反，他们使用各种策略，包括基于规则的、基于原型的和基于案例的推理。这种多样性要求灵活的方法，既能适应多种推理策略，又能利用领域内知识。我们引入了 KGARevion，这是一种基于知识图谱 (KG) 的代理，旨在解决知识密集型医疗查询的复杂性。在收到查询后，KGARevion 通过使用 LLM 的知识库生成相关的三元组。然后，这些三元组将针对一个接地 KG 进行验证，以过滤掉错误信息，并确保只有准确、相关的数据有助于最终答案。与基于 RAG 的模型不同，这种多步骤过程确保了推理的稳健性，同时适应了不同的医疗推理模型。在四个黄金标准的医疗问答数据集上的评估表明，KGARevion 将准确率提高了 5.2% 以上，在处理复杂医疗问题方面优于 15 个模型。为了测试其能力，我们策划了三个新的医疗问答数据集，这些数据集具有不同的语义复杂性，其中 KGARevion 的准确率提高了 10.4%。
线性时序逻辑 (LTL) 近年来被用作一种强大的形式化方法，用于在强化学习 (RL) 中指定复杂、时间延长的任务。然而，学习能够有效满足训练期间未观察到的任意规范的策略仍然是一个具有挑战性的问题。现有的方法存在一些缺陷：它们通常只适用于 LTL 的有限范围片段，仅限于次优解，并且没有充分处理安全约束。在这项工作中，我们提出了一种新颖的学习方法来解决这些问题。我们的方法利用 Büchi 自动机的结构，该结构明确表示 LTL 规范的语义，来学习根据导致满足所需公式的一系列真值赋值来学习策略。在各种离散和连续域中的实验表明，我们的方法能够零样本满足各种有限和无限范围的规范，并且在满足概率和效率方面都优于现有方法。
在海上环境中，使用航行中的水上交通工具在两架飞机之间转运患者可以增加医疗后送的范围和灵活性。由于参与飞机的利用历史和参与水上交通工具的位置和速度，从多个航行中的水上交通工具中选择一个用于患者交换非常复杂。该选择问题被建模为一个半马尔可夫决策过程，其动作空间包括固定陆地和移动水上交通工具交换点。使用带根并行的蒙特卡洛树搜索来选择最佳交换点并确定飞机派遣时间。在模拟中改变模型参数以识别水上交通工具交换点减少事件响应时间的代表性场景。我们发现，具有水上交通工具交换点的最佳策略优于没有水上交通工具交换点的最佳策略和贪婪策略，分别提高了 35% 和 40%。与美国陆军合作，我们首次部署水上交通工具交换点，在夏威夷欧胡岛以南的两架 HH-60M 医疗后送直升机和一艘正在航行的陆军后勤支援舰之间执行了模拟患者转移，使用人体模型。两架直升机均根据我们优化的决策策略进行派遣。
知识图谱补全 (KGC) 任务旨在推断知识图谱 (KG) 中的缺失事实，以服务于许多知识密集型应用。然而，现有的基于嵌入的 KGC 方法主要依赖于事实三元组，这可能导致与常识不一致的结果。此外，为 KG 生成显式常识通常不切实际或成本高昂。为了解决这些挑战，我们提出了一种可插拔的常识增强 KGC 框架，该框架将事实和常识结合用于 KGC。该框架可根据其实体概念丰富度适应不同的 KG，并能够从事实三元组中自动生成显式或隐式常识。此外，我们引入了常识引导的负采样和针对具有丰富实体概念的 KG 的粗到细推理方法。对于没有概念的 KG，我们提出了一种涉及关系感知概念嵌入机制的双重评分方案。重要的是，我们的方法可以作为可插拔模块集成到许多知识图谱嵌入 (KGE) 模型中，促进联合常识和事实驱动的训练和推理。实验表明，我们的框架表现出良好的可扩展性，并在各种 KGC 任务中优于现有模型。