arXiv:2505.04539v1 宣告类型: 新
摘要: 在处理转移概率的不确定性时，鲁棒马尔可夫决策过程（RMDPs）通过定义一组可能的转移函数来扩展经典MDPs。目标是一组RMDP的运行（或无限轨迹），而目标的价值是在对抗环境中代理能保证的最大概率。我们考虑了(a)可达性目标，其中给定一个目标状态集，目标是最终到达其中一个；(b)帕里ty目标，这是ω-正规目标的一种标准表示。质化分析问题询问是否可以以100%的概率确保目标的实现。
本文中，我们在没有对RMDP结构做出任何假设（例如，单链或无周期性）的情况下，研究了可达性和帕里ty目标的质化问题。我们的贡献有两个方面。我们首先提出了具有不确定集合访问器的高效算法，用于解决可达性和帕里ty目标的质化问题。然后，我们报告了实验结果，展示了基于访问器的方法在文献中经典RMDP示例上的有效性，这些示例扩展到了数千个状态。
arXiv:2505.04528v1 宣告类型: 新
摘要: 作为一个看似自解释的任务，问题解决一直是科学和工程中的一个重要组成部分。然而，问题解决本身的通用且具体的表述仍然缺失。随着基于AI的问题解决代理的 recent 发展，过程级可验证的需求正在迅速增加但尚未得到充分开发。为填补这些空白，我们提出了一种问题解决的原理性表述，作为确定性马尔可夫决策过程；一种新型框架 FPS（形式化问题解决），利用现有的 FTP（形式化定理证明）环境进行过程验证的问题解决；以及 D-FPS（演绎 FPS），通过分离求解和答案验证以实现更好的人类对齐。框架的表达能力、正确性和完备性得到了证明。我们构建了三个问题解决基准：FormalMath500，MATH500 基准的一个形式化部分；MiniF2F-Solving 和 PutnamBench-Solving，FTP 基准 MiniF2F 和 PutnamBench 的适应版本。为了进行忠实、可解释且人类对齐的评估，我们提出了 RPE（受限命题等价性），这是一种通过形式验证确定答案正确性的符号方法。我们评估了四种流行的 FTP 模型和两种提示方法作为基线，在 FormalMath500 中最多解决了 23.77%，在 MiniF2F-Solving 中解决了 27.47%，在 PutnamBench-Solving 中解决了 0.31%。
arXiv:2505.04525v1 声明类型: 新
摘要: 本文首次对四种未经过实验测试的 Unbounded Best-First Minimax 算法的修改版本进行了实验评估。该算法通过迭代扩展当前部分游戏树中最有希望的动作序列来探索游戏树。我们首先评估了转置表的使用情况，它通过合并重复状态将游戏树转换为有向无环图。其次，我们将 Korf & Chickering 的原始算法与 Cohen-Solal 提出的变体进行了比较，后者在回传策略上有所不同：在遇到稳定值时不会停止，而是更新值直到根节点。这一变化在涉及值匹配或转置表时略微提高了性能。第三，我们评估了用学习得来的启发式函数替换准确的终端评估函数的效果。虽然在准确评估成本较高的情况下有利，但此修改在成本较低的设置中会降低性能。最后，我们研究了优先处理已解决的胜利状态并避免已解决的失败状态的完成技术，这种技术也提高了性能。总体而言，我们的发现强调了有针对性的修改如何可以提升 Unbounded Best-First Minimax 的效率。
arXiv:2505.04480v1 宣布类型: 新
摘要: 轨迹预测是建模人类行为的关键任务，特别是在社交机器人和自主车辆导航领域。传统的基于手工crafted规则的启发式方法往往缺乏准确性，而最近提出的深度学习方法则面临着计算成本高、可解释性差以及泛化能力差等问题，这些都限制了它们的实用应用。本文介绍了一种名为TrajEvo的框架，该框架利用大型语言模型（LLMs）自动生成轨迹预测启发式方法。TrajEvo采用进化算法从过去的轨迹数据中生成和改进预测启发式方法。我们引入了一种跨代精英采样方法以促进群体多样性，并引入了一个统计反馈循环，使得LLM能够分析替代预测。我们的评估结果表明，TrajEvo在ETH-UCY数据集上优于以前的启发式方法，并且在泛化到未见过的SDD数据集时，TrajEvo远远优于启发式方法和深度学习方法。TrajEvo代表了向自动化设计快速、可解释和可泛化的轨迹预测启发式方法迈出的第一步。我们将在https://github.com/ai4co/trajevo公开我们的源代码，以促进未来的研究。
arXiv:2505.04352v1 宣布类型: 新增
摘要: 机器伦理决策应考虑决策中的不确定性影响。应通过一系列行动来实现长期的最优结果。然而，评估结果时可能需要应用一种或多种道德理论，这可能会导致相互矛盾的判断。每种理论都要求对伦理情况进行不同的描述。例如，功利主义衡量数值，道义论分析义务，美德伦理强调道德品质。在平衡潜在冲突的道德考量时，可能需要做出决定，例如，以最低的成本实现道德中立的目标。在本文中，我们将该问题形式化为多道德马尔可夫决策过程和多道德随机最短路径问题。我们基于多目标AO*开发了一个启发式算法，并利用Sven-Ove Hansson的假设回顾程序来进行不确定性环境下的伦理推理。我们的方法通过机器伦理文献中的一个案例研究得到了验证：是否应窃取胰岛素供需要的人使用的问题。
arXiv:2505.04317v1 通知类型: 新
摘要: 在这篇论文中，我们探讨了学习玩3v3多无人机排球的问题，这是一个新的具身竟技任务，要求同时具备高级战略协调能力和低级敏捷控制能力。该任务是轮换进行、多智能体且基于物理的，由于其长时依赖性、智能体间紧密耦合以及四旋翼的欠驱动动态，提出了重大挑战。为应对这一挑战，我们提出了层次化共自演（HCSP），这是一种层次化的强化学习框架，将集中式的高层战略决策与分散式的低层运动控制分离。我们设计了一个基于群体的三阶段训练流程，以使策略和技能从头开始涌现，无需专家演示：(I) 训练多种低级技能，(II) 使用固定低级控制器进行自演以学习高层策略，和(III) 通过共自演进行联合微调。实验表明，HCSP在性能上表现出色，相对于非层次化自演和两阶段变体的基于规则的层次化基线，平均胜率分别为82.9%和71.5%。此外，共自演导致了诸如角色转换和协调队形等新兴团队行为的出现，展示了我们层次化设计和训练方案的有效性。
arXiv:2505.04313v1 通知类型: 新
摘要: 在本文中，我们介绍了KERAIA，一种用于符号知识工程的新型框架和软件平台，旨在解决在动态、复杂和语境敏感环境中表示、推理和执行知识的持续挑战。这项工作的主要研究问题是：如何有效地将结构不明确、往往是隐性的人类专长转变为计算上可行的算法，供人工智能系统高效利用？KERAIA 通过基于基础概念如明斯基框架推理和 K 线，同时引入了重大创新来弥合这一差距。这些创新包括知识云进行动态聚合、动态关系 (DRels) 用于语境敏感继承、显式思路线 (LoTs) 用于可追溯的推理，以及云详述 (Cloud Elaboration) 用于适应性知识转换。这种方法超越了传统、通常是静态的知识表示范式的限制。KERAIA 以可解释人工智能 (XAI) 为核心原则，确保透明性和可解释性，特别是通过 LoTs。本文详细介绍了该框架的架构、KSYNTH 表示语言和通用目的推理方法构建器 (GPPB)，以在统一结构中整合各种推理方法。我们通过涉及海军战争模拟、水处理厂的工业诊断和 RISK 游戏的战略决策等多个案例研究，详细分析验证了 KERAIA 的灵活性、表达能力和实践可行性。此外，我们还进行了与已确立的知识表示范式（包括本体、基于规则的系统和知识图谱）的比较分析，并讨论了 KERAIA 平台的实施方面和计算考虑。
arXiv:2505.04310v1 宣告类型: 新
摘要: 我们介绍了一种新的分布强化学习(DistRL)架构，使用归一化流来建模回报分布。这种方法允许回报分布具有灵活的、无界的支撑，这与依赖于固定或有界的表示方法的类别化方法（如C51）不同。它还能够比基于分位数的方法更好地捕捉多模态、偏斜度和尾部行为，同时具有更高的参数效率。常用的用于训练现有模型的标准度量标准（如KL散度或Wasserstein距离）要么对尺度不敏感，要么在回报支撑不重叠时有有偏样本梯度。为了解决这个问题，我们提出了一种新的Cramér距离的替代方案，这种替代方案是几何感知的，并可以直接从回报分布的PDF计算得出，避免了昂贵的CDF计算。我们在ATARI-5子基准测试中测试了我们的模型，并表明我们的方法在保持与基于分位数方法竞争力的同时，优于基于PDF的方法。
arXiv:2505.04115v1 宣告类型: 新
摘要: 在人工智能中，处理不确定性是一个基本的挑战。正如大多数这些挑战一样，语言表达能力与推理带来的计算问题的可处理性之间存在着严峻的矛盾。受到人类推理的启发，我们提出了一种满足这两个标准的一阶关系概率推理方法，并能处理混合（离散和连续）变量。具体而言，我们将期望的和式逻辑扩展到关系设置中，证明即使面对事先未知且/或可数无穷的对象集，在有界量词秩的知识库的有界度片段中进行提升推理可以在多项式时间内完成。关键的是，我们关于可处理性的概念是以证明论术语提出的，这超越了语言或查询的语法属性。我们能够通过证明程度和规模证明得出最紧的界限，并为固定程度建立了和式逻辑反驳的完整性。
arXiv:2505.04019v1 通知类型: 新
摘要: 在现代机器学习中，解释预测模型的重要性已经得到了广泛认可。然而，除了模型可解释性之外，理解预处理方法同样至关重要。了解数据修改如何影响模型性能提升和潜在偏差，并促进可靠的工作流程是开发稳健的机器学习解决方案的必要条件。孤立森林（iForest）是一种广泛使用的异常检测技术，表现良好。随着基于树的学习器数量的增加，其有效性也会提高。然而，这也使异常选择和内点决策边界解释复杂化。本研究引入了一种新型的可解释人工智能（XAI）方法，以解决全球解释性的难题。具体而言，它旨在为异常检测提供一个全局解释，以解决其不透明性问题。我们的方法基于决策谓词图（DPG），该方法阐明了集成方法的逻辑，并提供了见解以及基于图的度量，以解释如何使用所提出的内点-异常传递分数（IOP-Score）识别样本为异常。我们的提议增强了 iForest 的可解释性，并提供了决策过程的全面视图，详细说明了哪些特征有助于异常识别以及模型如何利用这些特征。通过提供决策边界的见解和全面的特征使用视图，该方法推动了最先进的技术水平，从而促进了一个完全可解释的机器学习管道。