LTL Verification of Memoryful Neural Agents
By: Mehran Hosseini, Alessio Lomuscio, Nicola Paoletti
Potential Business Impact:
Checks if AI teams follow rules correctly.
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.
Similar Papers
An Approach to Checking Correctness for Agentic Systems
Artificial Intelligence
Finds mistakes in AI actions, not just words.
Verifying Memoryless Sequential Decision-making of Large Language Models
Artificial Intelligence
Checks if AI makes safe choices in games.
Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems
Multiagent Systems
Checks if real-time computer systems work right.