-
(De-)Randomized Smoothing for Decision Stump Ensembles
Authors:
Miklós Z. Horváth,
Mark Niklas Müller,
Marc Fischer,
Martin Vechev
Abstract:
Tree-based models are used in many high-stakes application domains such as finance and medicine, where robustness and interpretability are of utmost importance. Yet, methods for improving and certifying their robustness are severely under-explored, in contrast to those focusing on neural networks. Targeting this important challenge, we propose deterministic smoothing for decision stump ensembles.…
▽ More
Tree-based models are used in many high-stakes application domains such as finance and medicine, where robustness and interpretability are of utmost importance. Yet, methods for improving and certifying their robustness are severely under-explored, in contrast to those focusing on neural networks. Targeting this important challenge, we propose deterministic smoothing for decision stump ensembles. Whereas most prior work on randomized smoothing focuses on evaluating arbitrary base models approximately under input randomization, the key insight of our work is that decision stump ensembles enable exact yet efficient evaluation via dynamic programming. Importantly, we obtain deterministic robustness certificates, even jointly over numerical and categorical features, a setting ubiquitous in the real world. Further, we derive an MLE-optimal training method for smoothed decision stumps under randomization and propose two boosting approaches to improve their provable robustness. An extensive experimental evaluation on computer vision and tabular data tasks shows that our approach yields significantly higher certified accuracies than the state-of-the-art for tree-based models. We release all code and trained models at https://github.com/eth-sri/drs.
△ Less
Submitted 14 November, 2022; v1 submitted 27 May, 2022;
originally announced May 2022.
-
Robust and Accurate -- Compositional Architectures for Randomized Smoothing
Authors:
Miklós Z. Horváth,
Mark Niklas Müller,
Marc Fischer,
Martin Vechev
Abstract:
Randomized Smoothing (RS) is considered the state-of-the-art approach to obtain certifiably robust models for challenging tasks. However, current RS approaches drastically decrease standard accuracy on unperturbed data, severely limiting their real-world utility. To address this limitation, we propose a compositional architecture, ACES, which certifiably decides on a per-sample basis whether to us…
▽ More
Randomized Smoothing (RS) is considered the state-of-the-art approach to obtain certifiably robust models for challenging tasks. However, current RS approaches drastically decrease standard accuracy on unperturbed data, severely limiting their real-world utility. To address this limitation, we propose a compositional architecture, ACES, which certifiably decides on a per-sample basis whether to use a smoothed model yielding predictions with guarantees or a more accurate standard model without guarantees. This, in contrast to prior approaches, enables both high standard accuracies and significant provable robustness. On challenging tasks such as ImageNet, we obtain, e.g., $80.0\%$ natural accuracy and $28.2\%$ certifiable accuracy against $\ell_2$ perturbations with $r=1.0$. We release our code and models at https://github.com/eth-sri/aces.
△ Less
Submitted 1 April, 2022;
originally announced April 2022.
-
An Attempt of Adaptive Heightfield Rendering with Complex Interpolants Using Ray Casting
Authors:
Daniel Cornel,
Zsolt Horváth,
Jürgen Waser
Abstract:
In this technical report, we document our attempt to visualize adaptive heightfields with smooth interpolation using ray casting in real time. The performance of ray casting depends strongly on the used interpolant and its efficient evaluation. Unfortunately, analytical solutions for ray-surface intersections are only given in the literature for very few simple, piece-wise polynomial surfaces. In…
▽ More
In this technical report, we document our attempt to visualize adaptive heightfields with smooth interpolation using ray casting in real time. The performance of ray casting depends strongly on the used interpolant and its efficient evaluation. Unfortunately, analytical solutions for ray-surface intersections are only given in the literature for very few simple, piece-wise polynomial surfaces. In our use case, we approximate the heightfield with radial basis functions defined on an adaptive grid, for which we propose a two-step solution: First, we reconstruct and discretize the currently visible portion of the surface with smooth approximation into a set of off-screen buffers. In a second step, we interpret these off-screen buffers as regular heightfields that can be rendered efficiently with ray casting using a simple bilinear interpolant. While our approach works, our quantitative evaluation shows that the performance depends strongly on the complexity and size of the heightfield. Real-time performance cannot be achieved for arbitrary heightfields, which is why we report our findings as a failed attempt to use ray casting for practical geospatial visualization in real time.
△ Less
Submitted 26 January, 2022;
originally announced January 2022.
-
Boosting Randomized Smoothing with Variance Reduced Classifiers
Authors:
Miklós Z. Horváth,
Mark Niklas Müller,
Marc Fischer,
Martin Vechev
Abstract:
Randomized Smoothing (RS) is a promising method for obtaining robustness certificates by evaluating a base model under noise. In this work, we: (i) theoretically motivate why ensembles are a particularly suitable choice as base models for RS, and (ii) empirically confirm this choice, obtaining state-of-the-art results in multiple settings. The key insight of our work is that the reduced variance o…
▽ More
Randomized Smoothing (RS) is a promising method for obtaining robustness certificates by evaluating a base model under noise. In this work, we: (i) theoretically motivate why ensembles are a particularly suitable choice as base models for RS, and (ii) empirically confirm this choice, obtaining state-of-the-art results in multiple settings. The key insight of our work is that the reduced variance of ensembles over the perturbations introduced in RS leads to significantly more consistent classifications for a given input. This, in turn, leads to substantially increased certifiable radii for samples close to the decision boundary. Additionally, we introduce key optimizations which enable an up to 55-fold decrease in sample complexity of RS for predetermined radii, thus drastically reducing its computational overhead. Experimentally, we show that ensembles of only 3 to 10 classifiers consistently improve on their strongest constituting model with respect to their average certified radius (ACR) by 5% to 21% on both CIFAR10 and ImageNet, achieving a new state-of-the-art ACR of 0.86 and 1.11, respectively. We release all code and models required to reproduce our results at https://github.com/eth-sri/smoothing-ensembles.
△ Less
Submitted 30 March, 2022; v1 submitted 13 June, 2021;
originally announced June 2021.
-
Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study
Authors:
Dániel Horpácsi,
Judit Kőszegi,
Zoltán Horváth
Abstract:
Widely used complex code refactoring tools lack a solid reasoning about the correctness of the transformations they implement, whilst interest in proven correct refactoring is ever increasing as only formal verification can provide true confidence in applying tool-automated refactoring to industrial-scale code. By using our strategic rewriting based refactoring specification language, we present t…
▽ More
Widely used complex code refactoring tools lack a solid reasoning about the correctness of the transformations they implement, whilst interest in proven correct refactoring is ever increasing as only formal verification can provide true confidence in applying tool-automated refactoring to industrial-scale code. By using our strategic rewriting based refactoring specification language, we present the decomposition of a complex transformation into smaller steps that can be expressed as instances of refactoring schemes, then we demonstrate the semi-automatic formal verification of the components based on a theoretical understanding of the semantics of the programming language. The extensible and verifiable refactoring definitions can be executed in our interpreter built on top of a static analyser framework.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.