Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks

Xuankang Lin, He Zhu, Roopsha Samanta, Suresh Jagannathan

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

15 Scopus citations

Abstract

Artificial Neural Networks (ANNs) have demonstrated remarkable utility in various challenging machine learning applications. While formally verified properties of their behaviors are highly desired, they have proven notoriously difficult to derive and enforce. Existing approaches typically formulate this problem as a post facto analysis process. In this paper, we present a novel learning framework that ensures such formal guarantees are enforced by construction. Our technique enables training provably correct networks with respect to a broad class of safety properties, a capability that goes well-beyond existing approaches, without compromising much accuracy. Our key insight is that we can integrate an optimization-based abstraction refinement loop into the learning process and operate over dynamically constructed partitions of the input space that considers accuracy and safety objectives synergistically. The refinement procedure iteratively splits the input space from which training data is drawn, guided by the efficacy with which such partitions enable safety verification. We have implemented our approach in a tool (ART) and applied it to enforce general safety properties on unmanned aviator collision avoidance system ACAS Xu dataset and the Collision Detection dataset. Importantly, we empirically demonstrate that realizing safety does not come at the price of much accuracy. Our methodology demonstrates that an abstraction refinement methodology provides a meaningful pathway for building both accurate and correct machine learning networks.

Original languageEnglish (US)
Title of host publicationProceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
EditorsAlexander Ivrii, Ofer Strichman, Warren A. Hunt, Georg Weissenbacher
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages148-157
Number of pages10
ISBN (Electronic)9783854480426
DOIs
StatePublished - Sep 21 2020
Event20th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2020 - Virtual, Haifa, Israel
Duration: Sep 21 2020Sep 24 2020

Publication series

NameProceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020

Conference

Conference20th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
Country/TerritoryIsrael
CityVirtual, Haifa
Period9/21/209/24/20

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Graphics and Computer-Aided Design
  • Software
  • Safety, Risk, Reliability and Quality
  • Modeling and Simulation

Fingerprint

Dive into the research topics of 'Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks'. Together they form a unique fingerprint.

Cite this