IJCAI 2026 论文列表

We investigate the computational complexity of neural network verification in quantised settings. We distinguish three classes of Feedforward Neural Networks (FNNs): rational FNNs with exact rational weights, quantised FNNs whose weights come from a finite-width arithmetic, and dynamically quantised FNNs in which rational networks are evaluated with respect to a given finite-width arithmetic. We consider two types of specifications used in the literature. Linear programming (LP) specifications are conjunctions of linear constraints, while bit-vector (BV) specifications allow reasoning at the bit level and can express non-linear constraints. Our results give a complexity landscape of these verification problems. For quantised FNNs with fixed arithmetic precision, we show that verification under both LP and BV specifications remains NP-complete, matching the complexity of the rational case. For dynamically quantised FNNs with BV specifications, we establish upper bounds, complementing a previously known PSPACE-hardness result.

Graph Neural Networks (GNNs) have become increasingly central to several analysis tasks in various domains, ranging, e.g., from social networks to molecular analysis. Understanding the decision-making process of GNNs is a critical challenge in machine learning, particularly when post-hoc explanations, attempting to answer why specific inputs are classified in a certain way by a given model, are required for specific input predictions. Existing post-hoc explainability methods for GNNs often rely on counterfactual reasoning, grounded in the `if this had not occurred' thinking, that typically identifies minimal subgraphs perturbations that would change a prediction. Notably, less attention has been posed on the equally important semifactual reasoning, grounded in the `even if this has not occurred' thinking, that results in identifying maximal subgraphs perturbations that would not change a prediction. In this paper, we introduce a novel technique for post-hoc explainability queries in GNNs by focusing on the semifactual reasoning. We first thoroughly investigate the computational complexity of several reasoning and optimization problems related to the computation of semifactuals, and then propose a novel learning architecture for addressing their computation. Finally, we experimentally evaluate the proposed approach in a variety of settings, showing its effectiveness in generating high-quality semifactual explanations.

Modern neural networks can be accurate yet poorly calibrated. We present Random Geometric Calibration (RGC), a post hoc method that augments confidence estimation with a geometric signal derived from distances to training data in an aggregated semantic representation space. Prior geometric calibration methods in feature space often rely on architecture-specific layer choices, which can be unstable across models and datasets. To avoid this dependence, RGC samples a fixed number of intermediate blocks uniformly at random and reuses this set at both calibration and test time. We instantiate RGC with RGCL, which applies spatial pyramid pooling to each sampled activation, projects features to a fixed dimension, and computes a nearest-neighbor separation score that is mapped to probabilities via isotonic regression. We also present RGCC, which replaces pooling and projection with uniform coordinate sampling for improved computational efficiency. We evaluate RGCL and RGCC across multiple datasets, including CIFAR-10, CIFAR-100, and Tiny-ImageNet, and across a diverse set of architectures such as ResNet, DenseNet, and DINOv2. Our results show that RGCL achieves state-of-the-art or near state-of-the-art calibration performance, reducing expected calibration error by approximately 78% on average and by up to 97% for some models. Finally, we provide representation analysis that explains why RGCL and RGCC succeed without layer selection and characterize their computational overheads. We observe that layers exhibiting favorable geometric structure tend to emerge in later network blocks, and that randomized aggregation implicitly emphasizes these layers, leading to robust and reliable calibration performance.

Chain-of-Thought (CoT) prompting trades inference speed for reasoning accuracy. Existing compressors force a compromise as static gradient techniques treat tokens independently, severing sequential logic, while uncertainty-based pruning ignores the final answer. We introduce Adaptive GoGI-Skip, a framework that resolves this tension by non-linearly coupling Goal-Gradient Importance (GoGI) with Adaptive Dynamic Skipping (ADS). GoGI quantifies each token's functional contribution to answer correctness via gradient sensitivity. ADS leverages runtime entropy to dynamically modulate the GoGI threshold, preserving low-gradient tokens essential for structural coherence at high-uncertainty junctions. Trained on 7,472 MATH traces, our policy transfers zero-shot to AIME, GPQA, and GSM8K, reducing token volume by >45% and accelerating inference up to 2.0x without accuracy loss. These results suggest that thinking-optimal compression demands synergy between teleological goals and epistemic uncertainty.

Synthesising autonomous agents that can navigate uncertain environments while adhering to complex temporal constraints remains a fundamental challenge. While Linear Temporal Logic (LTL) provides a rigorous language for specifying such tasks, the inherent undecidability of qualitatively verifying LTL satisfaction in partially observable Markov decision processes renders quantitative synthesis difficult, especially when designing reliable reward signals for approximate solvers. In this paper, we bridge this gap with a novel, sound reward-shaping mechanism that dynamically generates belief-dependent rewards grounded in certified LTL satisfaction. By integrating this mechanism into an enhanced Monte Carlo Planning framework, we empower agents to navigate the `fog' of partial observability with a search process focused on maximising verifiable success. Our experiments demonstrate that this approach not only thrives in scenarios where existing solvers fail but also maintains effectiveness and scalability across diverse benchmark domains.

Virtual Knowledge Graphs (VKGs) provide unified access to legacy relational data sources through a high-level ontology modeling a domain of interest. The content of the ontology elements (classes and properties) is virtually mapped to underlying data sources through declarative mappings. The standard approach to interacting with a VKG system is to use SPARQL as the query language. However, the complexity of SPARQL creates a high entry barrier for normal users. In this paper, we study the VKG-QA task, which enables users to interact with the VKGs through a natural language (NL) interface by translating their questions into SPARQL queries. One critical challenge in such translation is silent failures, where a syntactically correct SPARQL query returns empty results because it involves ontology elements that lack mappings to the underlying data. To address this, we propose NaVQA (Navigation-based VKG Question Answering), a framework leveraging Large Language Models that (1) identifies and indexes the active ontology elements based on the mapping specifications, and (2) iteratively constructs a query graph from the NL question using the active ontology elements and their relations to synthesize SPARQL. Experiments on three real-world VKGs show that NaVQA significantly mitigates silent failures and outperforms existing baselines.

Accurate estimation of time-varying treatment effects is crucial for optimizing interventions in personalized medicine. However, observational data often contains complex confounding bias and temporal complexities, making counterfactual estimation challenging. We propose Counterfactual Estimation via Temporal-Aware Intervention Networks (TAIN), a novel model that introduces an Intervention-aware Functional Convolution kernel to emphasize the role of treatments and capture complex temporal treatment interactions. TAIN addresses confounding bias from a domain generalization perspective, approximating the unknown target domain using adversarial examples and incorporating Sharpness-Aware Minimization to derive a generalization bound. This approach is more suitable for longitudinal settings compared to existing methods inspired by domain adaptation techniques due to inherent differences between static and longitudinal contexts. Experiments on simulated datasets demonstrate TAIN's superior performance compared to state-of-the-art models for counterfactual estimation over time.

AI for materials science is a critical topic within AI for science, aiming to accelerate materials discovery and produce accurate property predictions. Bilayer 2D material stacking is essential for exploring new materials with novel functions and inherent phenomena, enabling the creation of new 2D bilayers for diverse real-world applications. Research on bilayer vdWs materials has made significant progress from experimental and computational perspectives. Various bilayer materials have been successfully synthesized experimentally and the increasing utilization of high-throughput computing technology has constructed several computational two-dimensional materials databases. However, the use of AI to model bilayer stacking and predict new properties remains underexplored, necessitating further research studies. In this work, we propose a novel multimodal learning approach to study the interfaces between dissimilar materials that jointly enable new or multiple functions, and to predict new properties arising from the vertical integration (stacking) of different functional material layers under given configurations. Comprehensive experiments demonstrate the effectiveness and efficiency of our approach compared to baseline methods. Our code is available at https://github.com/AnVuong123/bimat_ml.

Probabilities of causation (PoCs) are fundamental quantities for counterfactual analysis and personalized decision making. However, existing analytical results are largely confined to binary settings. This paper extends PoCs to multi-valued treatments and outcomes by deriving closed form bounds for a representative family of discrete PoCs within Structural Causal Models, using standard experimental and observational distributions. We introduce the notion of equivalence classes of PoCs, which reduces arbitrary discrete PoCs to this family, and establish a replaceability principle that transfers bounds across value permutations. For the resulting bounds, we prove soundness in all dimensions and empirically verify tightness in low dimensional cases via Balke's linear programming method; we further conjecture that this tightness extends to all dimensions. Simulations indicate that our closed form bounds consistently tighten recent recursive bounds while remaining simpler to compute. Finally, we illustrate the practical relevance of our results through toy examples.

Combinatorial and optimization problems are fundamental to many industrial AI applications. Solving large-scale real-world instances of such problems typically requires careful problem formalization, specialized solvers, and expert-designed heuristics. Thus, experts need to specify not only *what* solutions are, but also *how* they are derived. By introducing the tool CheckMate, we show that algorithm generation via code evolution represents a paradigm shift by eliminating the need to formulate the *how*. CheckMate solely relies on the *what*. Specifically, a formal specification ensures solutions' correctness and enables systematic performance evaluation of the generated programs, while a natural language description guides the evolutionary process. The effectiveness of our method is demonstrated on selected problems from two industrial domains: configuration and scheduling. In all cases, the evolved algorithms consistently outperform state-of-the-art solvers. This underscores the potential of formal methods in guiding code evolution for automatically solving complex real-world problems.

Answer Set Programming (ASP) is a popular knowledge representation and reasoning framework with countless applications for modeling and solving combinatorial problems. With increasingly large applications, identifying crucial details and collapsing irrelevant or indistinguishable information becomes crucial for a human in the loop. This idea led to the investigation of different notions of abstraction, which relate to forgetting and projection. Very recently, clustering formalisms have been designed that also preserve program dependencies. However, crucial computational properties, such as finding abstractions, remained entirely unexplored to date. In this work, we examine the computational complexity of existing abstraction techniques based on clustering (faithful and uniform abstractions). Besides checking, we tackle the crucial question of constructing abstractions, by also proposing a novel syntactic operator to achieve uniform abstractions, when possible. Moreover, we investigate whether symmetry detection can be used to determine abstractable parts in a program, and give insights on the difference of interchangeability and indistinguishability, by introducing a relaxation of the uniform abstraction condition to capture semantic indistinguishability. We observe that this notion enables us to obtain intuitive faithful abstractions, while symmetry does not. We explore properties needed to reach abstractions from syntactic symmetry.

We propose a modular logical framework for both reasoning with and measuring inconsistency in propositional knowledge bases. The framework extends propositional logic with markers attached to occurrences of atoms and interpreted as pointers to worlds. This allows different occurrences of the same atom to be evaluated in different contexts unless they share a marker. We define paraconsistent entailment relations via abnormality functions that associate each model with a set of deviations from a preferred behavior. Each entailment relation is then defined with respect to models that are minimal under set inclusion. We show that suitable markings and abnormality functions capture several existing forms of inconsistency-tolerant reasoning, including entailment based on maximal satisfiable subsets and the minimally inconsistent Logic of Paradox. We also show how a range of inconsistency measures can be expressed in the same setting. Thus our framework provides a uniform basis for diverse approaches to inconsistency handling and measurement.

Virtual Knowledge Graphs (VKGs) provide an effective solution for data integration by mapping heterogeneous data sources to a unified ontology. However, existing VKG construction frameworks primarily focus on one-shot construction, which often results in partial data coverage and support for only initial information needs. After the VKG has been deployed, new information needs will inevitably arise over time. Therefore, enriching VKGs to support evolving information needs remains an expert-intensive iterative task. In this work, we formulate the task of Information-Needs-Guided VKG Enrichment (IN-VKGE), and propose an iterative framework that leverages large language models to assess whether information needs can be supported using SPARQL execution feedback and generate ontology and mapping enrichment proposals. Experiments on two real-world VKGs show that our approach outperforms existing paradigms, and produces enrichment proposals that receive high expert ratings for effectively resolving the identified information needs.

World models (WM) learn predictive representations from high-dimensional sensory input. However, their internal knowledge is implicit and often inadequate for systematic reasoning about object structure. Qualitative Spatial Reasoning (QSR) models provide explicit human-readable object descriptions under transformations. This paper shows that these two forms of modeling can be combined by injecting a QSR model into a WM to improve the WM reasoning abilities. Using a cube rotation setting inspired by the cube comparison test used in mental rotation tasks as a case study, we use a QSR model that captures the geometric relationships and transformation rules describing how features move across faces under discrete rotations. We translate this QSR model into differentiable constraints using Logic Tensor Networks (LTNs) to guide gradient based learning. These constraints are injected into the WM loss function to regularize its latent dynamics to satisfy the spatial constraints of rotation. The results show that under an extreme data scarce regime (10%), baseline model's performance collapses to near zero, whereas our approach achieves above 90% better performance relative to baseline. Our method consistently maintains high scores across all data regimes (~80%), for both in-distribution and out-of-distribution observations. This paper proposes a novel framework to infuse QSR knowledge inside WM to make learned latent dynamics logical. Code is available at: https:// github.com/ajayrao80/LtnDreamer/

Qualitative preferences specified in CP-theory define a partial order over outcomes based on induced dominance relations. We investigate the problem of measuring divergence between such induced orders. We introduce two formally equivalent distance metrics, each leveraging a distinct computational strategy based on different types of normalization. Preliminary empirical results support the soundness of the proposed methodologies and offer comparative insights into their computational properties. To the best of our knowledge, this is the first study to compute distance measures between qualitative preferences that jointly accounts for conditional dependencies and relative importance statements.

Inductive Logic Programming (ILP) learns interpretable logical rules from data. Existing methods are transductive: their learned parameters are bound to specific predicates and require retraining for each new task. We introduce Neural Rule Inducer (NRI), a pretrained model for zero-shot rule induction. Rather than encoding literal identities, NRI represents literals using domain-agnostic statistical properties such as class-conditional rates, entropy, and co-occurrence, which generalize across variable identities and counts without retraining. The model consists of a statistical encoder and a parallel slot-based decoder. Parallel decoding preserves the permutation invariance of logical disjunction; an autoregressive decoder would instead impose an arbitrary clause order. Product T-norm relaxation makes rule execution differentiable, allowing end-to-end training on prediction accuracy alone. We evaluate NRI on rule recovery, robustness to label noise and spurious correlations, and zero-shot transfer to real-world benchmarks, and we believe this work opens up the possibility of foundation models for symbolic reasoning. Code and the reference checkpoint are available at https://github.com/phuayj/neural-rule-inducer. An extended version with full appendices is available at https://arxiv.org/abs/2605.04916.

Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and thereby replace some of the manual work %alleviating some of the manual effort done by Formal Verification engineers and deliver value to industry. We present a neurosymbolic approach that includes two prompting frameworks to generate candidate invariants, which are checked using a formal symbolic tool. Our results indicate that with sufficient reprompting, LLMs are able to generate inductive arguments for mid-size open-source RTL designs. For 90% of our problem set, at least one of the prompt setups succeeded in producing a provably correct inductive argument.

Many semantics for abstract weighted argumentation assume that each argument is associated with a numerical initial weight. Eliciting these initial weights poses several challenges: (1) accurately providing a specific numerical value is often difficult, and (2) individuals frequently confuse initial weights with acceptability degrees in the presence of other arguments. We therefore propose an elicitation pipeline that allows a user to specify their believed final acceptability degree intervals for each argument. We can determine which portion (if any) of these intervals are rational, refining the intervals, or restoring rationality when the intervals are irrational. This allows us to ultimately identify possible initial weights for each argument.

Argumentation dynamics provides techniques for revising argumentation theories in real-world domains (e.g., an autonomous medical diagnostic agent). Within this context, enforcement in abstract argumentation has become a prominent topic. Enforcement aims to modify an argumentation framework to satisfy given acceptability conditions while minimizing change from the original framework. Motivated by the need to address both syntactic and semantic notions of change, we propose formula-based enforcement, a generic framework that strictly generalizes existing approaches, by additionally covering cases they cannot handle, including semantic change. We analyze its complexity under central argumentation semantics, obtaining results from NP-completeness to completeness for the third level of the polynomial hierarchy. For second-level complete variants, we present an exact procedure based on MaxSAT solving and counterexample-guided abstraction refinement (CEGAR), and evaluate it empirically.