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

Direct link
BETA
Törnblom, John
Publications (3 of 3) Show all publications
Törnblom, J. & Nadjm-Tehrani, S. (2020). Formal Verification of Input-Output Mappings of Tree Ensembles. Science of Computer Programming, 194
Open this publication in new window or tab >>Formal Verification of Input-Output Mappings of Tree Ensembles
2020 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 194Article in journal (Refereed) Published
Abstract [en]

Recent advances in machine learning and artificial intelligence are now beingconsidered in safety-critical autonomous systems where software defects maycause severe harm to humans and the environment. Design organizations in thesedomains are currently unable to provide convincing arguments that their systemsare safe to operate when machine learning algorithms are used to implement theirsoftware.

In this paper, we present an efficient method to extract equivalence classes from decision trees and tree ensembles, and to formally verify that their input-output mappings comply with requirements. The idea is that, given that safety requirements can be traced to desirable properties on system input-output patterns, we can use positive verification outcomes in safety arguments.

This paper presents the implementation of the method in the tool VoTE (Verifier of Tree Ensembles), and evaluates its scalability on two case studies presented in current literature. We demonstrate that our method is practical for tree ensembles trained on low-dimensional data with up to 25 decision trees and tree depths of up to 20.Our work also studies the limitations of the method with high-dimensionaldata and preliminarily investigates the trade-off between large number of trees and time taken for verification.

Keywords
Formal verification, Decision tree, Tree ensemble, Random forest, Gradient boosting machine
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-164563 (URN)10.1016/j.scico.2020.102450 (DOI)
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2020-03-24 Created: 2020-03-24 Last updated: 2020-04-24
Törnblom, J. & Nadjm-Tehrani, S. (2019). An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles. In: Computer Safety, Reliability, and Security: SAFECOMP 2019 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Turku, Finland, September 10, 2019, Proceedings. Paper presented at ​Second International Workshop on Artificial Intelligence Safety Engineering (pp. 301-313). Springer
Open this publication in new window or tab >>An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles
2019 (English)In: Computer Safety, Reliability, and Security: SAFECOMP 2019 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Turku, Finland, September 10, 2019, Proceedings, Springer, 2019, p. 301-313Conference paper, Published paper (Refereed)
Abstract [en]

Recent advances in machine learning are now being considered for integration in safety-critical systems such as vehicles, medical equipment and critical infrastructure. However, organizations in these domains are currently unable to provide convincing arguments that systems integrating machine learning technologies are safe to operate in their intended environments.

In this paper, we present a formal verification method for tree ensembles that leverage an abstraction-refinement approach to counteract combinatorial explosion. We implemented the method as an extension to a tool named VoTE, and demonstrate its applicability by verifying the robustness against perturbations in random forests and gradient boosting machines in two case studies. Our abstraction-refinement based extension to VoTE improves the performance by several orders of magnitude, scaling to tree ensembles with up to 50 trees with depth 10, trained on high-dimensional data.

Place, publisher, year, edition, pages
Springer, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11699
Keywords
Formal verification, Decision trees, Tree ensembles
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-160869 (URN)10.1007/978-3-030-26250-1_24 (DOI)978-3-030-26249-5 (ISBN)
Conference
​Second International Workshop on Artificial Intelligence Safety Engineering
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2019-10-11 Created: 2019-10-11 Last updated: 2019-11-14
Törnblom, J. & Nadjm-Tehrani, S. (2019). Formal Verification of Random Forests in Safety-Critical Applications. In: Formal Techniques for Safety-Critical Systems: . Paper presented at Sixth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2018), Gold Coast, Australia, 16 November, 2018 (pp. 55-71). Springer
Open this publication in new window or tab >>Formal Verification of Random Forests in Safety-Critical Applications
2019 (English)In: Formal Techniques for Safety-Critical Systems, Springer, 2019, p. 55-71Conference paper, Published paper (Refereed)
Abstract [en]

Recent advances in machine learning and artificial intelligence are now being applied in safety-critical autonomous systems where software defects may cause severe harm to humans and the environment. Design organizations in these domains are currently unable to provide convincing arguments that systems using complex software implemented using machine learning algorithms are safe and correct.

In this paper, we present an efficient method to extract equivalence classes from decision trees and random forests, and to formally verify that their input/output mappings comply with requirements. We implement the method in our tool VoRF (Verifier of Random Forests), and evaluate its scalability on two case studies found in the literature. We demonstrate that our method is practical for random forests trained on low-dimensional data with up to 25 decision trees, each with a tree depth of 20. Our work also demonstrates the limitations of the method with high-dimensional data and touches upon the trade-off between large number of trees and time taken for verification.

Place, publisher, year, edition, pages
Springer, 2019
Series
Communications in Computer and Information Science, ISSN 1865-0929 ; 008
Keywords
Machine learning, Formal verification, Random forest, Decision tree
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-154368 (URN)10.1007/978-3-030-12988-0_4 (DOI)978-3-030-12987-3 (ISBN)978-3-030-12988-0 (ISBN)
Conference
Sixth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2018), Gold Coast, Australia, 16 November, 2018
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2019-02-07 Created: 2019-02-07 Last updated: 2019-02-15Bibliographically approved
Organisations

Search in DiVA

Show all publications