Summary
Learning-enabled cyber-physical systems like self-driving cars use AI models but currently have incomplete methods to guarantee overall system safety. The authors suggest combining neural networks with explicit symbolic rules to better control these systems and verify their behavior. They propose a framework that uses testing, formal checks, and runtime monitoring to ensure the system behaves correctly even when AI models are uncertain or unpredictable. This approach helps create stronger safety guarantees across the entire system rather than just judging individual AI parts.
What this means in practice
- •For autonomous vehicle designers: Improve safety testing and runtime monitoring by combining AI with symbolic models to better assure whole vehicle system behavior.
- •For industrial robot developers: Develop modular contracts and verification methods integrating learned AI behaviors and formal rules for safer robot control systems.
A position paper. It proposes an approach and reports no results.
Authors
Xi Zheng, Ivan Ruchkin, Hong Jin Kang, Tevfik Bultan, Vijay Ganesh, Taylor T. Johnson, Ziyang Li, Lei Ma, Aloysius K. Mok, Daniel Neider, Ruzica Piskac, Nalini Venkatasubramanian, Simon Thompson, Sanjoy Baruah
Abstract
Learning-enabled cyber-physical systems (CPS), including autonomous vehicles and UAVs, increasingly incorporate foundation models, yet fragmented assurance practices provide insufficient support for system-level guarantees. We argue that restoring engineering control across stochastic neural, symbolic, and physical boundaries requires a shift from model-centric evaluation to system-level assurance. We introduce the Foundation Model Assurance Stack, connecting three directions: (i) neuro-symbolic architectures that constrain foundation models through explicit symbolic world models, reasoning layers, and interfaces; (ii) semantically grounded, conformance-based testing that combines formal specifications and symbolic world models with foundation-model-assisted specification mining, scenario generation, and test synthesis; and (iii) compositional verification and runtime assurance that target formally tractable components and interfaces through modular contracts, equivalence checking, verified synthesis, uncertainty-aware reasoning, and runtime monitoring and enforcement. Symbolic abstractions establish assurance boundaries between stochastic learning and formal reasoning, connecting testing, verification, and runtime evidence across the system lifecycle. Foundation models serve as constrained assistants whose outputs are independently checked wherever correctness can be formally specified. We identify research challenges in specification engineering, abstraction fidelity, evidence composition, and lifecycle certification, and outline a staged agenda toward trustworthy, deployable, and certifiable learning-enabled CPS.