PaperlayerView exact revision on arXiv

Source-linked AI summary

Assuring Learning-Enabled Cyber-Physical Systems with Foundation Models: A Neuro-Symbolic Agenda for Testing, Verification, and Runtime Assurance

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

arXiv:2610.39547v1cs.ROcs.SYeess.SY

TL;DR

Learning-enabled CPS increasingly use foundation models, but stochastic behavior and fragmented assurance leave system-level guarantees difficult to establish. The paper introduces a neuro-symbolic assurance stack connecting architecture, conformance-based testing, verification, and runtime assurance. Its conclusion is to verify what is tractable, test what must be established empirically, and constrain behavior when available evidence no longer justifies continued authority.

  • Problem

    Foundation models' stochastic, opaque behavior and uncertainty across perception, reasoning, planning, and physical execution complicate system-level assurance beyond individual model performance.

    Source: §1 · p. 3

  • Method

    The Foundation Model Assurance Stack connects symbolic world models and interfaces, conformance-based testing, compositional verification, and runtime assurance around constrained foundation-model assistants.

    Source: §1 · p. 3, §7 · p. 27

  • Results

    The paper concludes that assurance should verify formally tractable properties, test empirical conditions, monitor operational changes, and constrain behavior when evidence no longer justifies authority.

    Source: §7 · p. 27

  • Takeaways & Limitations

    Trust in safety-critical CPS should derive from independently checkable evidence and operational constraints governing foundation-model outputs, not apparent capability or confidence.

    Source: §7 · p. 27

    Some verified properties cannot be monitored at runtime because they depend on latent states, future behavior, unavailable information, or excessive evaluation cost.

    Source: §4.4 · p. 17

Abstract

from arXiv · show

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.

1 Introduction

Foundation models add powerful capabilities to learning-enabled CPS, but their stochastic behavior and the gaps between model-level performance and system-level requirements make assurance difficult. The paper proposes a system-level assurance stack that uses shared neuro-symbolic artefacts to connect architecture, testing, verification, and runtime assurance.

1 Introduction

  • Stochastic, opaque model behavior and uncertainty across system boundaries make model-level performance insufficient to establish integrated CPS correctness or safe failure.The challenge is to connect model-level properties to system requirements and environmental assumptions.Source: §1 · p. 3
  • The proposed shift is from model-centric evaluation to compositional system assurance built from empirical evidence, formal guarantees, and runtime enforcement.Symbolic world models, specifications, contracts, and interfaces provide shared assurance artefacts around learning-enabled components.Source: §1 · pp. 3–4
  • The Foundation Model Assurance Stack connects assistive foundation-model architectures, empirical testing, and formal verification through cross-cutting neuro-symbolic integration.Testing contributes conformance evidence and counterexamples; verification contributes contracts, abstractions, and constraints.Source: §1 · pp. 3–4, Figure 1 · p. 5
  • A distinct Simplex-style runtime layer combines a learning-enabled controller, monitor, safe controller, and shielding or switching to support operational safety under uncertainty.Pillar 3 develops verified properties and enforcement mechanisms; the runtime layer instantiates them during execution.Source: §1 · p. 4, Figure 1 · p. 5

2 Foundation Models as Assistive Components in CPS Architectures

The architectural pillar treats foundation models as constrained assistants and exposes symbolic representations, interfaces, and contracts for downstream assurance. These shared artefacts connect structured perception and reasoning to testing, verification, and runtime monitoring.

2 Foundation Models as Assistive Components in CPS Architectures

  • The architecture uses foundation models as constrained assistants while exposing symbolic world models, interfaces, and structured reasoning for downstream assurance.These explicit artefacts support testing, verification, and runtime assurance without giving foundation models direct CPS control.Source: §2 · p. 6

2.1 Structured Perception and World Model Construction

  • Symbolic world models represent entities, relations, states, and constraints in machine-interpretable forms that support downstream assurance across the lifecycle.Perception uncertainty, sensor noise, partial observability, and distribution shifts can propagate into these abstractions, so they are not ground truth.Source: §2.1 · pp. 6–7

2.2 Neural–Symbolic Interfaces and Contract Specifications

  • Neural–symbolic interfaces specify exchanged information's semantics, while contracts record operating assumptions and intended output properties for later checking.Foundation models may propose these artefacts, but syntactic, semantic, traceability, and behavioral checks are still required.Source: §2.2 · pp. 7–8

2.3 Symbolic Reasoning, Planning, and Control

  • Symbolic reasoning and hierarchical planning connect structured world models to execution through explicit interfaces where assumptions can be tested, verified, and monitored.Verified foundation-model-assisted planners and scalable assurance across neural–symbolic–physical interfaces remain open research directions.Source: §2.3 · p. 8

3 Testing and Validation of AI-Enabled Systems

The testing pillar seeks system-level conformance evidence rather than isolated model metrics, using structured assurance artefacts and foundation models as constrained assistants. Its outputs include counterexamples, failure modes, and calibrated thresholds that inform verification and runtime assurance.

3 Testing and Validation of AI-Enabled Systems

  • Conformance-driven validation uses architectural artefacts and constrained foundation-model assistance to produce evidence that can refine verification and runtime mechanisms.Testing yields failure modes, counterexamples, violated assumptions, coverage gaps, and empirically calibrated operating thresholds.Source: §3 · p. 9

3.1 Conformance-Based Testing over Structured World Models

  • Symbolic world models let tests evaluate system traces against requirements and explore meaningful entities, relations, events, and environmental conditions.This makes scenario generation an exploration of the semantic state space shared with reasoning and verification.Source: §3.1 · p. 9

3.2 Foundation-Model-Assisted Specification and Test Synthesis

  • Foundation models propose candidate specifications and tests from heterogeneous sources; DSLs and symbolic checks constrain, validate, and trace those artefacts before execution.The workflow iterates through generation, checking, execution, and refinement rather than relying on one-shot outputs.Source: §3.2 · pp. 10–11

3.3 Behavioural Coverage, Failure Modes, and Test Adequacy

  • Behavioral adequacy should cover semantic states, hazards, and assurance boundaries, while failures should be characterized by their context and conditions.This includes regions near contract boundaries, uncertainty limits, safety envelopes, and transitions between nominal and degraded operation.Source: §3.3 · pp. 11–12

3.4 Testing as Assurance Evidence: From Counterexamples to Runtime Thresholds

  • Testing directs empirical exploration toward formal boundary conditions and calibrates runtime thresholds, while counterexamples can refine contracts and abstractions.Calibrated thresholds provide empirical operating evidence, not formal guarantees; runtime monitors and safety constraints are synthesized through verification.Source: §3.4 · p. 12

4 Verification

The verification pillar prioritizes formally tractable system components and composes their guarantees across contracts, interfaces, and transformations. It also uses independently checked synthesis to produce design-time properties and runtime assurance artifacts, while recognizing that some properties cannot be monitored directly during execution.

4.1 Tractable Verification Targets

  • Verification should target safety-critical components and transformations with explicit specifications and independent checks, rather than treating an entire foundation model as the verification target.Candidate targets include symbolic world models, guardrails, contracts, interfaces, representation transformations, formal reasoning components, and generated artifacts.Source: §4.1 · p. 13

4.2 Compositional Verification of Contracts, Interfaces, and Transformations

  • Contracts decompose component guarantees under explicit assumptions, while interface verification must preserve the semantics, uncertainty, and provenance needed by downstream reasoning.This includes structural checks such as schema and type consistency as well as semantic obligations across neural and symbolic components.Source: §4.2 · p. 14
  • Transformation obligations must preserve safety-relevant meaning across representations; conformance testing can expose errors and refine the contracts and properties used in verification.The same obligations arise when requirements, symbolic states, or verified properties are translated for later assurance activities.Source: §4.2 · p. 15

4.3 Foundation-Model-Assisted Verified Synthesis

  • Foundation models can propose specifications, programs, or transformations, but independent checks—not generation—establish correctness and produce checkable evidence.Translation validation checks generated outputs against their sources; accepted artifacts can remain outside the trusted computing base when trustworthy mechanisms validate them.Source: §4.3 · pp. 15–16

4.4 Runtime Monitor and Safety Constraint Synthesis

  • Some properties are not directly monitorable because they depend on latent states, future behavior, unavailable information, or evaluations too costly for CPS timing constraints.A sound executable observation model must preserve the original obligation and correctly expose the relevant symbolic events and uncertainty.Source: §4.4 · p. 17
  • The verification pillar prepares runtime monitors and safety constraints from verified properties; the Simplex layer, rather than synthesis itself, operationalizes them during execution.Monitors observe specified properties, while constraints define conditions for permitted behavior and support shielding or switching to a verified safe controller.Source: §4.4 · pp. 17–18

5 Runtime Assurance through the Simplex Architecture

The Simplex-based Runtime Assurance Layer combines architectural, testing, and verification outputs to condition a learning-enabled controller’s authority during operation. Monitoring, shielding, and switching translate those assurance artifacts into constrained system behavior, with uncertainty informing intervention rather than serving as a safety guarantee.

5 Runtime Assurance through the Simplex Architecture

  • The Runtime Assurance Layer operationalizes architecture, testing, and verification outputs in a Simplex-style loop, allowing high-performance behavior only while supporting assumptions and safety conditions hold.The loop includes a learning-enabled controller, monitor, verified safe controller, and shielding or switching mechanisms.Source: §5 · p. 19

5.1 Simplex-Based Operational Assurance

  • The monitor checks observable states against assurance obligations; shielding can constrain individual actions, while switching transfers control to a verified safe controller when conditions no longer justify continued operation.The safe controller may sacrifice capability and optimality for predictable behavior within a defined operating envelope.Source: §5.1 · pp. 19–20

5.2 Integrating Assurance Artefacts at Runtime

  • Runtime decisions draw on distinct evidence: architecture exposes interpretable state, testing identifies failure regions and calibrates thresholds, and verification supplies properties and constraints.Testing-derived thresholds remain empirical evidence, not formal safety guarantees.Source: §5.2 · pp. 20–21
  • Uncertainty can tighten operating conditions or prompt shielding or switching, while runtime assurance ultimately outputs constrained behavior reaching the physical system.The monitor evaluates verified properties over structured state, using empirical calibration where appropriate to assess proximity to known failure regions.Source: §5.2 · p. 21

6 Research Agenda: From Foundation Models to Certifiable AI Systems

The agenda shifts assurance from verifying foundation models themselves to establishing explicit, machine-checkable boundaries around them and composing evidence across the system lifecycle. It identifies four connected challenges—specification, abstraction fidelity, evidence composition, and lifecycle certification—and proposes advancing according to assurance tractability.

6.1 Challenge 1: From Informal Intent to Executable Assurance Specifications

  • Safety intent is scattered across regulations, engineering requirements, procedures, incident reports, expertise, and implicit expectations, creating a bottleneck for executable assurance specifications.Requirements such as maintaining a safe distance need context, uncertainty, operating modes, and environmental assumptions made explicit.Source: §6.1 · p. 22

6.2 Challenge 2: Closing the Neural–Symbolic–Physical Assurance Gap

  • Neural-to-symbolic and symbolic-to-physical transformations can lose semantic fidelity, so formally correct reasoning may still rely on a world model that misrepresents reality.The agenda calls for interfaces that expose assumptions, uncertainty, provenance, validity regions, and transformation history.Source: §6.2 · p. 23

6.3 Challenge 3: From Component Evidence to Compositional System Assurance

  • Component-level evidence does not automatically establish system safety; contracts and symbolic interfaces must make assumptions and guarantees meaningful across components.The proposed evidence framework preserves evidence dependencies and limitations, enabling affected contracts and evidence to be re-established after updates.Source: §6.3 · p. 24
  • Assurance methods should form a closed loop: contracts identify test obligations, tests reveal counterexamples and assumptions to refine, and runtime evidence checks whether verification assumptions still hold.Foundation models may propose artefacts, but acceptance should rely on an independent oracle whenever correctness is formally expressible.Source: §6.3 · p. 24

6.4 Challenge 4: From Assurance Evidence to Lifecycle Certification and Operational Trust

  • Because models, environments, and data distributions can change after deployment, certification must connect safety claims to supporting evidence and the assumptions that keep it valid.Continuous assurance cases should allow deployment evidence to strengthen, challenge, or invalidate existing claims.Source: §6.4 · pp. 24–25
  • Technical assurance must be translated into evidence for operators and certification authorities, with assurance claims maintained, inspected, and re-established throughout operation.The proposed staged path culminates in certifiable closed-loop autonomy, with runtime monitors and shielding constraining behavior beyond justified safety envelopes.Source: §6.4 · pp. 24–25, §6.5 · p. 26

6.5 A Staged Path toward Certifiable Foundation-Model-Enabled Systems

  • Progress should expand machine-checkable assurance in stages, from checked artefacts and compositional pipelines to protected closed-loop autonomy, without requiring unrestricted foundation-model verification.Near-term work can focus on candidates with explicit correctness oracles; later stages address system assurance and lifecycle evidence.Source: §6.5 · pp. 25–26

7 Conclusion

The paper presents the Foundation Model Assurance Stack as a way to establish explicit assurance boundaries around learning-enabled CPS and connect testing, verification, and runtime assurance. It argues that trust should come from independently checkable evidence and operational constraints, not model capability alone.

7 Conclusion

  • The Foundation Model Assurance Stack connects symbolic world models, neural–symbolic interfaces, contracts, and structured representations to conformance-based testing, compositional verification, and Simplex-based runtime assurance.These shared artefacts establish explicit assurance boundaries around learning-enabled components.Source: §7 · p. 27
  • Foundation models should remain constrained assistants, while testing, verification, and runtime assurance govern their effects on physical systems.Verification establishes properties where correctness can be specified and independently checked; runtime assurance limits authority when assumptions or safety conditions cease to hold.Source: §7 · p. 27
  • Progress toward certifiable AI should expand machine-checkable assurance boundaries; unrestricted foundation-model verification need not be a prerequisite for trustworthy deployment.The agenda is to verify what is tractable, test what must be established empirically, monitor changing conditions, and constrain behavior when evidence no longer justifies authority.Source: §7 · p. 27
Loading 2610.39547v1…