排序方式: 共有4条查询结果,搜索用时 0 毫秒
1
1.
随着机器学习在安全关键领域的应用愈加广泛,对于机器学习可解释性的要求也愈加提高.可解释性旨在帮助人们理解模型内部的运作原理以及决策依据,增加模型的可信度.然而,对于随机森林等机器学习模型的可解释性相关研究尚处于起步阶段.鉴于形式化方法严谨规范的特性以及近年来在机器学习领域的广泛应用,提出一种基于形式化和逻辑推理方法的机器学习可解释性方法,用于解释随机森林的预测结果.即将随机森林模型的决策过程编码为一阶逻辑公式,并以最小不满足核为核心,提供了关于特征重要性的局部解释以及反事实样本生成方法.多个公开数据集的实验结果显示,所提出的特征重要性度量方法具有较高的质量,所提出的反事实样本生成算法优于现有的先进算法;此外,从用户友好的角度出发,可根据基于反事实样本分析结果生成用户报告,在实际应用中,能够为用户改善自身情况提供建议. 相似文献
2.
如今,越来越多的社会决策借助机器学习模型给出,包括法律决策、财政决策等等.对于这些决策,算法的公平性是极为重要的.事实上,在这些环境中引入机器学习的目的之一,就是为了规避或减少人类在决策过程中存在的偏见.然而,数据集常常包含敏感特征,或可能存在历史性偏差,会使得机器学习算法产生带有偏见的模型.由于特征选择对基于树的模型具有重要性,它们容易受到敏感属性的影响.提出一种基于概率模型检查的方法,以形式化验证决策树和树集成模型的公平性.将公平性问题转换为概率验证问题,为算法模型构建PCSP#模型,并使用PAT模型检查工具求解,以不同定义的公平性度量衡量模型公平性.基于该方法开发了FairVerify工具,并在多个基于不同数据集和复合敏感属性的分类器上验证了不同的公平性度量,展现了较好的性能.与现有的基于分布的验证器相比,该方法具有更高的可扩展性和鲁棒性. 相似文献
3.
机载软件被广泛应用于航空航天领域, 大幅提升了机载设备的性能.但随着机载软件规模逐渐增大、功能逐渐增多, 给软件的开发带来了难度, 如何保障机载软件的正确性和安全性也成为一个难题.基于模型的开发可以有效提升开发效率, 而形式化方法能够有效保障软件的正确性.为了降低开发难度, 同时保障机载软件的正确性、安全性, 本文提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先使用SysML状态机图对机载软件的动态行为进行建模, 根据提出的精化规则, 对初始模型进行手动逐层精化得到精化设计模型.然后针对软件模型动态变化的特性, 将SysML状态机模型自动转换为时间自动机网络, 并从软件需求中手动提取形式化TCTL性质进行模型检验.其次, 为了实现编码自动化, 将SysML模型自动转换至Simulink, 利用Simulink Coder生成源代码.最后, 以一个自动飞行控制软件为例进行了开发和验证, 实验结果表明了该方法的有效性. 相似文献
4.
目前,核能装备等安全关键系统中软件的作用越来越重要,对系统的安全稳定运行具有至关重要的影响。安全关键软件规模的增长和复杂度的增加给设计和开发高可信的软件带来了新的挑战,亟需新的软件开发和验证方法与模式。针对此需求,本文围绕核能装备安全控制代码自动生成软件研究面临的三大关键科学问题,分别开展一个基础理论、七大关键技术及一套原型系统的研究。通过核能安全控制代码自动生成软件总体设计集成与评估、核能安全控制与交互系统软件建模技术、核能安全控制系统模型分析与验证技术、核能安全控制系统可信软件代码自动生成技术等方面的研究,突破核能装备安全控制代码自动生成软件在建模、代码生成和测试验证面临的系统性技术瓶颈,建立起新的安全关键软件开发和验证方法与模式。通过可信安全控制代码自动生成软件工程化应用与认证技术研究,构建一个核能装备安全控制代码自动生成的原型系统,并在核能、汽车等领域对研究成果进行验证。通过上述研究实现以下5个方面创新:一是形式化方法与模型驱动开发融合理论,用确定的数学理论保证模型的高可信;二是状态机扩展同步数据流语言形式化定义方法,建立适用于核能、航空、汽车等场景的软件建模方法;三是基于交互... 相似文献
1