pith. sign in

arxiv: 1906.10991 · v1 · pith:WA3BUD4Hnew · submitted 2019-06-26 · 💻 cs.LG · cs.AI· cs.CR· stat.ML

Verifying Robustness of Gradient Boosted Models

Gil Einziger , Maayan Goldstein , Yaniv Sa'ar , Itai Segall This is my paper

Pith reviewed 2026-05-25 16:00 UTC · model grok-4.3

classification 💻 cs.LG cs.AIcs.CRstat.ML
keywords gradient boosted modelsrobustness verificationSMT encodingformal verificationmachine learningdecision treesadversarial robustness
0
0 comments X

The pith

Encoding a gradient boosted model as an SMT formula lets verification tools prove its robustness to small input changes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces VeriGB, a method that converts both a gradient boosted model and a robustness specification into a single satisfiability-modulo-theories formula. Existing automated solvers can then decide whether every input within a bounded distance produces the same output. If the encoding is faithful, this supplies the first general way to obtain formal robustness guarantees for this widely used model family. Experiments on public datasets show the approach scales to sizable models and that some training choices produce models that are easier to verify as robust.

Core claim

VeriGB encodes the model and the robustness property as an SMT formula, which enables state of the art verification tools to prove the model's robustness. The tool is evaluated on publicly available datasets and demonstrates a capability for verifying large models. Some model configurations tend to be inherently more robust than others.

What carries the argument

VeriGB, the encoding of a gradient boosted model together with a robustness property into an SMT formula that off-the-shelf solvers can decide.

If this is right

  • Gradient boosted models of practical size become amenable to formal robustness proofs.
  • Certain hyper-parameter choices produce models whose robustness is easier to certify.
  • Verification tools originally built for other domains can be reused directly on these models.
  • Robustness can be checked after training rather than only during training.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding strategy might apply to other tree-ensemble methods without major redesign.
  • If the approach scales further, practitioners could add a verification step to model-selection pipelines.
  • Training objectives that explicitly favor easy-to-verify models could emerge as a new design target.

Load-bearing premise

The robustness property of a gradient boosted model can be captured exactly by an SMT formula without any approximation that would change the verification outcome.

What would settle it

An input example that lies inside the claimed robustness radius yet produces a different model output, or an SMT solver verdict of robustness that is contradicted by exhaustive enumeration on a small model.

Figures

Figures reproduced from arXiv: 1906.10991 by Gil Einziger, Itai Segall, Maayan Goldstein, Yaniv Sa'ar.

Figure 1
Figure 1. Figure 1: Example of the lack of robustness in a gradient [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: Examples of GTSRB images that satisfy the lo [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Examples of MNIST images that satisfy the lo [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Examples of MNIST images that do not satisfy [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
read the original abstract

Gradient boosted models are a fundamental machine learning technique. Robustness to small perturbations of the input is an important quality measure for machine learning models, but the literature lacks a method to prove the robustness of gradient boosted models. This work introduces VeriGB, a tool for quantifying the robustness of gradient boosted models. VeriGB encodes the model and the robustness property as an SMT formula, which enables state of the art verification tools to prove the model's robustness. We extensively evaluate VeriGB on publicly available datasets and demonstrate a capability for verifying large models. Finally, we show that some model configurations tend to be inherently more robust than others.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces VeriGB, a tool that encodes gradient boosted models (as piecewise-constant functions defined by tree splits and leaf values) together with a robustness specification (e.g., absence of adversarial examples inside an L_p ball) into an SMT formula. Off-the-shelf SMT solvers are then used to prove or disprove robustness. The authors report an extensive experimental evaluation on public datasets, demonstrate scalability to large ensembles, and observe that certain hyper-parameter choices (depth, number of trees, learning rate) correlate with higher verified robustness.

Significance. If the encoding is shown to be exact, the result would be significant: it supplies the first practical method for formally proving robustness of gradient-boosted ensembles, a model class widely deployed yet previously lacking verification support. The ability to handle realistically sized models and the empirical finding that some configurations are inherently more robust are both valuable. The work also demonstrates a reusable reduction to an existing, mature verification technology rather than a bespoke solver.

major comments (2)
  1. [§3] §3 (Encoding): the manuscript must explicitly argue that the SMT encoding of the sum of tree outputs and the split predicates is exact (no discretization of thresholds, no bounding of continuous features, no relaxation of the piecewise-constant semantics). Without such an argument or a machine-checked correspondence proof, a 'robust' SMT result may not transfer to the original model; this is load-bearing for the central claim.
  2. [§5] §5 (Evaluation): the reported verification times and success rates are given only for the encoded SMT instances. A direct comparison against the original floating-point model on the same robustness queries (or an error-bound analysis) is needed to confirm absence of false positives/negatives introduced by the encoding.
minor comments (2)
  1. [Definition 2] Notation for the robustness property (Definition 2) should be aligned with the SMT encoding in §3 so that the mapping is one-to-one.
  2. [Table 2] Table 2: the column 'verified robust' should also report the number of instances for which the solver returned 'unknown' or timed out, to give a complete picture of solver behavior.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment of the work's significance and for the constructive comments. We address each major comment below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [§3] §3 (Encoding): the manuscript must explicitly argue that the SMT encoding of the sum of tree outputs and the split predicates is exact (no discretization of thresholds, no bounding of continuous features, no relaxation of the piecewise-constant semantics). Without such an argument or a machine-checked correspondence proof, a 'robust' SMT result may not transfer to the original model; this is load-bearing for the central claim.

    Authors: We agree that an explicit argument for exactness is essential. In the revised manuscript we will add a dedicated subsection to §3 that formally establishes the correspondence. The encoding represents split predicates using exact real arithmetic over the original thresholds and feature values (no discretization or artificial bounds), preserves leaf values exactly, and computes the sum of tree outputs by direct addition without relaxation or approximation of the piecewise-constant semantics. Consequently, any robustness verdict returned by the SMT solver applies directly to the original model. revision: yes

  2. Referee: [§5] §5 (Evaluation): the reported verification times and success rates are given only for the encoded SMT instances. A direct comparison against the original floating-point model on the same robustness queries (or an error-bound analysis) is needed to confirm absence of false positives/negatives introduced by the encoding.

    Authors: We will revise §5 to include the requested validation. On a representative subset of queries we will evaluate the original floating-point implementation of each model and compare the outcomes with the SMT results, reporting any discrepancies. We will also add a short error-bound discussion that analyzes potential numerical differences; because the encoding is exact, we expect none to arise from the translation itself. This addition will empirically confirm that the reported verification outcomes are faithful to the original models. revision: yes

Circularity Check

0 steps flagged

No circularity: novel SMT encoding presented as direct translation without reduction to fitted inputs or self-citations

full rationale

The paper introduces VeriGB as a new encoding of gradient-boosted tree ensembles and robustness specifications directly into SMT formulas, enabling off-the-shelf solvers. No equations, parameters, or predictions are described that reduce the claimed verification capability to a definition, fit, or prior self-citation. The core claim rests on the faithfulness of the encoding itself rather than any derived quantity that loops back to inputs. This is the common case of a self-contained methodological contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that gradient boosted models admit a precise SMT encoding and that SMT solvers can decide the resulting formulas for realistic model sizes.

axioms (1)
  • domain assumption Gradient boosted models and their robustness properties can be encoded as SMT formulas without loss of precision for verification purposes.
    This is the load-bearing premise that allows the use of off-the-shelf solvers; it is invoked when the abstract states that the model and property are encoded as an SMT formula.

pith-pipeline@v0.9.0 · 5637 in / 1213 out tokens · 45462 ms · 2026-05-25T16:00:22.036885+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages · 2 internal anchors

  1. [1]

    C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, pages 825–885. IOS Press, 2009

    work page 2009

  2. [2]

    Biggio, I

    B. Biggio, I. Corona, B. Nelson, B. I. P. Rubinstein, D. Maiorca, G. Fumera, G. Giacinto, and F. Roli.Secu- rity Evaluation of Support Vector Machines in Adver- sarial Environments, pages 105–153. Springer Interna- tional Publishing, Cham, 2014

    work page 2014

  3. [3]

    Biggio, G

    B. Biggio, G. Fumera, and F. Roli. Pattern recognition systems under attack: Design issues and research chal- lenges. IJPRAI, 28(7), 2014

    work page 2014

  4. [4]

    Biggio, G

    B. Biggio, G. Fumera, and F. Roli. Security evaluation of pattern classifiers under attack. IEEE Transactions on Knowledge and Data Engineering , 26(4):984–996, April 2014

    work page 2014

  5. [5]

    Buitinck, G

    L. Buitinck, G. Louppe, M. Blondel, F. Pedregosa, A. Mueller, O. Grisel, V . Niculae, P. Prettenhofer, A. Gramfort, J. Grobler, R. Layton, J. VanderPlas, A. Joly, B. Holt, and G. Varoquaux. API design for machine learning software: experiences from the scikit- learn project. In ECML PKDD Workshop: Languages for Data Mining and Machine Learning , pages 108...

    work page 2013

  6. [6]

    Caruana and A

    R. Caruana and A. Niculescu-Mizil. An empirical com- parison of supervised learning algorithms. In Proceed- ings of the 23rd International Conference on Machine Learning, ICML ’06, pages 161–168, New York, NY , USA, 2006. ACM

    work page 2006

  7. [7]

    Chapelle and Y

    O. Chapelle and Y . Chang. Yahoo! learning to rank challenge overview. In Proceedings of the 2010 Inter- national Conference on Yahoo! Learning to Rank Chal- lenge - Volume 14, YLRC’10, pages 1–24. JMLR.org, 2010

    work page 2010

  8. [8]

    De Moura and N

    L. De Moura and N. Bjørner. Z3: An efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Sys- tems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg, 2008. Springer-Verlag

    work page 2008

  9. [9]

    R. Ehlers. Formal verification of piece-wise linear feed-forward neural networks. CoRR, abs/1705.01320, 2017

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  10. [10]

    Freund and R

    Y . Freund and R. E. Schapire. A decision-theoretic generalization of on-line learning and an application to boosting. Journal of Computer and System Sciences , 55(1):119 – 139, 1997

    work page 1997

  11. [11]

    T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. T. Vechev. Ai: Safety and ro- bustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), 2018

    work page 2018

  12. [12]

    Hastie, R

    T. Hastie, R. Tibshirani, and J. Friedman. The Elements of Statistical Learning . Springer Series in Statistics. Springer New York Inc., New York, NY , USA, 2001

    work page 2001

  13. [13]

    Houben, J

    S. Houben, J. Stallkamp, J. Salmen, M. Schlipsing, and C. Igel. Detection of traffic signs in real-world im- ages: The German Traffic Sign Detection Benchmark. In The 2013 International Joint Conference on Neural Networks (IJCNN), pages 1–8, 2013

    work page 2013

  14. [14]

    https://www.kaggle.com/harlfoxem/housesalesprediction/home, 2018

    House Sales in King County, USA. https://www.kaggle.com/harlfoxem/housesalesprediction/home, 2018. 10

    work page 2018

  15. [15]

    Huang, M

    X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. Safety verification of deep neural networks. In R. Ma- jumdar and V . Kunˇcak, editors, Computer Aided Verifi- cation, pages 3–29, Cham, 2017. Springer International Publishing

    work page 2017

  16. [16]

    Jones, T

    E. Jones, T. Oliphant, P. Peterson, et al. SciPy: Open source scientific tools for Python, 2001

    work page 2001

  17. [17]

    G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In R. Majumdar and V . Kuncak, editors,Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Ger- many, July 24-28, 2017, Proceedings, Part I , volume 10426 of Lecture Notes in Computer Sci...

    work page 2017

  18. [18]

    Y . LeCun. The mnist database of handwritten digits. http://yann.lecun.com/exdb/mnist/, 1998

    work page 1998

  19. [19]

    Leistner, A

    C. Leistner, A. Saffari, P. M. Roth, and H. Bischof. On robustness of on-line boosting - a competitive study. In 2009 IEEE 12th International Conference on Computer Vision Workshops, ICCV Workshops, pages 1362–1369, Sept 2009

    work page 2009

  20. [20]

    Mason, J

    L. Mason, J. Baxter, P. Bartlett, and M. Frean. Boosting algorithms as gradient descent. In Proceedings of the 12th International Conference on Neural Information Processing Systems , NIPS’99, pages 512–518, Cam- bridge, MA, USA, 1999. MIT Press

    work page 1999

  21. [21]

    Moosavi-Dezfooli, A

    S. Moosavi-Dezfooli, A. Fawzi, O. Fawzi, and P. Frossard. Universal adversarial perturbations. In 2017 IEEE Conference on Computer Vision and Pat- tern Recognition (CVPR), pages 86–94, July 2017

    work page 2017

  22. [22]

    Narodytska, S

    N. Narodytska, S. P. Kasiviswanathan, L. Ryzhyk, M. Sagiv, and T. Walsh. Verifying properties of bi- narized deep neural networks. In S. A. McIlraith and K. Q. Weinberger, editors, Proceedings of the Thirty- Second AAAI Conference on Artificial Intelligence, New Orleans, Louisiana, USA, February 2-7, 2018 . AAAI Press, 2018

    work page 2018

  23. [23]

    Pulina and A

    L. Pulina and A. Tacchella. An abstraction-refinement approach to verification of artificial neural networks. In Proceedings of the 22Nd International Conference on Computer Aided Verification, CA V’10, pages 243–257, Berlin, Heidelberg, 2010. Springer-Verlag

    work page 2010

  24. [24]

    Pulina and A

    L. Pulina and A. Tacchella. Challenging smt solvers to verify neural networks. AI Communications , 25(2):117–135, Apr. 2012

    work page 2012

  25. [25]

    Y . Sun, S. Todorovic, and J. Li. Increasing the robustness of boosting algorithms within the linear- programming framework. The Journal of VLSI Signal Processing Systems for Signal, Image, and Video Tech- nology, 48(1):5–20, Aug 2007

    work page 2007

  26. [26]

    Viola and M

    P. Viola and M. Jones. Rapid object detection using a boosted cascade of simple features. In Proceedings of the 2001 IEEE Computer Society Conference on Com- puter Vision and Pattern Recognition. CVPR 2001, vol- ume 1, pages I–511–I–518 vol.1, 2001

    work page 2001

  27. [27]

    B. Yang, J. Yan, Z. Lei, and S. Z. Li. Convolutional channel features for pedestrian, face and edge detec- tion. CoRR, abs/1504.07339, 2015

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  28. [28]

    Zhang and A

    Y . Zhang and A. Haghani. A gradient boosting method to improve travel time prediction. In Transportation Research Part C Emerging Technologies , volume 58, 03 2015

    work page 2015

  29. [29]

    Y . Zhou, M. Kantarcioglu, B. Thuraisingham, and B. Xi. Adversarial support vector machine learning. In Proceedings of the 18th ACM SIGKDD International Conference on Knowledge Discovery and Data Min- ing, KDD ’12, pages 1059–1067, New York, NY , USA,

    work page