VERDI 2025

AI for V&V
Chair: Peter Popov

Program Verification for Rigorous Analysis of Decision Tree Ensembles against Specifications

Iat Tou Leong, Aleksandar Avdalovic, Raul Barbosa

at  16:30in  VERDIfor  30min
As machine learning continues to integrate into critical systems, ensuring the reliability and correctness of these models becomes essential. Decision tree ensembles, which combine multiple decision trees to improve performance and robustness, present unique challenges for verification due to their complexity. This paper explores the application of theorem proving techniques for the formal verification of decision tree ensembles against specified requirements. Theorem proving can identify and mitigate potential specification violations, enhancing the trustworthiness and safety of machine learning ensembles. Two case studies and experimental results show the effectiveness of the approach, highlighting its potential to serve as a critical tool in the deployment of reliable machine learning systems. Moreover, the paper describes an evaluation of the complexity of the verification process, focusing on the computational considerations and feasibility of applying theorem proving to random forests.

 Overview  Program