ARCH-COMP25 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants
D. Lopez, M. Althoff, L. Benet, S. Coogan, M. Forets, A. Harapanahalli, T. Johnson, T. Ladner, C. Schilling, H. Zhang, X. Zhong
Proceedings of 12th Int. Workshop on Applied Verification for Continuous and Hybrid Systems, 2025
Abstract
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 2025. In this edition of the AINNCS category at ARCH-COMP, five tools have been applied to solve 12 benchmarks, which are CORA, CROWN-Reach, immrax, JuliaReach, and NNV. For the second year in a row, we have the largest interest in the community, with four previous participants and one new participant, immrax. In reusing the hardware infrastructure and benchmarks from last year, we can observe comparable results from previous improvements, with slight improvements in computation time by CORA and NNV in selected benchmarks. A novelty of this year is the different problem abstraction between immrax and the rest of tools, leading to result disparities in 2 benchmarks: Single Pendulum and Attitude Control.