Perception Contracts for Safety of ML-Enabled Systems

被引：6

作者：

Astorga, Angello ^{[1
]}

Hsieh, Chiao ^{[1
]}

Madhusudan, P. ^{[1
]}

Mitra, Sayan ^{[1
]}

机构：

[1] Univ Illinois, Champaign, IL 61820 USA

来源：

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2023年 / 7卷 / OOPSLA期

基金：

美国食品与农业研究所;

关键词：

perception contracts; safety; neural perception;

D O I：

10.1145/3622875

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We introduce a novel notion of perception contracts to reason about the safety of controllers that interact with an environment using neural perception. Perception contracts capture errors in ground-truth estimations that preserve invariants when systems act upon them. We develop a theory of perception contracts and design symbolic learning algorithms for synthesizing them from a finite set of images. We implement our algorithms and evaluate synthesized perception contracts for two realistic vision-based control systems, a lane tracking system for an electric vehicle and an agricultural robot that follows crop rows. Our evaluation shows that our approach is effective in synthesizing perception contracts and generalizes well when evaluated over test images obtained during runtime monitoring of the systems.

引用

页数：28

共 44 条

[21]

Gibson John E, 1961, Stability of nonlinear control systems by the second method of Liapunov

[22]

Hoffmann GM, 2007, P AMER CONTR CONF, P3910

[23] Verifying Controllers With Vision-Based Perception Using Safe Approximate Abstractions [J].

Hsieh, Chiao ;

Li, Yangge ;

Sun, Dawei ;

Joshi, Keyur ;

Misailovic, Sasa ;

Mitra, Sayan .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2022, 41 (11) :4205-4216

[24]

Hsieh C, 2023, Arxiv, DOI [arXiv:2210.00982, 10.48550/ARXIV.2210.00982, DOI 10.48550/ARXIV.2210.00982]

[25] Verisig: verifying safety properties of hybrid systems with neural network controllers [J].

Ivanov, Radoslav ;

Weimer, James ;

Alur, Rajeev ;

Pappas, George J. ;

Lee, Insup .

PROCEEDINGS OF THE 2019 22ND ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC '19), 2019, :169-178

[26]

Jahangirova Gunel, 2016, P 25 INT S SOFTW TES, P247, DOI [10.1145/2931037.2931062, DOI 10.1145/2931037.2931062]

[27] Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks [J].

Katz, Guy ;

Barrett, Clark ;

Dill, David L. ;

Julian, Kyle ;

Kochenderfer, Mykel J. .

COMPUTER AIDED VERIFICATION, CAV 2017, PT I, 2017, 10426 :97-117

[28] Verification of Image-based Neural Network Controllers Using Generative Models [J].

Katz, Sydney M. ;

Corso, Anthony L. ;

Strong, Christopher A. ;

Kochenderfer, Mykel J. .

2021 IEEE/AIAA 40TH DIGITAL AVIONICS SYSTEMS CONFERENCE (DASC), 2021,

[29]

Leino K, 2021, PR MACH LEARN RES, V139

[30] Into the Unknown: Active Monitoring of Neural Networks [J].

Lukina, Anna ;

Schilling, Christian ;

Henzinger, Thomas A. .

RUNTIME VERIFICATION (RV 2021), 2021, 12974 :42-61

← 1 2 3 4 5 →