# LTL Verification of Memoryful Neural Agents

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 17 of its 59 references that are in the map.
- First posted on arXiv 4 Mar 2025.

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

- [Mamba: Linear-Time Sequence Modeling with Selective State Spaces](https://mlsanity.com/paper/2312.00752/) (2023)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Deep Recurrent Q-Learning for Partially Observable MDPs](https://mlsanity.com/paper/1507.06527/) (2015)
- [Wild Patterns: Ten Years After the Rise of Adversarial Machine Learning](https://mlsanity.com/paper/1712.03141/) (2017)
- [Memory Networks](https://mlsanity.com/paper/1410.3916/) (2014)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [PettingZoo: Gym for Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2009.14471/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [POPQORN: Quantifying Robustness of Recurrent Neural Networks](https://mlsanity.com/paper/1905.07387/) (2019)
- [Recurrent Neural Networks as Weighted Language Recognizers](https://mlsanity.com/paper/1711.05408/) (2017)
- [Verifying Recurrent Neural Networks using Invariant Inference](https://mlsanity.com/paper/2004.02462/) (2020)
- [Certification of Iterative Predictions in Bayesian Neural Networks](https://mlsanity.com/paper/2105.10134/) (2021)
- [Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2202.06255/) (2022)
- [Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2205.07546/) (2022)

## Abstract (arXiv)

We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA.