liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of Tree Ensembles against Real-World Composite Geometric Perturbations
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0001-6405-4794
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0002-1485-0802
2023 (English)In: Proceedings of the Workshop on Artificial Intelligence Safety 2023 (SafeAI 2023) co-located with the Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI 2023) / [ed] Pedroza G., Huang X., Chen X.C., Theodorou A., Hernandez-Orallo J., Castillo-Effen M., Mallah R., McDermid J., CEUR-WS , 2023, Vol. 3381, article id 38Conference paper, Published paper (Refereed)
Abstract [en]

Since machine learning components are now being considered for integration in safety-critical systems, safety stakeholdersshould be able to provide convincing arguments that the systems are safe for use in realistic deployment settings. In the caseof vision-based systems, the use of tree ensembles calls for formal stability verification against a host of composite geometricperturbations that the system may encounter. Such perturbations are a combination of an affine transformation like rotation,scaling, or translation and a pixel-wise transformation like changes in lighting. However, existing verification approachesmostly target small norm-based perturbations, and do not account for composite geometric perturbations. In this work,we present a novel method to precisely define the desired stability regions for these types of perturbations. We propose afeature space modelling process that generates abstract intervals which can be passed to VoTE, an efficient formal verificationengine that is specialised for tree ensembles. Our method is implemented as an extension to VoTE by defining a new propertychecker. The applicability of the method is demonstrated by verifying classifier stability and computing metrics associatedwith stability and correctness, i.e., robustness, fragility, vulnerability, and breakage, in two case studies. In both case studies,targeted data augmentation pre-processing steps were applied for robust model training. Our results show that even modelstrained with augmented data are unable to handle these types of perturbations, thereby emphasising the need for certifiedrobust training for tree ensembles.

Place, publisher, year, edition, pages
CEUR-WS , 2023. Vol. 3381, article id 38
Series
CEUR Workshop Proceedings, ISSN 1613-0073 ; 3381
Keywords [en]
Machine Learning, Formal Verification, Tree Ensembles, Composite Perturbations, Geometric Perturbations, Random Forests, Gradient Boosting Machines, Semantic Perturbations, Stability, Robustness, Trustworthy AI, Trustworthy Computing
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-195996Scopus ID: 2-s2.0-85159287306OAI: oai:DiVA.org:liu-195996DiVA, id: diva2:1778078
Conference
The AAAI-23 Workshop on Artificial Intelligence Safety (SafeAI 2023), Washington DC, USA, February 13-14, 2023
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)Available from: 2023-06-30 Created: 2023-06-30 Last updated: 2024-10-28Bibliographically approved

Open Access in DiVA

fulltext(1169 kB)8 downloads
File information
File name FULLTEXT02.pdfFile size 1169 kBChecksum SHA-512
84acb0ad5dafe7897357c8ce5b0b3447fde03477e1d944140af08f2b1f5f3e3ad053afef47efbbf9f9b9f01218e43982ca38851382d09ae40c9aa0e8986f348e
Type fulltextMimetype application/pdf

Other links

ScopusKonferensens hemsida / Link to conference

Authority records

Colaco, ValencyNadjm-Tehrani, Simin

Search in DiVA

By author/editor
Colaco, ValencyNadjm-Tehrani, Simin
By organisation
Software and SystemsFaculty of Science & Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 8 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 209 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf