ARCH-COMP24 Category Report: Artificial Intelligence and Neural Network Control System (AINNCS) for Continuous and Hybrid Systems Plants

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with artificial intelligence (AI) components. Specifically, machine learning (ML) components in cyber-physical systems (CPS), such as feedforward neural networks used as feedback controllers in closed-loop systems, are considered, which is a class of systems classically known as intelligent control systems, or in more modern and specific terms, neural network control systems (NNCS). We broadly refer to this category as AI and NNCS (AINNCS). The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2024. In the 8th edition of this AINNCS category at ARCH-COMP, five tools have been applied to solve 12 benchmarks, which are CORA, CROWN-Reach, GoTube, JuliaReach, and NNV. This is the year with the largest interest in the community, with two new, and three previous participants. Following last year’s trend, despite the additional challenges presented, the verification results have improved year-over-year. In terms of computation time, we can observe that the previous participants have improved as well, showing speed-ups of up to one order of magnitude, such as JuliaReach on the TORA benchmark with ReLU controller, and NNV on the TORA benchmark with both heterogeneous controllers.