An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles
An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles
复制标题
DOI：
10.1007/978-3-030-26250-1_24
复制
发表时间：
2019-09
期刊：
影响因子：
--
通讯作者：
John Törnblom;S. Nadjm-Tehrani
中科院分区：
文献类型：
--
作者：
John Törnblom;S. Nadjm-Tehrani
机器学习的最新进展正在考虑集成到安全关键系统中，如车辆，医疗设备和关键基础设施。然而，在这些领域的组织目前无法提供令人信服的论据，系统集成机器学习技术是安全的，在他们的预期environments.In本文中，我们提出了一个正式的验证方法树合奏，利用抽象细化的方法来抵消组合爆炸。我们实现的方法作为一个名为投票的工具的扩展，并证明其适用性，通过验证的鲁棒性对扰动的随机森林和梯度增强机在两个案例研究。我们对VoTE的基于抽象细化的扩展将性能提高了几个数量级，扩展到树集合，最多有50棵树，深度为10，在高维数据上进行训练。
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.