如今越来越多的社会决策借助机器学习模型给出,包括法律决策、财政决策等等。对于这些决策,算法的公平性是极为重要的。事实上,在这些环境中引入机器学习的目的之一就是为了规避或减少人类在决策过程中存在的偏见。然而,数据集常常包含敏感特征,或可能存在历史性偏差,使得机器学习算法产生带有偏见的模型。树模型因为其高效、易于实现、泛化能力强等特性,被广泛地应用在各个领域的决策系统中。但由于其数据驱动以及对数据特征的依赖,很容易在模型中引入偏见元素,存在不公平性。现有的许多公平性验证和提升算法往往是从启发式角度出发,缺少形式化的保证,同时,针对树集成模型的群体公平性研究也是一个挑战。本文提出了一种基于概率模型检查的方法来形式化验证树模型的公平性。本文主要的工作和贡献如下:1.本文将公平性问题转化为概率验证问题,提出了一个基于概率模型检查的树模型公平性验证框架,可以通过不同定义的公平性度量对模型的公平性进行验证与度量。框架支持包括单棵决策树模型和树集成模型的验证。同时,能够处理多个复合敏感属性组合的场景。2.在验证框架的基础上,本文进一步研究了模型潜在公平性的发现与分析,从属性相关性和因果公平性等不同角度提供了对隐形歧视的验证与分析并对框架进行扩展,以便于适用于不同的需求和场景。3.本文对框架进行了工具实现,并在公平性常用的数据集上进行了实验,证明了框架的有效性和可行性。框架不仅能够对模型的公平性进行验证,同时还能评估公平性提升算法的效率。此外,相比于现有的公平性验证方法,框架在大规模模型上表现出不错的性能优势。