Efficient and High-Quality Formal Verification for Decision Tree Ensembles
Saori Matsunaga, Genta Yoshimura · 2024
Given that the inference of machine learning models is inductive and typically operates as a complex black box, applying conventional software testing methods proves challenging. However, formal testing methods are essential for ensuring the quality of machine learning software. This study proposes a formal verification framework specially designed for decision-tree-based ensemble models, which rigorously verifies whether a model satisfies the expected verification properties and summarizes the verification results. The proposed method exhaustively enumerates verification violations by efficiently searching the input space corresponding to the verification properties and summarizes the violation regions, allowing for the appropriate addressing of discovered violations. Experimental results on four datasets across three tasks confirm that the proposed method completes the verification more efficiently than existing methods, with one case demonstrating a reduction in verification time by approximately 1000 times. Additionally, by introducing a metric to quantify the quality of violation regions, we verified that the proposed method presents violation regions more accurately than existing approaches. Furthermore, we conducted an experiment to illustrate that the proposed method can identify unexpected hazardous behaviors in the model.