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

Researchers present the first formal verification framework for multi-agent reinforcement learning (MARL) communication policies by distilling neural networks into interpretable decision trees and verifying them with probabilistic model checking. The approach achieves 97.9% fidelity to original policies while enabling safety verification for critical robotic applications like drone swarms and autonomous vehicle fleets.

This research addresses a fundamental gap between advanced AI capabilities and deployment safety requirements. Multi-agent reinforcement learning systems can develop sophisticated emergent communication strategies, but their neural network foundations lack the formal guarantees demanded by safety-critical applications. The proposed solution—distilling learned policies into decision trees before verification—represents a pragmatic bridge between cutting-edge deep learning and established formal methods.

The verification pipeline demonstrates technical sophistication across multiple domains. Decision tree distillation maintains 97.9% fidelity while dramatically improving interpretability, a crucial property for safety assurance. The translation to PRISM specifications enables automated verification of temporal logic properties covering safety, liveness, and cooperation constraints. The framework successfully verified 18 properties in multi-drone scenarios with collision probabilities held below 1% thresholds.

The practical validation is particularly significant. Monte Carlo experiments confirm that verified safety properties transfer to original neural policies with minimal deviation (≤0.6 percentage points), validating the abstraction approach's reliability. Discrete communication messages outperformed continuous alternatives by 11.6-13.6 percentage points while enabling 3-4x faster verification, suggesting design choices matter substantially for deployable systems.

For the robotics and autonomous systems industries, this framework enables evidence-based confidence in multi-agent coordination systems for real-world deployment. The approach scales to 5-7 agent scenarios, addressing immediate practical needs while maintaining formal rigor. Future work likely involves scaling to larger agent populations and handling more complex communication topologies.

• →Neural MARL policies can be distilled to decision trees with 97.9% fidelity while enabling formal verification
• →Safety properties verified through decision tree abstraction transfer to original neural networks with ≤0.6% deviation
• →Discrete communication messages provide 11.6-13.6 percentage-point fidelity improvements and 3-4x faster verification
• →Framework successfully verified 18 temporal logic properties including collision avoidance below critical thresholds
• →Approach provides practical path toward deploying multi-agent systems in safety-critical applications like drone swarms