mlsanityData to 7 Oct 2026

LTL Verification of Memoryful Neural Agents

arXiv 2503.02512 ↗First posted 4 Mar 2025cs.LO cs.AI cs.LGcited by 0

Not on the map. Why?

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.

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

Builds on

17 of 59 references.

References · 17

  1. 2023Mamba: Linear-Time Sequence Modeling with Selective State Spacescited by 4,616
  2. 2013Playing Atari with Deep Reinforcement Learningcited by 3,211
  3. 2015Deep Recurrent Q-Learning for Partially Observable MDPscited by 457
  4. 2017Wild Patterns: Ten Years After the Rise of Adversarial Machine Learningcited by 411
  5. 2014Memory Networkscited by 354
  6. 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 322
  7. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
  8. 2020PettingZoo: Gym for Multi-Agent Reinforcement Learningcited by 209
  9. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  10. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  11. 2017An approach to reachability analysis for feed-forward ReLU neural networkscited by 126
  12. 2019POPQORN: Quantifying Robustness of Recurrent Neural Networkscited by 36
5 more
  1. 2017Recurrent Neural Networks as Weighted Language Recognizerscited by 30
  2. 2020Verifying Recurrent Neural Networks using Invariant Inferencecited by 25
  3. 2021Certification of Iterative Predictions in Bayesian Neural Networkscited by 8
  4. 2022Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Gamescited by 5
  5. 2022Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Gamescited by 3

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026LOGIGEN: Logic-Driven Generation of Verifiable Agentic Tasks
  2. 2026hint2: Hierarchical World Models for Inference-Time Temporal Logic Guidance
  3. 2026PlatoLTL: Scaling LTL-Guided Multi-Task RL
  4. 2026Verification and Self-Improvement in Agentic AI: Foundations and Limits
  5. 2026Advancing Multimodal Agent Reasoning with Long-Term Neuro-Symbolic Memory
  6. 2026Scaling the Scaling Logic: Agentic Meta-Synthesis of Logic Reasoning
  7. 2026Memory for Autonomous LLM Agents:Mechanisms, Evaluation, and Emerging Frontiers
  8. 2026MAS-ProVe: Understanding the Process Verification of Multi-Agent Systems