liu.seSök publikationer i DiVA
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of Input-Output Mappings of Tree Ensembles
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten. (Real-Time Systems Laboratory)
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten.ORCID-id: 0000-0002-1485-0802
2020 (Engelska)Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 194Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
2020. Vol. 194
Nyckelord [en]
Formal verification, Decision tree, Tree ensemble, Random forest, Gradient boosting machine
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:liu:diva-164563DOI: 10.1016/j.scico.2020.102450OAI: oai:DiVA.org:liu-164563DiVA, id: diva2:1416647
Forskningsfinansiär
Wallenberg AI, Autonomous Systems and Software Program (WASP)Tillgänglig från: 2020-03-24 Skapad: 2020-03-24 Senast uppdaterad: 2020-04-24

Open Access i DiVA

Publikationen är tillgänglig i fulltext från 2022-03-19 12:13
Tillgänglig från 2022-03-19 12:13

Övriga länkar

Förlagets fulltext

Personposter BETA

Törnblom, JohnNadjm-Tehrani, Simin

Sök vidare i DiVA

Av författaren/redaktören
Törnblom, JohnNadjm-Tehrani, Simin
Av organisationen
Programvara och systemTekniska fakulteten
I samma tidskrift
Science of Computer Programming
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 20 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf