近年来,机器学习因其优越的计算能力,在安全领域展现出了巨大的发展前景。与此同时,机器学习的可解释性问题也成为了人们所重点关注的问题,可解释性能够揭示机器学习的决策原理,增强其可靠性,帮助模型优化,具有很大的意义。然而,目前大部分可解释性方法仍视机器学习模型为黑盒模型,并未深入其内部进行分析,具有较大的局限性。树模型因其非线性结构,较神经网络模型更加难以分析,鲜少有针对树模型的可解释性分析,因此,针对树模型的可解释性分析也是一个巨大的挑战。形式化方法因其严谨的逻辑特性,在机器学习性质验证方面得到了大范围的应用。鉴于此,本文基于形式化方法,提出了针对随机森林模型的局部可解释性问题的研究方法,主要针对样本特征重要性和反事实样本生成这两个方面。具体而言,文中的三个贡献如下:1.本文提出了基于可满足性模理论的随机森林决策过程编码方法,以此能够较为直观地了解随机森林的内部运行方式。2.本文提出了基于最小不满足核的溯因解释这一概念。利用可满足性模理论求解器对编码的随机森林决策公式进行分析求解,根据经计算后提供的最小不满足核,以反映在决策过程中对样本的预测结果有重要性影响的特征。实验结果表明了使用形式化方法深入分析模型可解释问题的可行性和精确性。3.本文提出了基于最小不满足核的最优反事实样本生成方法,为反事实分析提供了新的思路。实验结果证明了优越的性能和良好的结果。本文采用真实的贷款数据集进行了案例分析,为贷款失败的用户提供了合适且易于实现的建议,即根据反事实样本改善用户的申请条件,使得下一次贷款成功,以展示其在现实中的实用性。基于形式化方法的可解释性方法能够深入模型内部进行分析,以此为黑盒模型的解析引入了新的视角。同时,本文对于可满足性模理论中的最小不满足核赋予了新的价值,即能够根据最小不满足核,从两个不同的角度对机器学习的可解释性进行研究和讨论,给可解释性领域提供了一套新型实用的可解释性方法。