Decoding Heart Risk: A Logic-Based Approach to Explainable AI

by

Author: Denis Avetisyan

Researchers are leveraging the power of formal logic to make cardiovascular risk assessments more transparent and understandable.

This work introduces a framework using First-Order Logic and SMT solvers to generate abductive and counterfactual explanations for the Framingham Risk Score.

Despite the widespread use of the Framingham Risk Score (FRS) for cardiovascular disease (CVD) assessment, its opacity hinders clinical trust and targeted intervention. This work, ‘Enhancing Framingham Cardiovascular Risk Score Transparency through Logic-Based XAI’, addresses this limitation by introducing a novel framework leveraging first-order logic and Satisfiability Modulo Theories (SMT) solvers to generate transparent explanations for FRS predictions. Our approach identifies minimal sets of risk factors driving a patient’s classification and proposes actionable scenarios for risk reduction, validated across over 22,000 FRS input combinations. Could this logic-based explainer facilitate broader adoption of CVD risk assessment, particularly in resource-constrained settings, by converting opaque scores into prescriptive insights?

The Inevitable Cascade: Forecasting Cardiac Risk

Cardiovascular disease persistently represents a significant global health challenge, accounting for approximately one in three deaths worldwide. This staggering statistic underscores the critical need for proactive identification of individuals at elevated risk, enabling timely interventions and potentially preventing life-threatening events like heart attacks and strokes. Accurate risk prediction isn’t merely about identifying those already affected; it’s about forecasting future cardiac events, allowing for preventative lifestyle changes, medication, or closer monitoring. Consequently, substantial research has focused on developing and refining tools capable of estimating an individual’s probability of developing cardiovascular disease, moving beyond simply reacting to symptoms and towards a more predictive and preventative model of care. The pursuit of these tools isn’t just a scientific endeavor, but a public health imperative, aiming to reduce the immense personal and economic burden imposed by heart disease.

The Framingham Heart Study, a landmark longitudinal investigation initiated in 1948, meticulously tracked residents of Framingham, Massachusetts, to identify factors contributing to cardiovascular disease. Through decades of data collection and analysis, researchers pinpointed several key risk factors, including high blood pressure, elevated cholesterol levels, smoking, and age. These findings didn’t just illuminate the causes of heart disease; they formed the basis of the Framingham Risk Score, a widely adopted clinical tool for estimating an individual’s 10-year risk of developing cardiovascular events. This score, calculated from easily obtainable patient data, allows healthcare professionals to proactively identify individuals who would benefit most from preventative measures and lifestyle interventions, representing a pivotal advance in cardiovascular health management and a testament to the study’s enduring legacy.

Despite its proven efficacy in estimating cardiovascular risk, the Framingham Risk Score often functions as a ‘black box’ for clinicians. The score generates a percentage likelihood of heart disease within a specified timeframe, but the underlying calculations – weighting various factors like cholesterol, blood pressure, and age – remain opaque. This lack of transparency hinders a physician’s ability to fully explain the score to a patient, fostering distrust or reluctance to adhere to preventative measures. Furthermore, the score’s limited interpretability complicates individualized treatment plans; a high score doesn’t pinpoint which risk factor contributes most significantly, leaving doctors to rely on standard protocols rather than targeted interventions. Addressing this ‘black box’ issue through more explainable AI models could substantially improve both patient engagement and the precision of cardiovascular care.

Formalizing the Trajectory: Logic and Linear Rationality

First-Order Logic (FOL) enables the precise articulation of the Framingham Risk Score’s conditional rules. The score, traditionally expressed as a set of if-then statements relating risk factors to probability of cardiovascular events, is translated into FOL predicates and quantifiers. Specifically, variables represent patient attributes – age, cholesterol level, blood pressure, and smoking status – and predicates define relationships between these attributes and risk categories. Logical connectives such as conjunction ( \land ), disjunction ( \lor ), and implication (→) model the scoring algorithm’s decision-making process. This formalization allows for unambiguous representation of the score’s logic, facilitating automated verification, sensitivity analysis, and the development of explainable AI systems for cardiovascular risk assessment.

The Framingham Risk Score incorporates continuous variables such as cholesterol and blood pressure, necessitating the use of Linear Rational Arithmetic (LRA) within its formalization. LRA extends First-Order Logic to accommodate real-valued numbers and linear inequalities. This allows for the precise representation of risk factor thresholds and their contributions to the overall score; for example, a statement like “ cholesterol > 240 \implies risk\_increase = 0.05 ” can be formally expressed. Without LRA, these continuous variables would require discretization, potentially introducing inaccuracies and losing the granularity of the original scoring system. The use of LRA ensures that the formal model accurately reflects the quantitative relationships defined by the Framingham Risk Score.

Formalizing the Framingham Risk Score as a set of logical statements enables automated reasoning about risk assessment. This translation allows a computational system to not only calculate a risk score given patient data, but also to determine why a specific score was assigned. By representing the scoring rules-such as thresholds for cholesterol and blood pressure, and their associated weighting-as logical predicates and quantifiers, the system can trace the derivation of the final risk value back to the contributing factors. This facilitates explainability, allowing for the identification of the most influential risk factors for a given individual, and verification of the score’s calculation process, which is crucial for clinical trust and debugging potential errors in the model or its implementation.

Unveiling the Mechanisms: Abductive and Counterfactual Reasoning

The Z3 SMT Solver was utilized to perform automated reasoning with the formalized Framingham Risk Score, enabling the computation of minimal sets of risk factors that explain a given patient’s score. This implementation treats the Framingham Risk Score as a set of logical constraints, allowing Z3 to determine the satisfying assignments – the specific combinations of risk factor values – that result in a particular risk level. By leveraging Z3’s constraint solving capabilities, the system can efficiently identify the key drivers of cardiovascular risk for individual patients, and subsequently generate both abductive and counterfactual explanations without requiring exhaustive search algorithms.

The implemented explainable AI system successfully generates abductive explanations-identifying the minimal set of risk factors contributing to a patient’s cardiovascular risk score-in 77% of cases when those explanations include five or more features. This indicates a capability to move beyond single-factor or simple two-factor explanations and uncover complex interactions between multiple risk factors. The ability to reliably identify combinations of five or more features demonstrates the model’s capacity to represent and communicate nuanced relationships within the Framingham Risk Score, providing a more comprehensive understanding of individual patient risk profiles.

Abductive explanation, in the context of cardiovascular risk assessment, functions by identifying the fewest number of risk factors that, when combined, result in a patient’s calculated Framingham Risk Score. This approach differs from simply listing all contributing factors; it aims to pinpoint a minimal sufficient set – the smallest combination of features that fully explains the observed risk level. The resulting explanation provides a concise justification for the patient’s risk, enabling clinicians to focus on the most impactful drivers of cardiovascular disease. This focused approach facilitates a more targeted understanding of individual risk profiles compared to models providing broad, non-prioritized factor lists.

Counterfactual explanations, as implemented in this system, determine the minimal adjustments to a patient’s risk factors that would result in a change to their overall cardiovascular risk category. This functionality is designed to support personalized intervention strategies by identifying actionable changes. Analysis indicates that over 80% of generated counterfactual explanations require modification of at most two risk factors to achieve this category shift, suggesting that effective interventions can often be focused on a limited set of parameters for individual patients. The system computationally derives these minimal changes, providing a data-driven basis for tailored recommendations.

Analysis of abductive explanations generated by the formalized Framingham Risk Score indicates that age and systolic blood pressure are consistently identified as key drivers of cardiovascular risk. Specifically, these two features appear in over 90% of the minimal sets of risk factors used to justify a patient’s calculated risk score. This high prevalence suggests these variables are fundamental determinants in the model’s assessment and highlights their importance in understanding individual risk profiles when using this predictive framework. The consistent inclusion of age and systolic blood pressure provides a robust basis for focusing clinical attention and further investigation in a majority of cases.

Beyond Prediction: Towards a Proactive Cardiovascular Future

Clinicians are increasingly equipped with sophisticated tools that move beyond simply identifying cardiac risk to providing a nuanced understanding of why that risk exists. This advancement stems from the integration of formal logic, which establishes a rigorous framework for analyzing patient data, with automated reasoning – systems capable of drawing inferences and identifying complex relationships. Crucially, these systems are coupled with explainable AI, ensuring that the reasoning behind risk assessments isn’t a ‘black box’ but rather a transparent process. By revealing the specific factors driving a patient’s risk score, these technologies empower healthcare professionals to move beyond generalized guidelines and tailor preventative strategies with greater precision, ultimately fostering a more proactive and effective approach to cardiovascular care.

Traditional risk assessments often identify that a patient is at risk of cardiovascular disease, but fall short of explaining why. This limitation hinders the development of truly personalized preventative strategies. Recent advances in explainable AI are changing this, providing clinicians with detailed insights into the specific factors driving an individual’s risk. By pinpointing the key contributors – whether it’s elevated cholesterol, hypertension, or lifestyle choices – interventions can be precisely tailored to address the root causes. This targeted approach moves beyond generalized recommendations, increasing the likelihood of positive behavioral changes and improved health outcomes. Ultimately, understanding the ‘why’ empowers both clinicians and patients to collaborate on a proactive, effective plan for safeguarding heart health.

A shift towards proactive heart health management is becoming increasingly feasible through technologies capable of pinpointing actionable risk factors. Rather than simply predicting cardiovascular events, these systems can identify elements within a patient’s lifestyle – diet, exercise, medication adherence – that, if altered, could demonstrably improve outcomes. Crucially, the technology doesn’t stop at identification; it simulates the impact of potential interventions, allowing clinicians to visualize the likely benefits of specific changes. This capability moves beyond reactive treatment towards preventative strategies, empowering both doctors and patients to collaboratively design personalized pathways towards sustained cardiovascular wellbeing and ultimately lessening the future burden of heart disease.

Analyses of counterfactual explanations – those detailing what changes to a patient’s data would alter a risk prediction – consistently pinpoint systolic blood pressure and total cholesterol as dominant factors influencing cardiovascular risk assessments. Appearing in over 40% of these explanations, these two biomarkers emerge as key drivers in determining an individual’s likelihood of developing heart disease. This prevalence suggests that even subtle shifts in these values can significantly impact a predicted risk score, highlighting their crucial role in both diagnosis and preventative strategies. Further investigation into these frequently cited factors could refine targeted interventions and improve the accuracy of personalized heart health plans, ultimately allowing clinicians to focus on the most impactful areas for patient improvement.

The convergence of advanced analytical technologies holds substantial promise for diminishing the widespread impact of cardiovascular disease and enhancing the health of entire populations. By shifting from reactive treatment to preventative care, these systems facilitate early intervention and empower individuals to actively manage their heart health. A reduction in the overall disease burden isn’t simply a matter of extending lifespans, but of improving the quality of life for millions, decreasing healthcare costs associated with chronic conditions, and fostering a more productive and resilient society. This proactive approach, driven by data-informed insights, ultimately envisions a future where cardiovascular events are significantly less frequent, and individuals can enjoy longer, healthier lives.

The pursuit of understanding complex systems, such as cardiovascular risk assessment via the Framingham Risk Score, inevitably reveals their inherent fragility. This work, translating the score’s logic into First-Order Logic, isn’t about achieving perfect prediction, but about gracefully observing how risk is determined. As Linus Torvalds once said, “Most good programmers do programming as a hobby, and then they get paid to do it.” This echoes the sentiment that true progress stems from intrinsic curiosity, not solely from practical application. The framework’s ability to generate both abductive and counterfactual explanations demonstrates an acceptance of the system’s limitations, prioritizing clarity and actionable insight over absolute certainty-a sign of a system aging with dignity.

What Lies Ahead?

The pursuit of transparency in risk assessment, as demonstrated by this work, merely delays the inevitable entropic cascade. The Framingham Risk Score, even when rendered through the lens of logic-based explainable AI, remains a static snapshot-a momentary caching of correlations within a relentlessly flowing system. While abductive and counterfactual explanations offer a fleeting sense of control, they do not alter the underlying reality of biological decay. Latency, in this context, is not merely computational; it’s the temporal tax levied on every prediction, every intervention.

Future efforts will likely focus on dynamic explanations-systems that adapt to a patient’s evolving state, acknowledging that risk isn’t a fixed value but a probability continually reshaped by time and circumstance. However, the inherent limitations of model-based reasoning must be confronted. The illusion of stability is easily maintained through increasing complexity, but the core problem persists: models are, by definition, abstractions, and all abstractions eventually diverge from the observed reality.

A potentially fruitful, yet largely unexplored, avenue lies in integrating the framework with longitudinal data streams-allowing explanations to be generated not just for a current risk assessment, but for the trajectory of that risk. This necessitates grappling with the inherent uncertainties of future states, and accepting that prediction, even with the most sophisticated tools, is ultimately a game of informed speculation against a backdrop of inevitable change.

Original article: https://arxiv.org/pdf/2602.22149.pdf

Contact the author: https://www.linkedin.com/in/avetisyan/

See also:

2026-02-26 18:26