树集成输入输出映射的形式化验证
机器学习
2020-03-24 v2 机器学习
摘要
机器学习和人工智能的最新进展正被考虑用于安全关键自主系统，其中软件缺陷可能对人类和环境造成严重危害。在这些领域中，当使用机器学习算法实现软件时，设计组织目前无法提供令人信服的论据证明其系统运行安全。本文中，我们提出一种从决策树和树集成中提取等价类，并形式化验证其输入输出映射是否符合要求的高效方法。其思想是，鉴于安全需求可追溯到系统输入输出模式上的期望属性，我们可在安全论证中使用正向验证结果。本文介绍了该方法在工具 VoTE（树集成验证器）中的实现，并基于现有文献中的两个案例研究评估了其可扩展性。我们证明，对于在低维数据上训练、至多 25 棵决策树且树深度至多 20 的树集成，我们的方法是实用的。我们的工作还研究了该方法在高维数据上的局限性，并初步探讨了树数量众多与验证耗时之间的权衡。
引用
@article{arxiv.1905.04194,
title = {Formal Verification of Input-Output Mappings of Tree Ensembles},
author = {John Törnblom and Simin Nadjm-Tehrani},
journal= {arXiv preprint arXiv:1905.04194},
year = {2020}
}