-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
242 lines (202 loc) · 16.9 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Description" content="">
<meta name="Keywords" content="">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/pure/0.6.0/pure-min.css">
<link rel="stylesheet" type="text/css" href="style.css" />
<title>Verified AI</title>
</head>
<body>
<div class="pure-menu" id="menu">
<a id="home-link" href="#" class="pure-menu-heading pure-menu-link">
Home</a>
<ul class="pure-menu-list">
<li class="pure-menu-item">
<a href="#about" class="pure-menu-link">About</a></li>
<li class="pure-menu-item">
<a href="#research" class="pure-menu-link">Research</a>
</li>
<li class="pure-menu-item">
<a href="#talks" class="pure-menu-link">Talks</a>
</li>
<li class="pure-menu-item">
<a href="#tools" class="pure-menu-link">Tools</a>
</li>
<li class="pure-menu-item">
<a href="#examples" class="pure-menu-link">Case Studies</a>
</li>
<li class="pure-menu-item">
<a href="#contact" class="pure-menu-link">Contact</a>
</li>
<li class="pure-menu-item">
<a href="#sponsors" class="pure-menu-link">Sponsors</a>
</li>
</ul>
</div>
<div class="header">
<h1>Verified AI</h1>
</div>
<section class="content">
<section id="about">
<h2>About</h2>
<p>
<i>Verified Artificial Intelligence (AI)</i> is the goal of designing AI-based systems
that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements.
Our paper <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-arxiv16.html">Towards Verified Artificial Intelligence</a>,
first published in 2016, presents our view of the
challenges for applying formal methods to improve assurance in AI-based systems, identifying five major categories:
<i>environment modeling</i>, <i>formal specification</i>, <i>modeling learning systems</i>,
<i>scalable computational engines</i>, and <i>correct-by-construction design methods</i>. The paper also proposes
principles for tackling these challenges.
<p> In this website, we describe our ongoing progress towards the goal of Verified AI,
providing links to publications, tools, and industrial case studies. Our work is being applied to
the use of AI in several domains, including autonomous driving, aircraft and aerospace systems,
and robotics including human-robot systems.
The paper cited above provides more details on our perspective of the field, including links to
the work by other groups.
</p>
</section>
<section id="research">
<h2>Research</h2>
We briefly describe the main challenges along with some of the research we have been doing to address them.
For a more detailed description of the challenges and principles for Verified AI, please consult <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-arxiv16.html">our paper</a>.
<h3>Environment Modeling</h3>
The environment of AI-based systems can be extremely complex --- indeed, the use of AI and Machine Learning (ML) is often introduced to deal with this complexity. Some key challenges are: finding the right model fidelity, modeling human behavior, and dealing with the "unknown variables" problem, where we do not know all the agents and objects in the environment, let alone have models of their behaviors. Here are the principles we are applying to address these challenges:
<ul>
<li><i>Probabilistic Modeling</i>: We have designed Scenic, a probabilistic programming language for modeling environments of systems with AI-based autonomy. <br>
See <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-fremont-pldi19.html">Scenic: A Language for Scenario Specification and Scene Generation</a>, Fremont et al., PLDI 2019.<br>
For a more detailed description of Scenic including its features for dynamic scenario modeling, see the <a href="https://arxiv.org/abs/2010.06580">extended version of the paper</a>.
</li>
<li><i>Active Data-Driven Model Inference</i>: We are developing techniques for learning models of human behavior from data gathered actively. <br>
See <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-sadigh-iros16.html">Information Gathering Actions Over Human Internal State</a>, Sadigh et al., IROS 2016.
</li>
<li><i>Introspective Environment Modeling</i>: To deal with the "unknown variables" problem, we propose the use of algorithmic methods to extract assumptions on the environment, monitorable by reliable sensors, under which safe and correct operation can be guaranteed.<br>
See <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-rv19.html">Introspective Environment Modeling</a>, Seshia, RV 2019.
</li>
</ul>
<h3>Formal Specification</h3>
This crucial aspect of formal methods faces multiple challenges, including "hard-to-formalize" tasks such as perception, combining quantitative and Boolean
specification formalisms, and bridging the gap between data and logic-based specifications. Here are some of the ways we
are addressing these:
<ul>
<li><i>Specification for ML</i>: This paper surveys the various types of properties of interest for ML models/systems, especially for deep neural networks: <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html">Formal Specification for Deep Neural Networks</a>, Seshia et al., ATVA 2018.
</li>
<li><i>Start at the System Level</i>: We are developing methods that start with specifications at the system level, i.e., for the entire AI/ML-based system, and then derive component-level properties from those, an approach particularly relevant for hard-to-formalize tasks. <br>
See <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-dreossi-jar19.html">Compositional Falsification of Cyber-Physical Systems with Machine Learning Components</a>, Dreossi et al., JAR 2019 (first version in NFM 2017).
</li>
<li><i>Hybrid Quantitative-Boolean Specifications</i>: Here is a paper formalizing the various flavors of "robustness" that people have considered in the literature, especially on Adversarial ML, giving a unifying quantitative-Boolean formulation of robustness:<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-dreossi-vnn19.html">A Formalization of Robustness for Deep Neural Networks</a>, Dreossi et al., VNN 2019.
</li>
<li><i>Specification Mining</i>: We believe the paradigm of learning formal (logic/automata-based) specifications from data is a promising approach to bridge the gap with how tasks are specified in ML using data. Here are some papers exploring this approach:<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-vazquez-neurips18.html">Learning Task Specifications from Demonstrations</a>, Vazquez-Chanlatte et al, NeurIPS 2018.<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-vazquez-cav17.html">Logical Clustering and Learning for Time-Series Data</a>, Vazquez-Chanlatte et al, CAV 2017.<br>
</li>
</ul>
<h3>Modeling Learning Systems</h3>
The high-dimensionality of input and state spaces for AI-based systems, illustrated, e.g., by deep neural networks used for perception,
require new approaches for abstraction and modeling of learning systems. Here are some representative results addressing this need:
<ul>
<li><i>Semantic Feature Spaces</i>: Modeling the underlying semantic context in which an AI/ML system operates can be crucial to scale up analysis and also provide more meaningful results. <br>
See <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-dreossi-cav18.html">Semantic Adversarial Deep Learning</a>, Dreossi et al, CAV 2018.
</li>
<li><i>Abstractions for ML Models</i>: Even simple abstractions of ML models can help a great deal, as shown in this paper: <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-dreossi-jar19.html">Compositional Falsification of Cyber-Physical Systems with Machine Learning Components</a>, Dreossi et al., JAR 2019 (first version in NFM 2017).
</li>
<li><i>Generating Interpretations/Explanations for ML Models</i>: Complex ML models such as deep neural networks become more amenable to formal analysis when they can be lifted to more interpretable/explainable representations. Here is a representative publication on this topic: <br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-kim-cvpr20.html">A Programmatic and Semantic Approach to Explaining and Debugging Neural Network Based Object Detectors</a>, Kim et al, CVPR 2020.
</li>
</ul>
<h3>Scalable Computational Engines</h3>
Several advances are needed in creating computational engines for efficient and scalable training, testing,
design, and verification of AI-based systems. Here are some results along this direction:
<ul>
<li><i>Compositional Analysis</i>: A modular approach is central to scaling up formal methods to large systems.
We are developing compositional methods for AI-based systems, even in the case where components (such as
perception) do not themselves have precise, formal specifications. See this sample paper:
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-dreossi-jar19.html">Compositional Falsification of Cyber-Physical Systems with Machine Learning Components</a>, Dreossi et al., JAR 2019 (NFM 2017).
</li>
<li><i>Quantitative Semantic Analysis</i>: We are leveraging optimization-driven methods to search in an efficient goal-directed manner over semantic feature spaces, see sample papers: <br>
<a href="https://arxiv.org/abs/1910.00727">Analyzing and Improving Neural Networks by Generating Semantic Counterexamples through Differentiable Rendering</a>, Jain et al., 2020.<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-verifai-cav19.html">VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems</a>, Dreossi et al., CAV 2019.
</li>
<li><i>Data Set Design</i>: We are developing methods for efficiently generating data satisfying hard, soft, and distributional constraints, based on the theory of algorithmic (controlled) improvisation, implemented in the back end of the Scenic programming system:<br>
See <a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-fremont-pldi19.html">Scenic: A Language for Scenario Specification and Scene Generation</a>, Fremont et al., PLDI 2019.
</li>
</ul>
<h3>Correct-by-Construction Design</h3>
The techniques described in the above thrusts must be augmented by methods to design correct and robust AI/ML-based systems.
Here is some of our work on such methods:
<ul>
<li><i>Formal Inductive Synthesis</i>: Learning systems can be coupled with oracles (such as verifiers) that provide formal guarantees on the learned models or produce counterexamples and other data that they can be improved with. This leads us to develop a theory of <i>oracle-guided inductive synthesis</i> described and applied in the papers listed below: <br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-jha-acta17.html">A Theory of Formal Synthesis via Inductive Learning</a>, Jha and Seshia, Acta Informatica, 2017.<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-dreossi-ijcai18.html">Counterexample-Guided Data Augmentation</a>, Dreossi et al., IJCAI 2018.
</li>
<li><i>Run-time Assurance Systems</i>: Techniques for run-time assurance compose a component that might be unverified
or only verified to operate safety under certain conditions with a fall-back component that can take over
when necessary to provide a minimal assurance of safe operation at all times, along with associated switching logic.
In this regard, we have developed a runtime assurance system called SOTER, described in the following papers:<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-desai-dsn19.html">SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems</a>, Desai et al., DSN 2019.<br>
<a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-shivakumar-rv20.html">SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System</a>, Shivakumar et al., RV 2020.
</li>
</ul>
</section>
<section id="talks">
<h2>Selected Talks</h2>
<ul>
<li><a href="http://www.eecs.berkeley.edu/~sseshia/talks/Seshia-VerifiedAI_NFM20.pdf">Verified Artificial Intelligence and Autonomy (PDF)</a>, Sanjit A. Seshia, Keynote Talk at the NASA Formal Methods Conference (NFM), May 2020. (<a href="https://youtu.be/_qszqXlKADw?t=12274">watch the video on youtube</a>) </li>
<li><a href="http://www.eecs.berkeley.edu/~sseshia/talks/Seshia-VerifiedAI_RV19.pdf">Verified Artificial Intelligence: A Runtime Verification Perspective (PDF)</a>, Sanjit A. Seshia, Keynote Talk at the International Conference on Runtime Verification (RV), October 2019. (<a href="https://www.youtube.com/watch?v=QF210fIhkuo">watch the video on youtube</a>)</li>
<li><a href="https://simons.berkeley.edu/talks/towards-verified-deep-learning">Towards Verified Deep Learning (video)</a>, Sanjit A. Seshia, Invited Talk at Simons Institute Workshop on Emerging Challenges in Deep Learning, August 2019.</li>
<li><a href="https://www.youtube.com/watch?v=D_Cze9y_Ips">Scenic and VerifAI: Tools for Assured AI-Based Autonomy (video)</a>, Sanjit A. Seshia, Edward Kim, Daniel J. Fremont, and Atul Acharya, Webinar, August 2020.
(<a href="doc/VerifAI_Scenic_Webinar_Aug2020_Overview.pdf">Overview Slides</a> and <a href="doc/VerifAI_Scenic_Webinar_Aug2020_Tutorial.pdf">Tutorial Slides</a>, both in PDF)
</li>
</ul>
</section>
<section id="tools">
<h2>Tools</h2>
Our research is mainly implemented in two open-source tools, VerifAI and Scenic:
<ul>
<li>
<b>VerifAI</b>: A software toolkit for the formal design and
analysis of systems that include artificial intelligence
(AI) and machine learning (ML) components.
(for code and more details, follow this <a href="https://github.com/BerkeleyLearnVerify/VerifAI"/>link</a>)
</li>
<li>
<b>Scenic</b>: A compiler and scene generator for the Scenic probabilistic
scenario description language, with interfaces to several
simulators (in domains spanning autonomous driving, robotics, aircraft).
(for code and more details, follow this <a href="https://github.com/BerkeleyLearnVerify/Scenic"/>link</a>)
</li>
</ul>
VerifAI and Scenic are designed to be used in tandem: Scenic is a modeling language for the
back-end algorithms implemented in VerifAI.
</section>
<section id="examples">
<h2>Industrial Case Studies</h2>
Scenic and VerifAI have been used in industrial case studies, here are two documented instances involving collaborations with industrial partners:
<ul>
<li><a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-fremont-cav20.html"><i>Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI</i></a>,
Fremont, Chiu, Margineantu, Osipychev, and Seshia, CAV 2020.
</li>
<li><a href="https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-fremont-itsc20.html"><i>Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World</i></a>,
Fremont, Kim, Pant, Seshia, Acharya, Bruso, Wells, Lemke, Lu, and Mehta, ITSC 2020.
[See also <a href="https://gomentumstation.net/wp-content/uploads/2020/03/AAA-UCB-LG-AV-Testing-Project-Whitepaper-Final-2020-7-15.pdf">accompanying white paper</a> and <a href="https://gomentumstation.net/blog-2020-03-26/">associated blog post</a>.]
</li>
<ul>
</section>
<section id="contact">
<h2>Contact</h2>
For further information on the Verified AI effort, please contact <a href="https://people.eecs.berkeley.edu/~sseshia">Professor Sanjit Seshia</a> and his research group.
</section>
<section id="sponsors">
<h2>Sponsors</h2>
We gratefully acknowledge our funding sponsors: the National Science Foundation (NSF) under projects
such as <a href="http://vehical.org">VeHICaL</a>,
the Defense Advanced Research Projects Agency (DARPA), and industrial sponsors providing
support to centers such as the Industrial Cyber-Physical Systems (iCyPhy) Center and
Berkeley Deep Drive.
</section>
</section>
</body>
</html>