Neural network based method for solving SMT problems

Lu, Keyu

Permalink

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

Description

Title

Neural network based method for solving SMT problems

Author(s)

Lu, Keyu

Issue Date

2025-05-05

Director of Research (if dissertation) or Advisor (if thesis)

Zhang, Huan

Department of Study

Electrical & Computer Eng

Discipline

Electrical & Computer Engr

Degree Granting Institution

University of Illinois Urbana-Champaign

Degree Name

M.S.

Degree Level

Thesis

Keyword(s)

• neural network verification
• SMT solving

Abstract

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.

Graduation Semester

2025-05

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2025 Keyu Lu

Owning Collections