arXiv subjects

Chih-Hong Cheng

Publications and source records attributed to Chih-Hong Cheng.

At least 55 records · Page 3Linked to original sources

arXiv2021

Continuous Safety Verification of Neural Networks

Deploying deep neural networks (DNNs) as core functions in autonomous driving creates unique verification and validation challenges. In particular, the continuous engineering paradigm of gradually perfecting a DNN-based perception can make the previously established result of safety verification no longer valid. This can occur either due to the newly encountered examples (i.e., input domain enlargement) inside the Operational Design Domain or due to the subsequent parameter fine-tuning activities of a DNN. This paper considers approaches to transfer results established in the previous DNN safety verification problem to the modified problem setting. By considering the reuse of state abstractions, network abstractions, and Lipschitz constants, we develop several sufficient conditions that only require formally analyzing a small part of the DNN in the new problem. The overall concept is evaluated in a $1/10$-scaled vehicle that equips a DNN controller to determine the visual waypoint from the perceived image.

cs.LG↗

arXiv2021

Provably-Robust Runtime Monitoring of Neuron Activation Patterns

For deep neural networks (DNNs) to be used in safety-critical autonomous driving tasks, it is desirable to monitor in operation time if the input for the DNN is similar to the data used in DNN training. While recent results in monitoring DNN activation patterns provide a sound guarantee due to building an abstraction out of the training data set, reducing false positives due to slight input perturbation has been an issue towards successfully adapting the techniques. We address this challenge by integrating formal symbolic reasoning inside the monitor construction process. The algorithm performs a sound worst-case estimate of neuron values with inputs (or features) subject to perturbation, before the abstraction function is applied to build the monitor. The provable robustness is further generalized to cases where monitoring a single neuron can use more than one bit, implying that one can record activation patterns with a fine-grained decision on the neuron value interval.

cs.LG↗

arXiv2021

Testing Autonomous Systems with Believed Equivalence Refinement

Continuous engineering of autonomous driving functions commonly requires deploying vehicles in road testing to obtain inputs that cause problematic decisions. Although the discovery leads to producing an improved system, it also challenges the foundation of testing using equivalence classes and the associated relative test coverage criterion. In this paper, we propose believed equivalence, where the establishment of an equivalence class is initially based on expert belief and is subject to a set of available test cases having a consistent valuation. Upon a newly encountered test case that breaks the consistency, one may need to refine the established categorization in order to split the originally believed equivalence into two. Finally, we focus on modules implemented using deep neural networks where every category partitions an input over the real domain. We present both analytical and lazy methods to suggest the refinement. The concept is demonstrated in analyzing multiple autonomous driving modules, indicating the potential of our proposed approach.

cs.AI↗

arXiv2021

Safety Metrics for Semantic Segmentation in Autonomous Driving

Within the context of autonomous driving, safety-related metrics for deep neural networks have been widely studied for image classification and object detection. In this paper, we further consider safety-aware correctness and robustness metrics specialized for semantic segmentation. The novelty of our proposal is to move beyond pixel-level metrics: Given two images with each having N pixels being class-flipped, the designed metrics should, depending on the clustering of pixels being class-flipped or the location of occurrence, reflect a different level of safety criticality. The result evaluated on an autonomous driving dataset demonstrates the validity and practicality of our proposed methodology.

cs.CV↗

arXiv2021

Monitoring Object Detection Abnormalities via Data-Label and Post-Algorithm Abstractions

While object detection modules are essential functionalities for any autonomous vehicle, the performance of such modules that are implemented using deep neural networks can be, in many cases, unreliable. In this paper, we develop abstraction-based monitoring as a logical framework for filtering potentially erroneous detection results. Concretely, we consider two types of abstraction, namely data-label abstraction and post-algorithm abstraction. Operated on the training dataset, the construction of data-label abstraction iterates each input, aggregates region-wise information over its associated labels, and stores the vector under a finite history length. Post-algorithm abstraction builds an abstract transformer for the tracking algorithm. Elements being associated together by the abstract transformer can be checked against consistency over their original values. We have implemented the overall framework to a research prototype and validated it using publicly available object detection datasets.

cs.AI↗

arXiv2020

Safety-Aware Hardening of 3D Object Detection Neural Network Systems

We study how state-of-the-art neural networks for 3D object detection using a single-stage pipeline can be made safety aware. We start with the safety specification (reflecting the capability of other components) that partitions the 3D input space by criticality, where the critical area employs a separate criterion on robustness under perturbation, quality of bounding boxes, and the tolerance over false negatives demonstrated on the training set. In the architecture design, we consider symbolic error propagation to allow feature-level perturbation. Subsequently, we introduce a specialized loss function reflecting (1) the safety specification, (2) the use of single-stage detection architecture, and finally, (3) the characterization of robustness under perturbation. We also replace the commonly seen non-max-suppression post-processing algorithm by a safety-aware non-max-inclusion algorithm, in order to maintain the safety claim created by the neural network. The concept is detailed by extending the state-of-the-art PIXOR detector which creates object bounding boxes in bird's eye view with inputs from point clouds.

cs.LG↗

arXiv2019

Towards Safety Verification of Direct Perception Neural Networks

We study the problem of safety verification of direct perception neural networks, where camera images are used as inputs to produce high-level features for autonomous vehicles to make control decisions. Formal verification of direct perception neural networks is extremely challenging, as it is difficult to formulate the specification that requires characterizing input as constraints, while the number of neurons in such a network can reach millions. We approach the specification problem by learning an input property characterizer which carefully extends a direct perception neural network at close-to-output layers, and address the scalability problem by a novel assume-guarantee based verification approach. The presented workflow is used to understand a direct perception neural network (developed by Audi) which computes the next waypoint and orientation for autonomous vehicles to follow.

cs.SE↗

arXiv2019

Towards Robust Direct Perception Networks for Automated Driving

We consider the problem of engineering robust direct perception neural networks with output being regression. Such networks take high dimensional input image data, and they produce affordances such as the curvature of the upcoming road segment or the distance to the front vehicle. Our proposal starts by allowing a neural network prediction to deviate from the label with tolerance $Δ$. The source of tolerance can be either contractual or from limiting factors where two entities may label the same data with slightly different numerical values. The tolerance motivates the use of a non-standard loss function where the loss is set to $0$ so long as the prediction-to-label distance is less than $Δ$. We further extend the loss function and define a new provably robust criterion that is parametric to the allowed output tolerance $Δ$, the layer index $\tilde{l}$ where perturbation is considered, and the maximum perturbation amount $κ$. During training, the robust loss is computed by first propagating symbolic errors from the $\tilde{l}$-th layer (with quantity bounded by $κ$) to the output layer, followed by computing the overflow between the error bounds and the allowed tolerance. The overall concept is experimented in engineering a direct perception neural network for understanding the central position of the ego-lane in pixel coordinates.

cs.LG↗

arXiv2019

nn-dependability-kit: Engineering Neural Networks for Safety-Critical Autonomous Driving Systems

Can engineering neural networks be approached in a disciplined way similar to how engineers build software for civil aircraft? We present nn-dependability-kit, an open-source toolbox to support safety engineering of neural networks for autonomous driving systems. The rationale behind nn-dependability-kit is to consider a structured approach (via Goal Structuring Notation) to argue the quality of neural networks. In particular, the tool realizes recent scientific results including (a) novel dependability metrics for indicating sufficient elimination of uncertainties in the product life cycle, (b) formal reasoning engine for ensuring that the generalization does not lead to undesired behaviors, and (c) runtime monitoring for reasoning whether a decision of a neural network in operation is supported by prior similarities in the training data. A proprietary version of nn-dependability-kit has been used to improve the quality of a level-3 autonomous driving component developed by Audi for highway maneuvers.

cs.LG↗

arXiv2019

Architecting Dependable Learning-enabled Autonomous Systems: A Survey

We provide a summary over architectural approaches that can be used to construct dependable learning-enabled autonomous systems, with a focus on automated driving. We consider three technology pillars for architecting dependable autonomy, namely diverse redundancy, information fusion, and runtime monitoring. For learning-enabled components, we additionally summarize recent architectural approaches to increase the dependability beyond standard convolutional neural networks. We conclude the study with a list of promising research directions addressing the challenges of existing approaches.

cs.SE↗

arXiv2018

Runtime Monitoring Neuron Activation Patterns

For using neural networks in safety critical domains, it is important to know if a decision made by a neural network is supported by prior similarities in training. We propose runtime neuron activation pattern monitoring - after the standard training process, one creates a monitor by feeding the training data to the network again in order to store the neuron activation patterns in abstract form. In operation, a classification decision over an input is further supplemented by examining if a pattern similar (measured by Hamming distance) to the generated pattern is contained in the monitor. If the monitor does not contain any pattern similar to the generated pattern, it raises a warning that the decision is not based on the training data. Our experiments show that, by adjusting the similarity-threshold for activation patterns, the monitors can report a significant portion of misclassfications to be not supported by training with a small false-positive rate, when evaluated on a test set.

cs.LG↗

arXiv2018

Towards Dependability Metrics for Neural Networks

Artificial neural networks (NN) are instrumental in realizing highly-automated driving functionality. An overarching challenge is to identify best safety engineering practices for NN and other learning-enabled components. In particular, there is an urgent need for an adequate set of metrics for measuring all-important NN dependability attributes. We address this challenge by proposing a number of NN-specific and efficiently computable metrics for measuring NN dependability attributes including robustness, interpretability, completeness, and correctness.

cs.LG↗

arXiv2018

Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems

Systematically testing models learned from neural networks remains a crucial unsolved barrier to successfully justify safety for autonomous vehicles engineered using data-driven approach. We propose quantitative k-projection coverage as a metric to mediate combinatorial explosion while guiding the data sampling process. By assuming that domain experts propose largely independent environment conditions and by associating elements in each condition with weights, the product of these conditions forms scenarios, and one may interpret weights associated with each equivalence class as relative importance. Achieving full k-projection coverage requires that the data set, when being projected to the hyperplane formed by arbitrarily selected k-conditions, covers each class with number of data points no less than the associated weight. For the general case where scenario composition is constrained by rules, precisely computing k-projection coverage remains in NP. In terms of finding minimum test cases to achieve full coverage, we present theoretical complexity for important sub-cases and an encoding to 0-1 integer programming. We have implemented a research prototype that generates test cases for a visual object defection unit in automated driving, demonstrating the technological feasibility of our proposed coverage criterion.

cs.SE↗

arXiv2018

Verification of Binarized Neural Networks via Inter-Neuron Factoring

We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a energy-efficient alternative to traditional learning networks. The verification of BNNs, using the reduction to hardware verification, can be even more scalable by factoring computations among neurons within the same layer. By proving the NP-hardness of finding optimal factoring as well as the hardness of PTAS approximability, we design polynomial-time search heuristics to generate factoring solutions. The overall framework allows applying verification techniques to moderately-sized BNNs for embedded devices with thousands of neurons and inputs.

cs.SE↗

arXiv2017

Neural Networks for Safety-Critical Applications - Challenges, Experiments and Perspectives

We propose a methodology for designing dependable Artificial Neural Networks (ANN) by extending the concepts of understandability, correctness, and validity that are crucial ingredients in existing certification standards. We apply the concept in a concrete case study in designing a high-way ANN-based motion predictor to guarantee safety properties such as impossibility for the ego vehicle to suggest moving to the right lane if there exists another vehicle on its right.

cs.SE↗

arXiv2017

Maximum Resilience of Artificial Neural Networks

The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of ANN-based classifiers as the maximal amount of input or sensor perturbation which is still tolerated. This problem of computing maximal perturbation bounds for ANNs is then reduced to solving mixed integer optimization problems (MIP). A number of MIP encoding heuristics are developed for drastically reducing MIP-solver runtimes, and using parallelization of MIP-solvers results in an almost linear speed-up in the number (up to a certain limit) of computing cores in our experiments. We demonstrate the effectiveness and scalability of our approach by means of computing maximal resilience bounds for a number of ANN benchmark sets ranging from typical image recognition scenarios to the autonomous maneuvering of robots.

cs.LG↗

arXiv2017

Automated Analysis of Multi-View Software Architectures

Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for certain stylized, and widely used, multi-view architectures by suitably interpreting and fusing sub-models from different UML diagrams. Possible counter-examples produced by model checking are fed back as test scenarios for debugging the multi-view architectural model. We have implemented this algorithm as a plug-in for the Enterprise Architect development tool, and successfully used SPIN model checking for debugging some industrial architectural multi-view models by identifying a number of undesirable corner cases.

cs.SE↗

arXiv2016

Structural Synthesis for GXW Specifications

We define the GXW fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since GXW includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For GXW controller specifications, we develop a novel approach for synthesizing a set of synchronously communicating actor-based controllers. This synthesis algorithm proceeds by means of recursing over the structure of GXW specifications, and generates a set of dedicated and synchronously communicating sub-controllers according to the formula structure. In a subsequent step, 2QBF constraint solving identifies and tries to resolve potential conflicts between individual GXW specifications. This structural approach to GXW synthesis supports traceability between requirements and the generated control code as mandated by certification regimes for safety-critical software. Synthesis for GXW specifications is in PSPACE compared to 2EXPTIME-completeness of full-fledged LTL synthesis. Indeed our experimental results suggest that GXW synthesis scales well to industrial-sized control synthesis problems with 20 input and output ports and beyond.

cs.LO↗