Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles

• URL: http://arxiv.org/abs/2105.02595v1
• Date: Thu, 6 May 2021 11:50:22 GMT
• Title: Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles
• Authors: John T\"ornblom and Simin Nadjm-Tehrani
• Abstract summary: We formalise and extend the VoTE algorithm presented earlier as a tool description. We show how the separation of property checking from the core verification engine enables verification of versatile requirements. We demonstrate the application of the tool in two case studies, namely digit recognition and aircraft collision avoidance.
• Score: 2.588973722689844
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: To guarantee that machine learning models yield outputs that are not only accurate, but also robust, recent works propose formally verifying robustness properties of machine learning models. To be applicable to realistic safety-critical systems, the used verification algorithms need to manage the combinatorial explosion resulting from vast variations in the input domain, and be able to verify correctness properties derived from versatile and domain-specific requirements. In this paper, we formalise the VoTE algorithm presented earlier as a tool description, and extend the tool set with mechanisms for systematic scalability studies. In particular, we show a) how the separation of property checking from the core verification engine enables verification of versatile requirements, b) the scalability of the tool, both in terms of time taken for verification and use of memory, and c) that the algorithm has attractive properties that lend themselves well for massive parallelisation. We demonstrate the application of the tool in two case studies, namely digit recognition and aircraft collision avoidance, where the first case study serves to assess the resource utilisation of the tool, and the second to assess the ability to verify versatile correctness properties.

Related papers

• Quantitative Assurance and Synthesis of Controllers from Activity Diagrams [4.419843514606336]
  Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties. This makes it not accessible for researchers and engineers who may not have the required knowledge. We propose a comprehensive verification framework for ADs, including a new profile for probability time, quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language. Most importantly, we developed algorithms for transformation and implemented them in a tool, called QASCAD, using model-based techniques, for fully automated verification.
  arXiv  Detail & Related papers  (2024-02-29T22:40:39Z)
• Fine-Tuning Enhances Existing Mechanisms: A Case Study on Entity Tracking [53.66999416757543]
  We study how fine-tuning affects the internal mechanisms implemented in language models. Fine-tuning enhances, rather than alters, the mechanistic operation of the model.
  arXiv  Detail & Related papers  (2024-02-22T18:59:24Z)
• Improving Adaptive Conformal Prediction Using Self-Supervised Learning [72.2614468437919]
  We train an auxiliary model with a self-supervised pretext task on top of an existing predictive model and use the self-supervised error as an additional feature to estimate nonconformity scores. We empirically demonstrate the benefit of the additional information using both synthetic and real data on the efficiency (width), deficit, and excess of conformal prediction intervals.
  arXiv  Detail & Related papers  (2023-02-23T18:57:14Z)
• A Correct-and-Certify Approach to Self-Supervise Object Pose Estimators via Ensemble Self-Training [26.47895284071508]
  Real-world robotics applications demand object pose estimation methods that work reliably across a variety of scenarios. Our first contribution is to develop a robust corrector module that corrects pose estimates using depth information. Our second contribution is an ensemble self-training approach that simultaneously trains multiple pose estimators in a self-supervised manner.
  arXiv  Detail & Related papers  (2023-02-12T23:02:03Z)
• Specifying and Testing $k$-Safety Properties for Machine-Learning Models [20.24045879238586]
  We take inspiration from specifications used in formal methods, expressing $k$ different executions, so-called $k$-safety properties. Here, we show the wide applicability of $k$-safety properties for machine-learning models and present the first specification language for expressing them. Our framework is effective in identifying property violations, and that detected bugs could be used to train better models.
  arXiv  Detail & Related papers  (2022-06-13T11:35:55Z)
• Information-Theoretic Odometry Learning [83.36195426897768]
  We propose a unified information theoretic framework for learning-motivated methods aimed at odometry estimation. The proposed framework provides an elegant tool for performance evaluation and understanding in information-theoretic language.
  arXiv  Detail & Related papers  (2022-03-11T02:37:35Z)
• Fantastic Features and Where to Find Them: Detecting Cognitive Impairment with a Subsequence Classification Guided Approach [6.063165888023164]
  We describe a new approach to feature engineering that leverages sequential machine learning models and domain knowledge to predict which features help enhance performance. We demonstrate that CI classification accuracy improves by 2.3% over a strong baseline when using features produced by this method.
  arXiv  Detail & Related papers  (2020-10-13T17:57:18Z)
• Verification of ML Systems via Reparameterization [6.482926592121413]
  We show how a probabilistic program can be automatically represented in a theorem prover. We also prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.
  arXiv  Detail & Related papers  (2020-07-14T02:19:25Z)
• A Trainable Optimal Transport Embedding for Feature Aggregation and its Relationship to Attention [96.77554122595578]
  We introduce a parametrized representation of fixed size, which embeds and then aggregates elements from a given input set according to the optimal transport plan between the set and a trainable reference. Our approach scales to large datasets and allows end-to-end training of the reference, while also providing a simple unsupervised learning mechanism with small computational cost.
  arXiv  Detail & Related papers  (2020-06-22T08:35:58Z)
• Generating Fact Checking Explanations [52.879658637466605]
  A crucial piece of the puzzle that is still missing is to understand how to automate the most elaborate part of the process. This paper provides the first study of how these explanations can be generated automatically based on available claim context. Our results indicate that optimising both objectives at the same time, rather than training them separately, improves the performance of a fact checking system.
  arXiv  Detail & Related papers  (2020-04-13T05:23:25Z)
• Adaptive Object Detection with Dual Multi-Label Prediction [78.69064917947624]
  We propose a novel end-to-end unsupervised deep domain adaptation model for adaptive object detection. The model exploits multi-label prediction to reveal the object category information in each image. We introduce a prediction consistency regularization mechanism to assist object detection.
  arXiv  Detail & Related papers  (2020-03-29T04:23:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.