将多智能体通信策略转为可验证的决策树，确保无人机编队安全。
Formal Verification of Learned Multi-Agent Communication Policies via Decision Tree Distillation
- 用决策树抽象神经网络策略，提升可解释性与可验证性
- 在5-7个智能体场景下验证18条逻辑性质，碰撞概率低至0.3%
- 适合需形式化安全保证的无人机、自动驾驶车队部署
多智能体强化学习使智能体通过涌现通信发展协作策略，但神经网络策略缺乏安全关键场景（如无人机编队、自动驾驶车队）所需的形式化安全保证。本文提出首个端到端框架，通过策略抽象实现学习型多智能体通信策略的安全验证：将神经策略蒸馏为可解释决策树，再进行形式化验证，并通过实证验证确认已验证安全属性可迁移至原始网络。四阶段流程包括：从智能体观测中提取领域特征、决策树蒸馏达到97.9% ±1.2%的保真度、自动转换为PRISM概率模型检查器规范并确保特征与状态变量完全对应、通过成对分解与并集界聚合实现概率计算树逻辑（PCTL）性质的组合验证及经验邻域建模。在5-7个智能体的多无人机协调任务中，对向量量化变分信息瓶颈（VQ-VIB）策略进行评估，验证了18项包含安全、活性与合作的时序逻辑性质，达成88.9%的性质满足率，全部五项安全阈值均达标（碰撞概率0.3% < 1%阈值）。蒙特卡洛验证原始神经网络表明，经验证的安全属性转移偏差不超过0.6个百分点（95%置信区间）。离散式VQ-VIB消息相比连续方法提升11.6至13.6个百分点保真度，实现3-4倍加速验证。本框架为蒸馏策略抽象提供了实证验证的安全性保障，成为深度多智能体强化学习与形式化安全流程之间实用的桥梁。
原文摘要 · Abstract (English)
Multi-agent reinforcement learning (MARL) enables agents to develop coordination strategies through emergent communication, but neural policies lack the formal safety guarantees required for safety-critical robotic deployment in drone swarms and autonomous vehicle fleets. We present the first end-to-end framework for safety verification of learned multi-agent communication policies through policy abstraction: neural policies are distilled into interpretable decision trees, then formally verified, with empirical validation confirming that verified safety properties transfer to original networks. Our four-stage pipeline consists of domain-specific feature extraction from agent observations, decision tree distillation achieving 97.9% +/- 1.2% fidelity to neural policies, automated translation to PRISM probabilistic model checker specifications with complete feature-to-state-variable correspondence, and compositional verification of Probabilistic Computation Tree Logic (PCTL) properties via pairwise decomposition with union-bound aggregation and empirical neighbor modeling. Evaluating Vector-Quantized Variational Information Bottleneck (VQ-VIB) policies for multi-drone coordination with 5-7 agents, we verify 18 temporal logic properties across safety, liveness, and cooperation, achieving 88.9% property satisfaction with all five safety thresholds satisfied (0.3% collision probability vs. 1% threshold). Monte Carlo validation of original neural policies confirms that verified safety properties transfer with <=0.6 percentage-point deviation (95% CI). Discrete VQ-VIB messages provide +11.6 to +13.6 percentage-point fidelity advantages over continuous methods, enabling 3-4x faster verification. Our framework provides empirically validated safety verification for distilled policy abstractions, serving as a practical bridge between deep MARL and formal safety workflows for multi-robot deployment.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。