Jun 2026· Herald of Kazakh-British technical university· Vol 23, pp. 312-325· 0 citations· 3 references
TL;DR
This paper proposes a robust translation scheme that converts trained decision trees into logical constraints, enabling constraint inference that guarantees demographic parity and local robustness at prediction time and demonstrates that the constrained model effectively eliminates demographic parity violations.
Abstract
As Artificial Intelligence systems are increasingly deployed in safety-critical domains such as healthcare and finance, ensuring their trustworthiness and compliance is paramount. While Deep Neural Networks have received significant attention in formal verification, traditional models such as Decision Trees, often preferred for their interpretability, cannot inherently enforce constraints after training for fairness and stability. This paper presents a novel, comprehensive approach for the formal verification of Decision Tree classifiers using Satisfiability Modulo Theories (SMT). We propose a robust translation scheme that converts trained decision trees into logical constraints, enabling constraint inference that guarantees demographic parity and local robustness at prediction time. We implement this framework by using the z3 SMT solver and validate it on widely recognized fairness benchmarks, including UCI Adult, German Credit, and Loan Approval datasets. Experimental results demonstrate that our constrained model effectively eliminates demographic parity violations with a marginal accuracy trade-off of less than 0.2%. This approach transforms the SMT solver from a simple diagnostic tool into a provably fair inference engine suitable for regulated industries.
This survey highlights how optimization- and certification-oriented reasoning can provide a useful framework for reasoning about differences in models, supporting tasks ranging from model training and selection to auditing and certification.
Results indicate that global feature importance, used as an active search signal rather than a post-hoc diagnostic, improves both the effectiveness and the efficiency of individual fairness testing.
H. Mamman, Abdullateef Oluwagbemiga Balogun, Mustapha Maidawa et al.· Journal of King Saud Univers...· 0 citations
This paper introduces C LUE (Clustering and Experience-based Verification) , a training-free, non-parametric verifier that improves selection and reranking in Large Language Model outputs and finds that correct and incorrect solutions exhibit measurable geometric differences in their hidden-state trajectories.
Zhenwen Liang, Ruosen Li, Yujun Zhou et al.· Annual Meeting of the Associ...· 0 citations
Data-driven decision pipelines combining predictive machine learning models with downstream optimization software are increasingly used to make high-stakes operational decisions. Certifying the safety, fairness, and reliability of these decisions is essential, yet traditional scenario generation methods rely on repeated random testing, which becomes computationally prohibitive when failure events are rare and offers little insight into why failures occur. We present a framework for local violation certification designed specifically for linear decision pipelines under input uncertainty. We mathematically demonstrate that standard sampling methods fail efficiently for rare violations, motivating a direct structural approach. By analyzing the fixed decision boundary of a deployed pipeline, we show that the local risk of failure can be calculated directly in closed form using a single optimization solve. Furthermore, we introduce an exact sampling procedure and closed-form risk statistics that provide feature-level attributions (identifying which input characteristics contribute most to potential non-compliance) without requiring repetitive random trials or complex sampling algorithms. We demonstrate our approach on an economic power dispatch system subject to emissions regulations, delivering precise, auditable risk assessments at a fraction of the traditional computational cost.
LLM benchmark scores can be precise even when the observation protocol does not identify the behavioral property they are intended to measure. In a controlled, solver-grounded setting, we formalize a protocol-level identifiability audit over a finite behavioral policy class: given policies H, observation support O, and estimand $\tau$, we test whether O separates every pair with different $\tau$. The audit requires zero model calls and resolves our diagnostic case: base-only observation collapses seven frozen deterministic policies into one equivalence class; full support yields seven classes and no cross-estimand collisions; every leave-one-out support retains a constructive collision witness. Empirically, both constrained-generation variants have pair-validity 1.0, yet base accuracy and selective-response fidelity diverge - 0.620 versus 0.324 across six balanced oracle-transition directions (cluster-bootstrap 95% CI [0.600, 0.642] vs. [0.304, 0.345]) - and the gap recurs on a second deterministic source (0.646 vs. 0.331). The audit also synthesizes a minimum identifying support $O^*$ for the frozen policy class: two cells instead of the full 36-cell tensor. This case shows how evaluation-design validity can be checked structurally before model inference and why base correctness does not determine intervention-response fidelity.
Fairness in machine learning (ML) and deep learning (DL) systems is becoming increasingly important because algorithmic decisions start to have a considerable influence on the governance of some high-stakes domains, making unfairness detection and testing crucial. Despite notable progress, existing automated fairness testing approaches remain limited by static fairness definitions, single-objective optimization, and restricted adaptability across models and datasets. This study addresses these limitations by proposing a Genetic Algorithm–based Test Case Generation (GATCG) framework that combines knowledge-based reasoning with multi-objective evolutionary optimization to reveal unfair behavior dynamically. Our approach comprises a Fairness Knowledge Base (FKB) that formally encodes fairness concepts through logical rules and semantic networks, thereby enabling explicit analysis of the relationships between protected attributes, fairness metrics, and constraints. This knowledge-driven foundation is tightly integrated with a multi-objective genetic algorithm that evolves test cases via selection, crossover, and mutation while simultaneously optimizing disparate impact, disparate treatment, and disparate mistreatment. By combining structured fairness reasoning with evolutionary search, the proposed approach extends beyond single-metric detection to include automatic and adaptable fairness testing. Experiments conducted on benchmark datasets (Adult Income and German Credit) using a Multi-Layer Perceptron (MLP) classifier as the underlying model demonstrate that GATCG achieves lower discrimination sample search time and higher detection success rates compared to baseline approaches (ExpGA, AEQUITAS, SG and ADF). Prior to introducing the uniqueness-tracking mechanism, GATCG demonstrated strong effectiveness by reducing discriminatory sample search time (DSS) by 35%, increasing the number of discovered discriminatory samples (DSN) by 22%, expanding test sample generation (TSN) by 8%, and improving the success rate (SUR) by 9% compared to baseline approaches. To provide a more accurate assessment of the approach, a uniqueness-tracking mechanism and a one-per-generation rule were subsequently incorporated to eliminate duplicate discriminatory discoveries. Under this enhanced evaluation setting, GATCG achieved overall success rates (SUR) of 61.85% on the Adult Income dataset and 68.17% on the German Credit dataset. The results indicate that GATCG efficiently directs the search toward unique discrimination-prone regions of the input space, leading to improved detection speed, more effective identification of biased samples, higher-quality test generation, and strong discriminatory sample discovery performance. Finally, we conduct a controlled experiment that demonstrates GATCG’s superiority over THEMIS and manual testing with respect to unfairness detection effectiveness, usability, coverage, and testing efficiency.