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

> **NSF 01002930DB NSF RESEARCH & RELATED ACTIVIT** · University of Illinois at Urbana-Champaign (IL) · $597,023

## Abstract

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 cro

## Key facts

- **NSF award ID:** 2543005
- **Awardee organization:** University of Illinois at Urbana-Champaign (IL)
- **SAM.gov UEI:** Y8CWNJRCNN91
- **PI:** Huan Zhang
- **Primary program:** 01002930DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Artificial Intelligence (AI), CAREER-Faculty Erly Career Dev, PROGRAMMING LANGUAGES
- **Estimated total:** $597,023
- **Funds obligated:** $368,343
- **Transaction type:** Continuing Grant
- **Period:** 08/01/2026 → 07/31/2031

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2543005

## Citation

> US National Science Foundation, Award 2543005, CAREER: From Neural Network Verification to General SMT Solving: A New Framework for Solving SMT over Non-linear Real Arithmetic. Retrieved via AI Analytics 2026-07-19 from https://api.ai-analytics.org/grant/nsf/2543005. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*