Compositional Verification without Compositional Specification for Learning-Based Systems

Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2017-164
November 26, 2017

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-164.pdf

We consider the problem of performing compositional verification of a system with machine learning components whose behavior cannot easily be formally specified. We present an approach involving a system-level verifier communicating with a component-level analyzer wherein the former identifies a subset of environment behaviors that might lead to a system-level failure while the latter identifies erroneous behaviors, such as misclassifications, of the machine learning component that might be extended to a system-level counterexample. Results on cyber-physical systems with deep learning components used for perception demonstrate the promise of this approach.


BibTeX citation:

@techreport{Seshia:EECS-2017-164,
    Author = {Seshia, Sanjit A.},
    Title = {Compositional Verification without Compositional Specification for Learning-Based Systems},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2017},
    Month = {Nov},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-164.html},
    Number = {UCB/EECS-2017-164},
    Abstract = {We consider the problem of performing compositional verification
of a system with machine learning components whose behavior
cannot easily be formally specified. 
We present an approach involving a system-level verifier
communicating with a component-level analyzer wherein 
the former identifies a subset of environment behaviors
that might lead to a system-level failure while the latter
identifies erroneous behaviors, such as misclassifications,
of the machine learning component that might be extended
to a system-level counterexample.
Results on cyber-physical systems with deep learning
components used for perception demonstrate the promise of
this approach.}
}

EndNote citation:

%0 Report
%A Seshia, Sanjit A.
%T Compositional Verification without Compositional Specification for Learning-Based Systems
%I EECS Department, University of California, Berkeley
%D 2017
%8 November 26
%@ UCB/EECS-2017-164
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-164.html
%F Seshia:EECS-2017-164