Verifying safety of neural network control systems that use images as input is a difficult problem because, from a given system state, there is no known way to mathematically model what images are possible in the real-world. We build on recent work that considers a surrogate verification approach, training a conditional generative adversarial network (cGAN) as an image generator in place of the real world. This enables set-based formal analysis of the closed-loop system, providing analysis beyond simulation and testing. While existing work is effective on small examples, excessive overapproximation both within a single control period and across multiple control periods limits its scalability. We propose approaches to overcome these two sources of error. First, we overcome one-step error by composing the system's dynamics along with the cGAN and neural network controller, without losing the dependencies between input states and the control outputs as in the monotonic analysis of the system dynamics. Second, we reduce multi-step error by repeating the single-step composition, essentially unrolling multiple steps of the control loop into a large neural network. We then leverage existing network verification tools to compute accurate reachable sets for multiple steps, avoiding the accumulation of abstraction error at each step. We demonstrate the effectiveness of our approach in terms of both accuracy and scalability using two case studies: an autonomous aircraft taxiing system and an advanced emergency braking system. On the aircraft taxiing system, the converged reachable set is 175% larger using the prior baseline method compared with our proposed approach. On the emergency braking system, with 24x the number of image output variables from the cGAN, the baseline method fails to prove any states are safe, whereas our improvements enable set-based safety analysis.
Property-Directed Verification of Recurrent Neural Networks
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay（巴黎萨克雷高等师范学院、巴黎萨克雷大学、法国国家科学研究中心、验证与安全实验室）；Inria（法国国家信息与自动化研究所）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Université Paris-Est Créteil（巴黎东大克雷泰伊校区）；Universität zu Lübeck（吕贝克大学）；CentraleSupélec（中央理工-高等电力学院）；Institut Universitaire de France（法国大学研究院）
CREDIT: Certified Ownership Verification of Deep Neural Networks Against Model Extraction Attacks
Department of Computer Science, Florida State University, Tallahassee, Florida, United States（佛罗里达州立大学计算机科学系）；Department of Mathematics, University of Wisconsin, Madison, Wisconsin, United States（威斯康星大学麦迪逊分校数学系）；Department of Computer Science, Duke University, Durham, North Carolina, United States（杜克大学计算机科学系）；Department of Statistics and Operations Research, University of North Carolina at Chapel Hill, Chapel Hill, North Carolina, United States（北卡罗来纳大学教堂山分校统计与运筹学系）
Certified Neural Approximations of Nonlinear Dynamics
Delft Center for Systems and Control（代尔夫特系统与控制中心）；Department of Computer Science, University of Oxford（牛津大学计算机科学系）；The Italian Institute of Artificial Intelligence (AI4I)（意大利人工智能研究所（AI4I））
Physics-Audited Agentic Discovery in Scientific Machine Learning
New York University Abu Dhabi（纽约大学阿布扎比分校）；National Center for Supercomputing Applications, University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校国家超级计算应用中心）
A Numerical Method for Coupling Parameterized Physics-Informed Neural Networks and FDM for Advanced Thermal-Hydraulic System Simulation
Division of Advanced Nuclear Engineering, Pohang University of Science and Technology（浦项科技大学先进核工程学部）；Mueunjae School of Undergraduate Studies, Pohang University of Science and Technology（浦项科技大学文在本科书院）；Department of Quantum System Engineering, Jeonbuk National University（全北国立大学量子系统工程系）
