Singapore

Case-based reasoning networks are models that make predictions based on similarity between the input and prototypical parts of training samples. Such models explain each decision by pointing to the prototypes that contributed the most to the final outcome. While promising, such explanations are sometimes misleading, which hampers their usefulness in safety-critical contexts. Several instances may lead to different predictions and yet have the same explanation. Drawing inspiration from formal eXplainable AI, we propose Abductive Latent Explanations (ALEs), a formalism to express sufficient conditions on the latent representation of the instance that imply the prediction. Our approach combines the inherent interpretability of case-based reasoning models and the guarantees provided by formal XAI. We propose a solver-free algorithm for generating ALEs based on three distinct paradigms, compare them, and present the feasibility of our approach on diverse datasets for image classification.

AAAI 2026

Formal Abductive Latent Explanations for Prototype-Based Networks

formal xai

explainability

interpretability

workshop paper

We are pleased to announce the Fortieth AAAI Conference on Artificial Intelligence (AAAI-26), which will be held in Singapore EXPO from January 20 to January 27, 2026.

The purpose of the AAAI conference series is to promote research in Artificial Intelligence (AI) and foster scientific exchange between researchers, practitioners, scientists, students, and engineers across the entirety of AI and its affiliated disciplines. AAAI-26 will feature technical paper presentations, special tracks, invited speakers, workshops, tutorials, poster sessions, senior member presentations, competitions, and exhibit programs, and a range of other activities to be announced.<br><br>

To access this event page, you need to log in with the **email address you registered with**. <br>Access credentials will be sent to your email from Underline -  subject line "Welcome to AAAI 2026". Please be sure to check your spam email folder if you do not see an email confirmation right away.

Please log in

To access this event page, you are required to register.
Please complete your registration to continue.

We recommend reading [**the registration information**](https://aaai.org/conference/aaai/aaai-26/registration/) first.

**Online Registration Form**: https://aaai.getregistered.net/conference-2026 

Registration Required

We are pleased to announce the Fortieth AAAI Conference on Artificial Intelligence (AAAI-26), which will be held in Singapore EXPO from January 20 to January 27, 2026.

In reinforcement learning (RL), it is advantageous to consider additional constraints on the action space to ensure safety. Existing work on such action-constrained RL often lacks expressive policy updates, computational efficiency, and predictable runtime. Recent work proposes to use truncated normal distributions for stochastic policy gradient methods. However, the computation of key characteristics, such as the entropy, log-probability, and their gradients, becomes intractable. Hence, prior work approximates these using the non-truncated distributions, which severely degrades performance. We argue that accurate estimation of these characteristics is crucial in the action-constrained RL setting, and propose efficient numerical approximations for them. We also provide an efficient sampling strategy for truncated policy distributions and validate our approach on three benchmark environments, which demonstrate significant performance improvements when using accurate estimations.

Improving Stochastic Action-Constrained Reinforcement Learning via Truncated Distributions

Robust Markov Decision Processes generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for $\omega$-regular objectives. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. We present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives, together with experimental results.

Qualitative Analysis of $\omega$-Regular Objectives on Robust MDPs

Python has become the dominant language for general-purpose programming, yet it lacks robust tools for formal verification. In contrast, programmers working in languages such as C benefit from mature model checkers, for example CBMC, which enable exhaustive symbolic reasoning and fault localisation. In this paper, we propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model checking and MaxSAT-based fault localisation in the generated C code. PyVeritas enables verification and bug localisation for Python code using existing model checking tools for C. Our empirical evaluation demonstrates that LLM-based transpilation can achieve a high degree of accuracy, up to 90% for some LLMs, enabling effective development environment that supports assertion-based verification and interpretable fault diagnosis for small yet non-trivial Python programs.

PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C

Privacy leakage in AI-based decision processes poses significant risks, particularly when sensitive information can be inferred. We propose a formal framework to audit privacy leakage using abductive explanations, which identifies minimal sufficient evidence justifying model decisions and determines whether sensitive information disclosed. Our framework formalizes both individual and system-level leakage, introducing the notion of Potentially Applicable Explanations (PAE) to identify individuals whose outcomes can shield those with sensitive features. This approach provides rigorous privacy guarantees while producing human-understandable explanations, a key requirement for auditing tools. Experimental evaluation on the German Credit Dataset illustrates how the importance of sensitive literal in the model decision process affects privacy leakage.

Beyond Verification: Abductive Explanations for Post-AI Assessment of Privacy Leakage

We explore AI-driven distributed-systems policy design by combining stochastic code generation from large language models (LLMs) with deterministic verification in a domain-specific simulator. Using a Function-as-a-Service runtime (Bauplan) and its open-source simulator (Eudoxia) as a case study, we frame scheduler design as an iterative generate-and-verify loop: an LLM proposes a Python policy, the simulator evaluates it on standardized traces, and structured feedback steers subsequent generations. This setup preserves interpretability while enabling targeted search over a large design space. We detail the system architecture and report preliminary results on throughput improvements across multiple models. Beyond early gains, we discuss the limits of the current setup and outline next steps; in particular, we conjecture that AI will be crucial for scaling this methodology by helping to bootstrap new simulators.

AI for Distributed Systems Design: Scalable Cloud Optimization Through Repeated LLMs Sampling And Simulators

We introduce INDIMATHBENCH, a human-verified benchmark designed to evaluate mathematical theorem proving, curated using an AI-powered human-assisted pipeline for formalizing natural language problems in Lean. INDIMATHBENCH is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads. Through category-based retrieval, iterative compiler feedback, and multi-model ensembles, our pipeline generates candidate formalizations that experts efficiently validate via an interactive dashboard with automated quality summaries. Evaluation across multiple frontier models demonstrates that autoformalization remains challenging, with substantial gaps between syntactic validity and semantic correctness, while theorem proving success rates remain low even with iterative refinement, demonstrating that INDIMATHBENCH presents a challenging testbed for mathematical reasoning.

IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

Reinforcement learning (RL) commonly relies on scalar rewards with limited ability to express temporal, conditional, or safety-critical goals, and can lead to reward hacking. Temporal logic expressible via the more general class of $\omega$-regular objectives addresses this by precisely specifying rich behavioural properties. We address both limitations simulatenously by combining $\omega$-regular objectives with explicit constraints, allowing safety requirements and optimisation targets to be treated separately. We develop a model-based RL algorithm based on linear programming, which in the limit produces a policy maximizing the probability of satisfying an $\omega$-regular objective while also adhering to $\omega$-regular constraints within specified thresholds. Furthermore, we establish a translation to constrained limit-average problems with optimality-preserving guarantees.

Reinforcement Learning with $\omega$-Regular Objectives and Constraints

Clinical and regulatory discussions about trustworthy therapeutic AI speak in ethical and legal terms, while technical work reports performance through AUC, F1, PPV, or survival concordance. The mapping between these numerical summaries and the social norms they support is implicit and often incoherent. This gap is acute for therapeutic AI systems built on spatially resolved data---such as digital pathology, radiology, and spatial omics---where models guide target selection, biomarker discovery, and responder prediction. We provide a technical--normative analysis of common evaluation metrics. We formalize metric families by their aggregation operations: expectation-based (expected loss; AUC as a U-statistic over pairs), quantile/tail-based (median, upper quantiles, CVaR), supremum-type (worst-group risk, minimax regret), thresholded confusion-matrix ratios (PPV/precision, sensitivity, F1), and ranking metrics (top- 
, average precision). For each family we identify the implicit social norm: maximizing average benefit, protecting typical patients, guarding against worst-case harms, or prioritizing top-predicted benefit. We prove an incompatibility result showing that high AUC can coexist with very low worst-group sensitivity under deployment-relevant thresholding, and we illustrate further incompatibilities via clinical examples. We then propose a metric design framework: (i) explicit normative declarations, (ii) multi-objective evaluation with subgroup and tail-risk constraints, and (iii) deployment checklists tying thresholds to institutional responsibilities. The goal is not to replace ethical debate with formulas, but to make explicit and auditable the value judgments encoded by metric choices.

From AUC to Accountability: Metric Choices, Social Norms, and the Deployment of Therapeutic AI

Immune checkpoint inhibitors (ICIs) have led to paradigm shifts in the treatment of several tumour types, yet microsatellite stable (MSS) colon cancer remains a major challenge and currently has no approvals for ICI-based therapies. Nevertheless, recent neoadjuvant trials introducing ICIs to early-stage MSS colon tumours have reported encouraging findings. To further improve ICI efficacy on this subset, it is first necessary to mechanistically understand how ICIs function in this otherwise immune-cold disease.\n\nPrevious studies profiling pre- and post-treatment ICI colorectal tumors (e.g., Feng et al., Nat Commun 2024) are compromised by significant sampling bias in post-treatment samples: our analysis reveals that responders are primarily composed of normal adjacent stroma while non-responders are predominantly tumor core. To overcome this limitation and characterize the effect of treatment in action, we utilized paired pre- and on-treatment samples from a window-of-opportunity study administering pembrolizumab (anti-PD-1) with XELOX chemotherapy in non-metastatic MSS colon cancer. Pre-treatment samples were composed of 3-4 biopsy pieces, while on-treatment samples were obtained from surgical resection following two cycles of therapy. To achieve a comprehensive spatial overview, large pieces from on-treatment samples (1 cm x 2 cm, encompassing both tumor nest and peripheral stroma) were selected for profiling. Using high-resolution spatial transcriptomics (10x Genomics Xenium), we profiled both pre- and on-treatment samples, generating ~17 million cells across 7 patients with detailed cell-state annotations.\n\nAs this is a window-of-opportunity study, clinical response evaluation was not the primary endpoint. Instead, to approximate treatment effect, we focused on CD8+ T-cell infiltration as a key indicator of immune modulation. Consistent with the immune-cold phenotype of MSS disease, only a subset of cases (2/7) showed increased intratumoural CD8+ effector T-cell infiltration during treatment. In contrast, most tumours (5/7) exhibited increased CD8+ pre-effector T cells restricted to peripheral stroma, showing an immune-excluded phenotype.\n\nTo link on-treatment CD8+ T-cell localization to local molecular signals, we developed linear regression models that predict CD8+ T-cell spatial distribution from secreted-factor expression. Distinct sets of secreted factors were found to be spatially associated with the two CD8+ T-cell populations: factors associated with infiltrating effector T cells included chemokines like CXCL9, CXCL10, and CXCL11 among others, whereas factors associated with stroma-restricted pre-effector T cells included CXCL12 and a broader collection of suppressive programmes. Our analysis identified specific fibroblast and macrophage states as the source of these secreted factors, suggesting distinct infiltration- and stroma-restricted immune neighborhoods. Furthermore, the infiltration- and exclusion-associated programmes were recapitulated in independent validation datasets, including on-treatment breast cancer samples from a window-of-opportunity trial (n=40; Bassez et al., Nat Med 2021) and treatment-naïve primary colorectal tumours.\n\nOverall, our study provides a comprehensive, high-resolution spatial view into how neoadjuvant chemo-immunotherapy remodels the MSS tumour microenvironment. Notably, key findings, including pre-effector T cells and their associated secreted programs, were predominantly detected at the peripheral stroma, highlighting the critical importance of characterizing this often-overlooked region. By revealing distinct spatial molecular programs that govern T-cell infiltration versus stroma-restriction, our work identifies potential therapeutic strategies to overcome immune exclusion in MSS colon cancer. 


Spatial profiling reveals molecular determinants of CD8+ dynamics during chemo-immunotherapy in MSS colon cancer

We present an improved methodology for gene expression imputation (GEI) in Xenium, a\ntargeted spatial transcriptomics platform. Xenium provides single-cell resolution but measures\nonly a limited set of genes, restricting downstream analyses. Our approach of aligning spatial\nand reference scRNA-seq data through “Symphony” in a common embedding space, integrating\nthem using single-cell neighborhood information improved recovery of genome-wide expression\nprofiles from targeted panels, enabling more accurate downstream analysis 


Downloads

Next from AAAI 2026

Improving Stochastic Action-Constrained Reinforcement Learning via Truncated Distributions

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES

.css-70qvj9{display:-webkit-box;display:-webkit-flex;display:-ms-flexbox;display:flex;-webkit-align-items:center;-webkit-box-align:center;-ms-flex-align:center;align-items:center;}Downloads

Next from AAAI 2026

Improving Stochastic Action-Constrained Reinforcement Learning via Truncated Distributions

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES

Downloads