Verifying feedforward neural networks for classification in Isabelle/HOL

DOI10.1007/978-3-031-27481-7_24MaRDI QIDQ6174545zbMATH OpenFDO

Authors Achim D. Brucker, Amy Stell

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-27481-7_24

zbMATH Keywords

classification networkdeep learningfeedforward networkIsabelle/HOLneural networkverification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Artificial neural networks and deep learning (68T07) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formal verification of piece-wise linear feed-forward neural networks
• Safety verification of deep neural networks
• Formal specification for deep neural networks
• Reluplex: a calculus for reasoning about deep neural networks
• Exploiting verified neural networks via floating point numerical error

Cites work

• Building Formal Method Tools in the Isabelle/Isar Framework
• Eisbach: a proof method language for Isabelle
• Formal specification for deep neural networks
• Formal verification of piece-wise linear feed-forward neural networks
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Learning representations by back-propagating errors
• Neural networks and deep learning. A textbook
• Operating system verification---an overview
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Safety verification of deep neural networks

Cited in

(5)

• Proving properties of binary classification neural networks via Łukasiewicz logic
• Modelling and verifying robotic software that uses neural networks
• Taming differentiable logics with Coq formalisation
• (Extended) Interval Analysis
• Formalizing Neural Networks

This page was built for publication: Verifying feedforward neural networks for classification in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174545)