Neural Networks, Secure by Construction: An Exploration of Refinement Types

Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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,“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,“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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems. APLAS 2020
EditorsBruno C. Oliveira
PublisherSpringer
Pages67-85
Number of pages19
ISBN (Electronic)9783030644376
ISBN (Print)9783030644369
DOIs
Publication statusPublished - 24 Nov 2020
Event18th Asian Symposium on Programming Languages and Systems 2020 - Fukuoka, Japan
Duration: 30 Nov 20202 Dec 2020

Publication series

NameLecture Notes in Computer Science
Volume12470
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th Asian Symposium on Programming Languages and Systems 2020
Abbreviated titleAPLAS 2020
CountryJapan
CityFukuoka
Period30/11/202/12/20

Keywords

  • Neural networks
  • Refinement types
  • Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Neural Networks, Secure by Construction: An Exploration of Refinement Types'. Together they form a unique fingerprint.

Cite this