Neural networks, secure by construction : an exploration of refinement types

Kokke, Wen and Komendantskaya, Ekaterina and Kienitz, Daniel and Atkey, Bob and Aspinall, David (2020) Neural networks, secure by construction : an exploration of refinement types. In: The 18th Asian Symposium on Programming Languages and Systems, 2020-11-29 - 2020-12-03, Online. (https://doi.org/10.1007/978-3-030-64437-6_4)

[thumbnail of Kokke-etal-ASPLAS-2020-Neural-networks-secure-by-construction]
Preview
 Text. Filename: Kokke_etal_ASPLAS_2020_Neural_networks_secure_by_construction.pdf
Accepted Author Manuscript
Download (577kB)| Preview

Abstract

We present StarChild and Lazuli, two libraries which leverage refinement types to verify neural networks, implemented in F∗ and Liquid Haskell. Refinement types are types augmented, or refined, with assertions about values of that type, e.g., "integers greater than five", which are checked by an SMT solver. Crucially, these assertions are written in the language itself. A user of our library can refine the type of neural networks, e.g., "neural networks which are robust against adversarial attacks", and expect F∗ to handle the verification of this claim for any specific network, without having to change the representation of the network, or even having to learn about SMT solvers. Our initial experiments indicate that our approach could greatly reduce the burden of verifying neural networks. Unfortunately, they also show that SMT solvers do not scale to the sizes required for neural network verification.

ORCID iDs

Kokke, Wen, Komendantskaya, Ekaterina, Kienitz, Daniel, Atkey, Bob ORCID logoORCID: https://orcid.org/0000-0002-4414-5047 and Aspinall, David;
CORE (COnnecting REpositories)