Reluplex: a calculus for reasoning about deep neural networks

DOI10.1007/s10703-021-00363-7zbMath1522.68328OpenAlexW3190946860MaRDI QIDQ6108442

Guy Katz, Kyle D. Julian, Clark Barrett, David L. Dill, Mykel J. Kochenderfer

Publication date: 29 June 2023

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-021-00363-7

zbMATH Keywords

verificationsatisfiability modulo theoriesdeep neural networks

Mathematics Subject Classification ID

Artificial neural networks and deep learning (68T07) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

Reachability in Simple Neural Networks ⋮ Reachability is NP-complete even for the simplest neural networks

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear programming: foundations and extensions
• Reluplex: an efficient SMT solver for verifying deep neural networks
• An abstraction-based framework for neural network verification
• Challenging SMT solvers to verify neural networks
• A Branch-and-Cut Algorithm for the Resolution of Large-Scale Symmetric Traveling Salesman Problems
• Solving SAT and SAT Modulo Theories
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
• GRASP: a search algorithm for propositional satisfiability
• Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
• Formal verification of neural network controlled autonomous systems
• Reachability analysis for neural feedback systems using regressive polynomial rule inference
• Verisig
• Splitting on Demand in SAT Modulo Theories
• DeepSafe: a data-driven approach for assessing robustness of neural networks

This page was built for publication: Reluplex: a calculus for reasoning about deep neural networks