TACPS 2025-July In Conjunction with CAV 2025

The 3rd TACPS: Neurosymbolic and Foundation Models for AI verification
in Autonomous CPS

Introduction

The integration of machine learning (ML) into cyber-physical systems (CPS) has revolutionized applications such as self-driving cars, delivery drones, service robotics, and automated medical procedures. However, the deployment of these systems has brought safety and reliability concerns to the forefront, with real-world failures resulting in fatalities and economic losses. These incidents underscore the urgent need for robust verification and validation methodologies tailored to ML-driven CPS.

Traditional verification techniques face significant challenges in addressing the complexities of ML components within CPS. These challenges include the reliance on representative training data, susceptibility to out-of-distribution inputs, and the black-box, non-explainable nature of ML models. Existing tools, such as hybrid automata, fall short of adequately modeling and reasoning about these systems, necessitating innovative approaches to ensure their safety and reliability.

Emerging technologies, particularly neurosymbolic methods and foundation models like Large Language Models (LLMs), offer transformative potential in this domain. By combining symbolic reasoning with data-driven learning, these approaches facilitate the generation of interpretable representations, extraction of formal specifications, and rigorous handling of uncertainty in ML-based systems. Such advancements not only enhance test generation and issue discovery but also pave the way for extending formal verification to learning-enabled CPS. These contributions are critical for addressing the probabilistic behaviors and transparency challenges inherent in AI components, making them pivotal for the verification and reliability of autonomous CPS.

This workshop aims to bring together researchers and practitioners from the verification, ML, and CPS communities to explore the integration of neurosymbolic approaches and foundation models into the formal verification landscape. Through interdisciplinary discussions, the workshop seeks to advance the state-of-the-art in verifying learning-enabled CPS and ensuring the safety and reliability of AI-driven autonomous systems.