Paper deep dive
Formal Abductive Explanations for Navigating Mental Health Help-Seeking and Diversity in Tech Workplaces
Belona Sonna, Alain Momo, Alban Grastien
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%
Last extracted: 3/22/2026, 5:04:27 AM
Summary
This paper introduces a formal abductive explanation (AXP) framework to interpret AI-driven mental health help-seeking predictions in tech workplaces. By converting neural network models into SMT formulas, the authors compute minimal sufficient reasons for individual predictions, enabling bias assessment regarding sensitive attributes like gender and identifying critical feature combinations that influence clinical outcomes.
Entities (5)
Relation Signals (3)
Formal Abductive Explanation Framework → usedon → Mental Health in Tech Survey
confidence 98% · We leverage the Mental Health in Tech Survey dataset... to establish the following contributions
Formal Abductive Explanation Framework → appliedto → Neural Network
confidence 95% · The trained neural network is then converted into an SMT formula, which serves as the basis for computing abductive explanations
Gender → influences → Neural Network
confidence 90% · we explicitly examine the influence of sensitive attributes such as gender on model decisions
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:This work proposes a formal abductive explanation framework designed to systematically uncover rationales underlying AI predictions of mental health help-seeking within tech workplace settings. By computing rigorous justifications for model outputs, this approach enables principled selection of models tailored to distinct psychiatric profiles and underpins ethically robust recourse planning. Beyond moving past ad-hoc interpretability, we explicitly examine the influence of sensitive attributes such as gender on model decisions, a critical component for fairness assessments. In doing so, it aligns explanatory insights with the complex landscape of workplace mental health, ultimately supporting trustworthy deployment and targeted interventions.
Tags
Links
- Source: https://arxiv.org/abs/2603.14007v1
- Canonical: https://arxiv.org/abs/2603.14007v1
Trouble viewing inline? Open PDF directly →
Full Text
24,033 characters extracted from source content.
Expand or collapse full text
Formal Abductive Explanations for Navigating Mental Health Help-Seeking and Diversity in Tech Workplaces Belona Sonna1 Alain Momo2 Alban Grastien1 1Australian National University 2Australian Reinforcing Company belona.sonna@anu.edu.au, momoalain0505@gmail.com, alban.grastien@anu.edu.au Abstract This work proposes a formal abductive explanation framework designed to systematically uncover rationales underlying AI predictions of mental health help-seeking within tech workplace settings. By computing rigorous justifications for model outputs, this approach enables principled selection of models tailored to distinct psychiatric profiles and underpins ethically robust recourse planning. Beyond moving past ad-hoc interpretability, we explicitly examine the influence of sensitive attributes such as gender on model decisions, a critical component for fairness assessments. In doing so, it aligns explanatory insights with the complex landscape of workplace mental health, ultimately supporting trustworthy deployment and targeted interventions 1 Introduction The global burden of mental health disorders is immense, affecting over 970 million people worldwide and posing substantial social and economic challenges (Gupta and others, 2024). In workplace contexts, mental health concerns ranging from depression and anxiety to stress-related disorders are particularly prevalent, yet often underreported and undertreated due to stigma or lack of structural support (Jin et al., 2023). As organizations increasingly turn to AI to predict, monitor, or support mental health interventions, critical questions arise about the appropriateness and trustworthiness of such systems (Ali and others, 2024; Taylor and others, 2025). Recent studies underscore the promise of AI models in detecting early signs of psychiatric distress (Gupta and others, 2024), enhancing access in resource-limited settings (Kumar and others, 2024), and tailoring interventions (Doraiswamy and others, 2019). However, these benefits are tempered by concerns over algorithmic bias, lack of transparency, and the mismatch between predictive patterns and clinical reality (Stefanis and others, 2024; Zhu and others, 2024). Importantly, mental health is not a uniform concept but a heterogeneous collection of conditions, each influenced by distinct psychosocial and occupational factors (Omar and others, 2024). This heterogeneity means that the same AI model may rely on very different reasons to predict help-seeking across individuals. Thus, there is a pressing need for methodologies that do not merely interpret model outputs but formally justify why a particular model is suitable (or unsuitable) for specific mental health contexts, ensuring ethically sound, clinically relevant, and personalized care pathways. 2 Problem Statement and Hypothesis Despite the growing use of AI in predicting mental health outcomes in workplace settings, there remains a critical gap in formally understanding why models make specific treatment-related predictions, particularly given the diverse manifestations of mental health conditions. Existing interpretability approaches often yield fragmented or heuristic insights, which are insufficient for assessing whether an AI model’s reasoning genuinely aligns with the multifaceted nature of psychiatric disorders. This lack of structured, auditable justification complicates efforts to ensure ethical deployment, appropriate intervention planning, and sustained clinician trust We hypothesize that the use of formal abductive explanations can help bridge this gap by systematically uncovering minimal, context-specific reasons that drive model predictions. This, in turn, will reveal the heterogeneity of factors influencing help-seeking across different mental health contexts and enable principled selection of AI models best suited to distinct psychiatric needs, thereby enhancing both transparency and clinical relevance. Although this work is preliminary, we conducted an empirical study on the Mental Health in Tech Survey dataset to establish the following contributions: 1. Train a neural network as a baseline predictive model for help-seeking behavior. 2. Compute formal abductive explanations to systematically uncover the reasons behind each decision of the trained network. 3. Leverage these explanations to assess potential bias, particularly with respect to sensitive attribute such as gender. 4. Analyze the impact of each feature on the outcome of the neural network. 5. Identify the most prominent combinations of features that are likely to trigger predictions of seeking treatment or not. 3 Preliminaries To ensure clarity, we first introduce the formal notation, the dataset and the decision process used throughout this paper. 3.1 Notation • V=v1,…,vnV=\v_1,…,v_n\ denotes a set of n Boolean variables (features). • An individual x=[x1,…,xn]x=[x_1,…,x_n] is represented as a vector of Boolean values corresponding to the features in V. We interpret x both as a vector and as a conjunction (or set) of literals, where each x[i]x[i] is either viv_i or ¬vi v_i. • X denotes the space of all possible individuals. • D is the domain of the decision function, with d∈Dd∈ D. • Δ:X→D :X→ D is the decision function computed by the model. • XPXP is a property of an individual x, defined as a subset (i.e., conjunction) of literals from x, such that XP⊆xXP x. We denote by vars(XP)vars(XP) the set of features that appear in XPXP. • p∈Vp∈ V denotes the protected attribute. • X(V′)xX_(V )^x denotes the set of individuals that are identical to x except (potentially) on the subset of features V′⊆V V. 3.2 Dataset We leverage the Mental Health in Tech Survey dataset, which captures demographic, occupational, and mental health-related attributes of individuals in the tech industry, along with self-reported treatment-seeking behavior. The dataset comprises 1,257 instances, with 78.84% identifying as male and 21.16% as female or transgender. Among the respondents, 635 reported having sought treatment, while 622 did not. For simplicity, we binarized the dataset (X) according to the procedure described in Appendix A.1. 3.3 The Decision process In this paper, We have trained a feedforward neural network with slkearn-library to predict whether an individual seeks mental health treatment. The resulting model achieves an accuracy of 74%, with additional details and the full classification report provided in Appendix A.2. Then the trained model has been converted as a SMT model following the listed steps: • Extract the model’s weights and structure: input weights matrix, bias vector, activation function and the output layer. • Express each neuron as a linear formula using the weights and the bias term • Write similar formulas for all hidden neurons and then for the output neuron. • Combine them into a full logical expression that will be the decision function (Δ ) of the model. 4 What is formal Abductive explanations? Formal abductive explanations (AXPs) have been extensively studied in works such as Darwiche (2020); Huang and Marques-Silva (2023); Izza et al. (2023); Marques-Silva (2022, 2023); Marques-Silva and Ignatiev (2022), where an AXP is defined as follows: Definition 1. A formal abductive explanation (AXP) is a minimal set of features of an individual that is sufficient to guarantee the same decision by the model. Any individual sharing identical values on this minimal set of features will necessarily receive the same prediction. Algorithm 1 computes a minimal abductive explanation for an individual x. The algorithm operates greedily: it attempts to remove each literal from x and retains only those whose removal changes the outcome, thereby preserving minimal sufficiency. Algorithm 1 Compute-Explanation Input: Decision process Δ Input: Individual x Input: Decision d=Δ(x)d= (x) Output: XPXP, a minimal abductive explanation for x 1: XP←xXP← x 2: for each feature v∈Vv∈ V do 3: ℓ←x[v] ← x[v] 4: XP←XP∖ℓXP← XP \ \ 5: if ∃x′⊇XP∃ x XP such that Δ(x′)≠d (x )≠ d then 6: XP←XP∪ℓXP← XP∪\ \ 7: end if 8: end for 9: return XPXP Example 1. Let us compute a minimal abductive explanation for the decision of an individual represented by the feature vector x=[1,1,0,1,1,0,1,1,1,0,0,0,0,0,0,1,1,0,0],x=[1,1,0,1,1,0,1,1,1,0,0,0,0,0,0,1,1,0,0], Table 1: Computing an explanation for individual [1,1,0,1,1,0,1,1,1,0,0,0,0,0,0,1,1,0,0][1,1,0,1,1,0,1,1,1,0,0,0,0,0,0,1,1,0,0] Steps x0x_0 x1x_1 x2x_2 x3x_3 x4x_4 x5x_5 x6x_6 x7x_7 x8x_8 x9x_9 x10x_10 x11x_11 x12x_12 x13x_13 x14x_14 x15x_15 x16x_16 x17x_17 x18x_18 ∃x′∃ x 1 ? 1 0 1 1 0 1 1 1 0 0 0 0 0 0 1 1 0 0 ⊥ 2 ? ? 0 1 1 0 1 1 1 0 0 0 0 0 0 1 1 0 0 ⊥ 3 ? ? ? 1 1 0 1 1 1 0 0 0 0 0 0 1 1 0 0 ⊥ 4 ? ? ? ? 1 0 1 1 1 0 0 0 0 0 0 1 1 0 0 ⊤ 5 ? ? ? 1 ? 0 1 1 1 0 0 0 0 0 0 1 1 0 0 ⊥ 6 ? ? ? 1 ? ? 1 1 1 0 0 0 0 0 0 1 1 0 0 ⊥ 7 ? ? ? 1 ? ? ? 1 1 0 0 0 0 0 0 1 1 0 0 ⊥ 8 ? ? ? 1 ? ? ? ? 1 0 0 0 0 0 0 1 1 0 0 ⊤ 9 ? ? ? 1 ? ? ? 1 ? 0 0 0 0 0 0 1 1 0 0 ⊥ 10 ? ? ? 1 ? ? ? 1 ? ? 0 0 0 0 0 1 1 0 0 ⊤ 11 ? ? ? 1 ? ? ? 1 ? 0 ? 0 0 0 0 1 1 0 0 ⊤ 12 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 0 0 1 1 0 0 ⊥ 13 ? ? ? 1 ? ? ? 1 ? 0 0 ? ? 0 0 1 1 0 0 ⊤ 14 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? 0 1 1 0 0 ⊥ 15 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? ? 1 1 0 0 ⊥ 16 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? ? ? 1 0 0 ⊤ 17 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? ? 1 ? 0 0 ⊤ 18 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? ? 1 1 ? 0 ⊥ 19 ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? ? 1 1 ? ? ⊤ final ? ? ? 1 ? ? ? 1 ? 0 0 ? 0 ? ? 1 1 ? 0 Algorithm 1 is illustrated on Table 1. The explanation process follows the steps outlined in table 1, which iteratively checks the necessity of each feature with respect to the decision. In the first step (first row), the algorithm verifies whether feature x0x_0 is necessary by checking whether there exists an alternative input x′x , identical to x except for the value of x0x_0, such that the decision remains unchanged. Since the check is negative (denoted by ⊥ in the column ∃x′∃ x ), this indicates that x0x_0 is not necessary for the decision. As a result, its value is permanently removed for the remainder of the computation. In the second step, the algorithm evaluates whether x1x_1 is necessary and again obtains a negative result (⊥ ). Hence, x1x_1 is also removed. In contrast, Step 4 checks whether x3x_3 is necessary to reach the decision, and this time the result is positive (denoted by ⊤ in the column ∃x′∃ x ), indicating that x3x_3 is necessary. Consequently, its value is reintroduced in Step 5. The algorithm proceeds similarly for the remaining features, testing each one to determine whether it is necessary for preserving the decision outcome, and retaining only those features that are found to be necessary. The final row contains the minimal explanation XPXP. XP=x3∧x7∧¬x9∧¬x10∧¬x12∧x15∧x16∧¬x18.XP=\x_3 x_7 x_9 x_10 x_12 x_15 x_16 x_18\. This means that the specific values of the features in XPXP are sufficient to entail the outcome. Consequently, any other individual who shares these values on the features indexed by XPXP will also be predicted to seek treatment. To express XPXP in human-understandable terms, refer to Appendix B.1. 5 Methodology and Results 5.1 Bias assessment in the model As mentioned previously, AXPsAXPs can also be employed to assess whether an individual decision exhibits bias. Following the definition in Darwiche (2020), a decision is considered biased if all its abductive explanations necessarily include a sensitive or protected attribute. In addition, the model is considered as biased if it admits at least one biased decision. We apply this notion to evaluate bias in our trained model. More formally, the algorithm to make that check is to constraint the algorithm 1 to generate an explanation without the protected feature. If such an explanation exists, the decision is considered unbiased with respect to that feature. Otherwise, the decision is deemed biased. In the context of the Mental Health in Tech Survey dataset, the feature Gender is treated as a protected attribute, encoded as 11 for Male and 0 for Non-Male (Female or Trans). Accordingly, for each individual in the dataset, we examine whether there exists at least one AXPAXP that does not involve the Gender feature. If no such explanation exists,meaning that all minimal sufficient explanations include Gender: the decision is deemed biased. Table 2: Individual bias in the decision making process Unbiased decisions Negative Positive 864 290 103 Table 2 indicates that although the model exhibits bias since it produces at least one biased decision, the majority of individual decisions (68.73%) are in fact unbiased. This result highlights another strength of the abductive approach: it enables precise identification of the specific individuals affected by bias, thereby facilitating targeted mitigation strategies. Another notable finding is that the feature Gender leads to a greater number of biased decisions associated with negative outcomes (290) compared to positive ones (103). Example 2. The individual at index 11, who is predicted not to seek treatment, constitutes a biased decision under our framework, as there does not exist an abductive explanation for this prediction that excludes the protected feature Gender. 5.2 Impact of features on the model output In this section, we examine the impact of each feature on the model’s predictions by extending our earlier analysis of the sensitive attribute Gender. For each feature, we check whether there exists at least one abductive explanation for each decision that excludes it. If no such explanation exists, we deem the feature critical for that prediction. A comprehensive summary of the impact of each feature is provided in table 3. Table 3: Influence of features on the model outputs Features Non influenced Negative Positive x0x_0 1027 113 117 x1x_1 864 290 103 x2x_2 1065 107 85 x3x_3 630 422 205 x4x_4 1126 59 72 x5x_5 1109 81 67 x6x_6 1122 65 70 x7x_7 919 268 70 x8x_8 1075 76 106 x9x_9 1038 72 147 x10x_10 1017 71 169 x11x_11 910 217 130 x12x_12 1032 117 108 x13x_13 1019 172 66 x14x_14 964 221 72 x15x_15 888 92 277 x16x_16 1026 151 80 x17x_17 1138 56 63 x18x_18 896 273 88 It emerges that the most critical feature contributing to predictions of individuals not seeking treatment is feature x3x_3, which is indispensable in 422 decisions. This accounts for approximately 34%34\% of all cases and specifically 69.1%69.1\% of the instances predicted as not seeking treatment. Conversely, the most critical feature influencing predictions of individuals seeking treatment is feature x15x_15, appearing as critical in 277 decisions, or about 22%22\% of all cases and 42.8%42.8\% of the instances predicted as having sought treatment. 5.3 The most critical combinations that impact model’s outputs In Table 4, we have seected the five most critical features for each category of model outputs and highlight the most prominent feature combinations associated with each outcome. Notably, the combination (x1∧x15)(x_1 x_15) appears in all abductive explanations of 105 instances, accounting for 16.2%16.2\% of the cases predicted as seeking treatment and 8.3%8.3\% in the whole dataset. For the category of individuals predicted not to seek treatment, the combination (x3∧x11∧x18)(x_3 x_11 x_18) appears in 134 instances, representing 21.9%21.9\% of such predictions. Additional critical combinations are detailed in Table 4. Table 4: Critical combinations of features Outcomes Combinations Ratio Whole Specific Negative x3∧x14∧x18x_3 x_14 x_18 9.3% 19.1% x3∧x11∧x18x_3 x_11 x_18 10.6% 21.9% x1∧x14∧x18x_1 x_14 x_18 8.5% 17.5% x1∧x3∧x18x_1 x_3 x_18 10.5% 21.8% x1∧x3∧x14x_1 x_3 x_14 8.9% 18.5% Positive x3∧x15x_3 x_15 8.3% 16.23% x9∧x15x_9 x_15 7% 13.6% z9∧x10z_9 x_10 7% 13.6% 6 Guiding Model Selection and Recourse By aggregating abductive explanations across individuals and comparing them to established clinical insights (Stefanis and others, 2024; Ali and others, 2024), we can formally evaluate which models best reflect expected psychiatric patterns. This facilitates selecting the most appropriate model for specific mental health applications such as stress versus depression and guides recourse strategies by ensuring interventions target the true factors driving predictions. Conclusion This work introduces a formal abductive reasoning framework to interpret and audit mental health-related decisions in tech workplaces. By computing abductive explanations for each model prediction, we identify the critical features and combinations of factors that drive help-seeking behavior. This not only enables clinicians and practitioners to select models that align more closely with psychiatric understanding, but also supports the design of meaningful recourse strategies. Importantly, our method exposes potential bias in the decision processes by revealing the predictions that are sensitive to protected attributes. While some of this bias may reflect real-world asymmetries in mental health (e.g., gender-specific vulnerabilities like post-partum depression), our findings call for careful scrutiny to distinguish beneficial personalization from harmful discrimination. Our results have significant implications for shaping workplace mental health policies and advancing Responsible AI practices. By promoting transparency and trust, we pave the way for ethical, explainable, and fairer AI-driven systems in high-stakes domains. This study is limited to binary features; extending the approach to continuous or mixed-type data remains a compelling direction for future work. Additionally, assessing how fairness metrics evolve under abductive explanations could further deepen our understanding of model accountability. Mental health challenges affect people of all ages, genders, and geographies. It is therefore vital to develop reliable and interpretable AI systems that empower individuals, inform policy, and ultimately foster more inclusive and supportive work environments. References S. Ali et al. (2024) Generative artificial intelligence in mental healthcare: an ethical overview. Current Treatment Options in Psychiatry 11 (2), p. 145–158. External Links: Document, Link Cited by: §1, §6. A. Darwiche (2020) On the reasons behind decisions. Proceedings of the AAAI Conference on Artificial Intelligence 34 (04), p. 2930–2937. Cited by: §4, §5.1. P. M. Doraiswamy et al. (2019) Artificial intelligence and the future of psychiatry: insights from a global physician survey. arXiv preprint arXiv:1907.12386. External Links: Link Cited by: §1. R. Gupta et al. (2024) Exploring the role of artificial intelligence in mental healthcare: current trends and future directions—a narrative review. Risk Management and Healthcare Policy 17, p. 1339–1348. External Links: Document, Link Cited by: §1, §1. X. Huang and J. Marques-Silva (2023) From robustness to explainability and back again. CoRR abs/2306.03048. External Links: Link, Document, 2306.03048 Cited by: §4. Y. Izza, A. Ignatiev, P. J. Stuckey, and J. Marques-Silva (2023) Delivering inflated explanations. ArXiv abs/2306.15272. External Links: Link Cited by: §4. K. W. Jin, Q. Li, Y. Xie, and G. Xiao (2023) Artificial intelligence in mental healthcare: an overview and future perspectives. British Journal of Radiology 96 (1150), p. 20230213. External Links: Document, Link Cited by: §1. A. Kumar et al. (2024) Artificial intelligence in mental healthcare: an overview and future directions. Global Medical Discovery 4, p. 100099. External Links: Document, Link Cited by: §1. J. Marques-Silva and A. Ignatiev (2022) Delivering trustworthy ai through formal xai. Proceedings of the AAAI Conference on Artificial Intelligence. Cited by: §4. J. Marques-Silva (2022) Logic-based explainability in machine learning. ArXiv abs/2211.00541. External Links: Link Cited by: §4. J. Marques-Silva (2023) Disproving XAI myths with formal methods – initial results. 27th International Conference on Engineering of Complex Computer Systems (ICECCS), p. 12–21. External Links: Link Cited by: §4. M. Omar et al. (2024) Bias and risk in mental health ai decision making. arXiv preprint arXiv:2405.12345. External Links: Link Cited by: §1. N. C. Stefanis et al. (2024) Artificial intelligence in psychiatry: present trends and challenges. International Journal of Neuropsychopharmacology 28 (Suppl 1), p. i213. External Links: Document, Link Cited by: §1, §6. K. Taylor et al. (2025) AI for mental health: clinician expectations and priorities in computational psychiatry. BMC Psychiatry 25, p. 69. External Links: Document, Link Cited by: §1. F. Zhu et al. (2024) Risks from language models for automated mental healthcare: ethics and structure for implementation. arXiv preprint arXiv:2406.11852. External Links: Link Cited by: §1. Appendix A Dataset and Model A.1 Dataset processing This section lists the features used from the Mental Health in Tech Survey dataset and describes how each was binarized. • feature x0x_0: Is the applicant older than 31? 11 if yes, 0 otherwise. • feature x1x_1: Is the applicant male? 11 if yes, 0 otherwise. • feature x2x_2: Is the applicant self-employed? • feature x3x_3: Family history of mental health issues? • feature x4x_4: Works with a small number of people? • feature x5x_5: Works remotely? • feature x6x_6: Works in a tech company? • feature x7x_7: Aware of provided benefits? • feature x8x_8: Aware of care options? • feature x9x_9: Aware of employee wellness programs? • feature x10x_10: Knows how to seek help? • feature x11x_11: Is anonymity protected if using mental health resources? • feature x12x_12: Is it easy to take medical leave for mental health? • feature x13x_13: Believes discussing mental health with employer has negative consequences? • feature x14x_14: Believes discussing physical health with employer has negative consequences? • feature x15x_15: Comfortable discussing mental health with coworkers? • feature x16x_16: Comfortable discussing mental health with supervisors? • feature x17x_17: Believes employer treats mental health as seriously as physical health? • feature x18x_18: Has observed negative consequences for coworkers with mental health conditions? A.2 Model training and conversion The decision process is implemented as a single-layer neural network, whose properties and performance are summarized in Figure 1. Figure 1: Classification report of the trained model. The trained neural network is then converted into an SMT formula, which serves as the basis for computing abductive explanations via constraint programming. Appendix B Formal abductive explanations B.1 Computation XP=x3∧x7∧¬x9∧¬x10∧¬x12∧x15∧x16∧¬x18.XP=\x_3 x_7 x_9 x_10 x_12 x_15 x_16 x_18\. This means individual 55 is predicted to seek treatment because: • x3=1x_3=1: has a family history of mental health issues, • x7=1x_7=1: knows the benefits provided, • x9=0x_9=0: does not know about the wellness program, • x10=0x_10=0: does not know how to seek help at the workplace, • x12=0x_12=0: it is not easy to take leave for mental health conditions, • x15=1x_15=1: could discuss mental health with some coworkers, • x16=1x_16=1: could discuss mental health with a supervisor, • x18=0x_18=0: has not observed negative consequences for coworkers with mental health conditions.