{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/129304"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/129304","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Neural network based method for solving SMT problems","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_has_math":false,"creators":["Lu, Keyu"],"institution":"University of Illinois Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Zhang, Huan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-05-05","date_published":"2025-05-05","updated_at":"2026-07-22T22:25:04Z","subjects":["neural network verification","SMT solving"],"languages":["en","eng"],"rights":["Copyright 2025 Keyu Lu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/129304","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Zhang, Huan"]},{"key":"dc:creator","label":"Author","values":["Lu, Keyu"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2025-05-05","2025-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["neural network verification","SMT solving"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2025 Keyu Lu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/129304"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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","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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Neural network based method for solving SMT problems"]}]}],"canonical_facts":{"dc:contributor":["Zhang, Huan"],"dc:creator":["Lu, Keyu"],"dc:date":["2025-05-05","2025-05"],"dc:description":["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","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."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/129304"],"dc:language":["en","eng"],"dc:rights":["Copyright 2025 Keyu Lu"],"dc:subject":["neural network verification","SMT solving"],"dc:title":["Neural network based method for solving SMT problems"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:04Z"}