LTL Verification of Memoryful Neural Agents
This work addresses verification challenges for neural agents in safety-critical applications, representing an incremental advance with specific performance gains.
The paper tackles the problem of verifying memoryful neural multi-agent systems against full Linear Temporal Logic specifications, achieving verification of unbounded specifications for the first time and improving verification time for bounded specifications by an order of magnitude compared to state-of-the-art methods.
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.