标题： 扩展XReason：对抗检测的形式化解释 显示英文标题

标题： Extending XReason: Formal Explanations for Adversarial Detection

摘要： 可解释的人工智能（XAI）在提高复杂机器学习模型的透明度和可靠性方面发挥着重要作用，特别是在网络安全等关键领域。 尽管启发式解释方法如SHAP和LIME广泛应用，但这些技术通常缺乏形式保证，可能会产生不一致的局部解释。 为了满足这一需求，一些使用形式方法提供形式解释的工具已经出现。 其中，XReason使用SAT求解器为XGBoost模型生成形式化的实例级解释。 在本文中，我们将XReason工具扩展以支持LightGBM模型以及类别级解释。 此外，我们在XReason中实现了一个机制来生成和检测对抗样本。 我们在CICIDS-2017数据集上评估了我们方法的效率和准确性，该数据集是检测网络攻击的常用基准。 显示英文摘要

摘要： Explainable Artificial Intelligence (XAI) plays an important role in improving the transparency and reliability of complex machine learning models, especially in critical domains such as cybersecurity. Despite the prevalence of heuristic interpretation methods such as SHAP and LIME, these techniques often lack formal guarantees and may produce inconsistent local explanations. To fulfill this need, few tools have emerged that use formal methods to provide formal explanations. Among these, XReason uses a SAT solver to generate formal instance-level explanation for XGBoost models. In this paper, we extend the XReason tool to support LightGBM models as well as class-level explanations. Additionally, we implement a mechanism to generate and detect adversarial examples in XReason. We evaluate the efficiency and accuracy of our approach on the CICIDS-2017 dataset, a widely used benchmark for detecting network attacks.