Heterogeneous AI Systems Cannot Be Verified End-to-End for Trustworthiness Because Trust Frameworks Are Fragmented Across Communities

Real-world AI systems are not monolithic neural networks — they are assemblages of heterogeneous components: machine learning models for perception, symbolic reasoning engines for planning, optimization solvers for resource allocation, rule-based systems for safety constraints, and human-in-the-loop interfaces for oversight. Each component type has its own community with its own verification methods, trust definitions, and correctness criteria. But there is no methodology for composing component-level trust into system-level trustworthiness. A Dagstuhl seminar bringing together researchers from AI, machine learning, robotics, formal verification, software engineering, and philosophy found that the notion of trust in AI systems is "fragmented and bespoke for the individual communities." Fairness, accountability, and transparency (FAT) principles exist as high-level position papers and manifestos but lack formal, compositional verification methods that can demonstrate these properties hold for an integrated system — not just for each piece in isolation.

Governments, industry, and international bodies (EU AI Act, NIST AI Risk Management Framework, DARPA XAI) are demanding trustworthy AI, but the demand outpaces the technical ability to deliver it. When an autonomous vehicle misclassifies a pedestrian, the failure may originate in the ML perception model, the symbolic planner's decision logic, the sensor fusion algorithm, or the interaction between them — and current verification approaches cannot trace trust through these component boundaries. The EU AI Act will require conformity assessments for high-risk AI systems, but no conformity assessment methodology exists for systems that combine learning-based and logic-based components. The consequence is that deployed AI systems carry trust claims that rest on verifying components individually — ignoring the emergent behavior that arises from their interaction.

Formal verification (model checking, theorem proving) provides strong guarantees for logic-based software but cannot handle the statistical, approximate nature of ML components. ML evaluation (test accuracy, robustness benchmarks, interpretability techniques) provides probabilistic performance estimates but not formal guarantees. DARPA's Explainable AI (XAI) program produced methods for explaining individual model decisions but not for verifying that explanations are faithful to the actual reasoning process, and explanations of individual components don't compose into system-level explanations. The software engineering community has developed safety cases and assurance arguments (GSN notation) that can structure trust claims across components, but these arguments rely on evidence that the individual communities generate using incompatible methods. Causal reasoning — necessary for attributing responsibility when things go wrong — requires counterfactual analysis that current ML systems cannot reliably perform, because they capture correlations, not causal mechanisms. The result is that each community can make trustworthiness claims about its own components, but no one can make trustworthiness claims about the system.

A compositional verification framework where component-level properties (proved, tested, or argued) can be formally composed into system-level trustworthiness claims with explicit assumptions about component interactions. This requires: shared formal languages for expressing trust requirements across ML and symbolic components; methods for interface verification (proving that the output guarantees of one component satisfy the input assumptions of the next); causal reasoning tools that can attribute system-level failures to specific component interactions; and lifecycle integration that maintains trust arguments as components are updated or retrained. The seminar proposed a "Trustworthiness & Responsibility in AI" framework integrating quantifiable responsibility and verifiable correctness into all stages of the software engineering process — but acknowledged this is a research vision, not a current capability.

A team could build a small heterogeneous autonomous system (e.g., a robot that uses an ML vision model for perception, a symbolic planner for navigation, and a rule-based safety controller) and attempt to construct a formal trust argument spanning all three components. The exercise would reveal exactly where current trust methods break down at component boundaries. The deliverable would be a documented "trust gap analysis" identifying which properties can be verified, which can only be tested, and which cannot currently be assured at all. This is a feasible software engineering / formal methods project. Skills needed: familiarity with at least two of ML, formal methods, and software architecture.