No Proof for the Neural Network Inside

Safety-critical systems increasingly embed machine learning components — neural network perception in autonomous vehicles, ML-based anomaly detection in medical devices, learned control policies in robotic surgery. Traditional formal verification can prove that deterministic software meets its specification, but these methods assume that system behavior can be fully characterized by logical rules. ML components violate this assumption fundamentally: they are statistical approximations whose behavior is defined by billions of learned parameters rather than explicit logic, they can produce different outputs for imperceptibly different inputs (adversarial vulnerability), and their decision boundaries cannot be enumerated or inspected. No verification methodology can currently provide end-to-end safety guarantees for systems that include both formally specified software and learned ML components.

The FAA requires software certification (DO-178C) for all avionics systems, and automotive safety standards (ISO 26262) require hazard analysis through the full development lifecycle. As ML becomes essential for perception, prediction, and decision-making in these safety-critical domains, the inability to formally verify ML components creates a regulatory bottleneck: manufacturers cannot certify systems they cannot verify, and regulators cannot approve systems without certification. The US Department of Defense's push for autonomous systems, FDA's evolving framework for AI-enabled medical devices, and NHTSA's approach to autonomous vehicle approval all depend on solving this verification gap.

Robustness verification tools (e.g., CROWN, alpha-beta-CROWN) can verify that a neural network's output doesn't change within an epsilon-ball around a given input, but this local robustness says nothing about global safety properties and is computationally intractable for large networks (verification time scales exponentially with network depth). Abstract interpretation techniques can over-approximate neural network behavior but produce bounds so loose that meaningful safety properties cannot be proved. Testing-based validation (millions of simulated miles, metamorphic testing) provides statistical confidence but not formal guarantees — an important distinction when human lives are at stake. Runtime monitoring (simplex architecture, runtime assurance) can override unsafe ML outputs with verified fallback controllers, but this approach degrades system performance and doesn't verify the ML component itself. Neurosymbolic approaches that combine neural perception with symbolic reasoning are promising but lack mature verification theories for the interface between learned and symbolic representations.

New formal frameworks that can express and verify probabilistic safety specifications (e.g., "collision probability < 10^-9 per hour") rather than binary correctness, bridging the gap between deterministic formal methods and stochastic ML behavior. Compositional verification approaches that verify the ML component's contract (input-output specification) independently of the system, then verify the system against that contract — if the contract formalism is rich enough to capture ML behavior. Advances in interpretable or inherently verifiable ML architectures that constrain learned representations to be amenable to formal analysis without sacrificing performance.

A student team could implement a runtime assurance framework (simplex architecture) for a small ML-controlled system (e.g., an RL-controlled drone in simulation), comparing system performance with and without the verified safety monitor and measuring how often the monitor intervenes. Alternatively, a team could benchmark existing neural network verification tools (CROWN, Marabou, NNV) on a realistic perception pipeline, documenting the gap between what can be verified and what safety certification requires. Relevant disciplines include computer science (formal methods, ML), systems engineering, and aerospace/automotive engineering.