2026-09-20T23:55:52Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/129304 2025-10-20 col_2142_5131 col_2142_8888 com_2142_5130 com_2142_8887 com_2142_234

application/pdf en text Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms The student, Keyu Lu, accepted the attached license on 2025-05-01 at 20:25. The student, Keyu Lu, submitted this Thesis for approval on 2025-05-01 at 20:39. This Thesis was approved for publication on 2025-05-05 at 12:28. DSpace SAF Submission Ingestion Package generated from Vireo submission #22166 on 2025-10-19 at 18:11:31 Neural network based method for solving SMT problems Lu, Keyu 2025-05-05 Zhang, Huan neural network verification SMT solving eng 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. 2025-05 Thesis https://hdl.handle.net/2142/129304 Copyright 2025 Keyu Lu Electrical & Computer Eng Electrical & Computer Engr University of Illinois Urbana-Champaign M.S. Thesis