Enhancing Framingham Cardiovascular Risk Score Transparency through Logic-Based XAI

1. Problem Statement

Cardiovascular disease (CVD) is a leading global cause of mortality. The Framingham Risk Score (FRS) is a widely adopted clinical tool used to predict a patient's 10-year risk of developing CVD based on factors like age, cholesterol, blood pressure, smoking, and diabetes.

However, the FRS suffers from a critical lack of transparency and interpretability:

• Opacity: It outputs a numerical score and a risk category (Low, Moderate, High) but does not explain why a specific patient was assigned that category.
• Lack of Actionability: It fails to indicate which specific modifiable factors a patient should change to lower their risk.
• Trust Issues: This "black box" nature can reduce clinician confidence and hinder the adoption of risk assessment tools, particularly in regions with limited access to specialists.

The authors propose a solution using Explainable Artificial Intelligence (XAI) grounded in First-Order Logic (FOL) to generate rigorous, actionable explanations for FRS classifications.

2. Methodology

The authors developed a logic-based explainer that avoids heuristic approximations, ensuring mathematical correctness.

A. Logical Framework

The system models the FRS calculation rules using Quantifier-Free First-Order Logic over Linear Rational Arithmetic (LRA).

• Formalization: Continuous variables (e.g., age, cholesterol) and Boolean variables (e.g., smoker status) are converted into logical implications. For example: 40 ≤ age < 45 → age_points = 5.
• Solver: The Z3 SMT (Satisfiability Modulo Theories) solver (via the z3py API) is used to encode the entire FRS logic, including point tables and risk thresholds.

B. Explanation Types

The system generates two complementary types of explanations based on logical entailment:

1. Abductive Explanations (Why?):

   • Goal: Identify the minimal sufficient set of features that logically entail the assigned risk category.
   • Method: The system iteratively removes features from the patient's profile. If the remaining features still logically entail the original risk category, the removed feature is deemed irrelevant. The remaining set constitutes the explanation.
   • Significance: Highlights the core drivers of the risk score, distinguishing between necessary and redundant factors.

2. Counterfactual Explanations (How to change?):

   • Goal: Identify the minimal set of changes to modifiable features required to shift the patient to a lower risk category (e.g., from High to Moderate).
   • Method: The system starts with an empty set of mutable features and incrementally adds them to a target state (e.g., "Low Risk"). If the conjunction of these changes and the target is satisfiable, it forms a valid counterfactual.
   • Significance: Provides actionable, prescriptive guidance for clinicians and patients.

C. Data Generation

To ensure exhaustive evaluation, the authors created a synthetic dataset covering all possible input combinations of the FRS.

• Scope: By discretizing continuous variables into the ranges defined by FRS guidelines, they generated 22,000 unique samples (covering both male and female profiles).
• Validation: The logic-based engine processed all 22,000 samples to generate explanations without approximation errors.

3. Key Contributions

1. Formal Correctness: Unlike many XAI methods that rely on statistical approximations (e.g., SHAP, LIME), this approach uses formal logic and SMT solving to guarantee that explanations are mathematically correct and consistent with the FRS rules.
2. Dual-Mode Explanation: The system uniquely combines abductive (justification) and counterfactual (intervention) reasoning within a single framework.
3. Actionable Insights: It explicitly separates immutable factors (age, sex) from modifiable ones (cholesterol, smoking), providing clear pathways for risk reduction.
4. Scalability: Demonstrated the ability to exhaustively process the entire FRS input space (22k samples) efficiently.

4. Results

The evaluation of the 22,000 synthetic samples yielded the following insights:

• Abductive Explanations (Justification):

  • Complexity: Explanations are rarely simple; 77% of them required five or more features to justify the risk category.
  • Dominant Factors: Age (98.2%) and Systolic Blood Pressure (92.4%) were the most frequent drivers of risk classification.
  • Modifiable vs. Immutable: While age and sex are foundational, modifiable factors (blood pressure, cholesterol, smoking) appeared in 50–75% of explanations, confirming their critical role in the final score.

• Counterfactual Explanations (Intervention):

  • Sparsity: These explanations are highly sparse. Over 80% required changing only one or two features to lower the risk category.
  • Key Levers: Systolic Blood Pressure (43.7%) and Total Cholesterol (42.1%) were the most effective single factors for changing a risk classification.
  • Irrelevance of Immutable Factors: Age and Sex appeared in 0% of counterfactual explanations, as they cannot be changed to lower risk.

5. Significance and Impact

• Clinical Trust: By converting opaque scores into transparent, logically verified insights, the system enhances clinician trust in the FRS model.
• Prescriptive Medicine: It moves beyond prediction to prescription, telling patients exactly what to change (e.g., "Lower SBP by 10mmHg") to achieve a safer risk profile.
• Accessibility: The tool is particularly valuable for areas with restricted access to specialists, as it automates the complex reasoning required to interpret risk scores and suggest interventions.
• Future Work: The authors suggest testing the system on real-world clinical datasets and refining the counterfactuals to suggest specific numerical target values for interventions.

In summary, this paper presents a robust, logic-based XAI framework that successfully demystifies the Framingham Risk Score, providing both a rigorous justification for current risk levels and a clear, mathematically sound roadmap for risk reduction.