# Formal Verification of Learned Multi-Agent Communication Policies via Decision Tree Distillation

arXiv: https://arxiv.org/abs/2606.19632 · HTML: https://mlsanity.com/paper/2606.19632/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 29 references that are in the map.
- First posted on arXiv 17 Jun 2026.

## Builds on (most cited first, 16 of 16)

- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [Neural Discrete Representation Learning](https://mlsanity.com/paper/1711.00937/) (2017)
- [The Surprising Effectiveness of PPO in Cooperative, Multi-Agent Games](https://mlsanity.com/paper/2103.01955/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Monotonic Value Function Factorisation for Deep Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2003.08839/) (2020)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Learning Multiagent Communication with Backpropagation](https://mlsanity.com/paper/1605.07736/) (2016)
- [TarMAC: Targeted Multi-Agent Communication](https://mlsanity.com/paper/1810.11187/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [Toward Interpretable Deep Reinforcement Learning with Linear Model U-Trees](https://mlsanity.com/paper/1807.05887/) (2018)
- [Cautious Reinforcement Learning with Logical Constraints](https://mlsanity.com/paper/2002.12156/) (2020)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Learning Safe Control for Multi-Robot Systems: Methods, Verification, and Open Challenges](https://mlsanity.com/paper/2311.13714/) (2023)
- [MAVIPER: Learning Decision Tree Policies for Interpretable Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2205.12449/) (2022)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Bandwidth-Efficient Multi-Agent Communication through Information Bottleneck and Vector Quantization](https://mlsanity.com/paper/2602.02035/) (2026)

## Abstract (arXiv)

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.