Neural network based method for solving SMT problems

Satisfiability Modulo Theories (SMT) over nonlinear real arithmetic (NRA) represents a fundamental yet notoriously difficult problem class in formal verification and symbolic reasoning. Traditional SMT solvers struggle with the scalability and decidability of QF_NRA problems due to their intrinsic nonlinearity. In this work, we propose a novel reduction-based framework that translates SMT problems defined in the SMT-LIB2 format into equivalent neural network verification problems specified in the VNN-LIB format. By constructing tailored neural networks that capture the semantics of the original constraints, we leverage powerful neural network verifiers—specifically, the α,β-CROWN solver—to determine the satisfiability of the original NRA formulas. This transformation enables the application of recent advances in neural network verification to a broader class of symbolic problems. Our approach bridges the gap between symbolic logic reasoning and neural verification, potentially unlocking new paths for scalable and parallelizable SMT solving. We demonstrate the soundness and feasibility of the method through illustrative case studies and analyze its performance in terms of accuracy and approximation fidelity.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Electrical & Computer Engr

Grantor

University of Illinois Urbana-Champaign

Year dc:date

2025

Author dc:creator

• Lu, Keyu

Contributors dc:contributor

• Zhang, Huan

• neural network verification
• SMT solving

Statement dc:rights

• Copyright 2025 Keyu Lu

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/129304

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F129304