CAREER: From Neural Network Verification to General SMT Solving: A New Framework for Solving SMT over Non-linear Real Arithmetic

Satisfiability Modulo Theories (SMT) problems are akin to mathematical puzzles: given a mix of equations and logical rules, an SMT solver determines whether there exists an assignment of variables that satisfies everything at once. SMT solving underpins high-stakes assurance tasks: for example, proving that a self-driving car cannot steer into an obstacle under modeled operating conditions, and supporting safety checks in domains like avionics, medical devices, and power systems. These problems become increasingly challenging as modern software and systems incorporate machine learning (ML) and artificial intelligence (AI), which introduce large, highly nonlinear mathematical constraints that often exceed the scalability of traditional solvers. To address this gap, the project develops a new solver framework that transfers highly scalable, hardware-accelerated techniques originally created for neural-network verification into general SMT solving. The project’s novelties are the fundamental re-architecting of traditional SMT solving procedures around a new concept called linear bound propagation, which effectively handles large SMT problems with nonlinear arithmetic and enables massive parallel computation. The project's impacts are an open-source, high-performance reasoning engine that strengthens safety and reliability across software and cyber-physical domains where nonlinear constraints and rigorous safety requirements are central, including next-generation AI-enabled systems, thereby fostering public trust in autonomous technologies. Technically, the project advances formal verification for nonlinear real arithmetic (NRA) SMT through three synergistic thrusts. Thrust I builds a new NRA decision procedure grounded in linear bound propagation, introducing novel methods to efficiently account for correlations among constraints, infer bounds even when variables are only implicitly constrained, and tighten relaxations through computation-graph optimizations and cross-constraint bound refinement. Thrust II elevates this procedure into a delta-complete solver by specializing branch-and-bound for NRA and integrating the resulting engine into a DPLL(T) architecture with linear-bound-aware propagation, clause learning, and unsatisfiable core extraction. Thrust III delivers a practical, high-performance implementation via an asynchronous DPLL(T) pipeline that keeps parallel numerical evaluation highly utilized. The approach is validated on previously intractable verification workloads (including those with AI/ML components) while contributing new community benchmarks, accelerating progress in building toolchains for formally verified systems that integrate code, physics, and AI models. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2543005 | Program: 01002930DB NSF RESEARCH & RELATED ACTIVIT,01003031DB NSF RESEARCH & RELATED ACTIVIT,01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Huan Zhang | Institution: University of Illinois at Urbana-Champaign, URBANA, IL | Award Amount: $368,343 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2543005 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2543005.html