IJCAI 2026 论文列表

We present a unified framework for modeling agents’ epistemic states and counterfactual conditionals. The novelty of our approach lies at the semantic level. We introduce a computationally grounded semantics in which an agent’s doxastic accessibility relation, needed to model the standard notion of deductively closed belief, is derived from the agent’s belief base, and in which the notion of comparative similarity between states, needed to interpret counterfactual conditionals, is computed from both the atomic formulas describing the agents’ belief bases and those describing the environment. We use this semantics to interpret a language of beliefs and counterfactuals. We demonstrate the expressiveness of our language and the flexibility of the semantics by formalizing a wide range of notions: counterfactual dependence, counterfactual notions of reason and knowledge, conditional belief. Furthermore, we show that our semantics illuminates the subtle interplay between belief change and counterfactuals. On the computational side, we provide a succinct formulation of model checking for our language and establish a PSPACE complexity result.

Large Language Models (LLMs) still exhibit limited capability in following complex instructions. While existing approaches often rely on preference learning to enhance this ability, they typically overlook the relationships between the permissible response spaces of different instructions, which restricts a model to align with subtle and diverse constraint variations. To address this, we propose Cross-Relational Preference Learning (CRPL), a novel framework for constructing preference data that explicitly models inter-instruction relationships through two key techniques: Cross-Relationship Perturbation and Cross-Region Pair Sampling. This enables the generation of more diverse preference data that captures a wide spectrum of constraint variations. Additionally, we introduce an atomic constraint-based verification mechanism to rigorously assess response satisfaction, ensuring high-quality preference pair construction. Extensive experiments across multiple preference learning methods (e.g., DPO, KTO), LLM backbones and four instruction-following benchmarks demonstrate that our approach achieves substantial improvements over prior baselines and exhibits strong generalization.

Existential rules are a prominent formalism to enrich a database with knowledge from the domain of interest, but make even basic reasoning tasks on the resulting knowledge base undecidable. To circumvent this, several classes of rules offering various useful properties have been identified. One such class, for instance, contains all sets of rules on which the chase algorithm always terminates, which guarantees the existence of a finite universal model. However, these classes are often abstract rather than concrete: it may be undecidable to check whether a given set of rules belongs to them. Given that the most studied classes of existential rules are designed for reasoning on databases, thus ensuring decidable conjunctive query entailment, we ask: Within a class that supports decidable query entailment, do the usual abstract classes become concrete? We answer in the negative for classes based upon the termination of all classical chase variants and for the bts class.

We present an extension of the Angluin-style learning algorithm for tree automata that incorporates deductive inference. The learning algorithm is provided with a term rewriting system that specifies properties of the target tree language (e.g., the order of subtrees under a symbol f is irrelevant). This term rewriting system is used to infer answers to some queries, which reduces the query complexity of the learning algorithm. We present examples of rewrite systems that express natural properties of tree-structured data, which yield a significant reduction in the number of queries.

We present two new algorithms for the problem of lexicographic inference from conditional knowledge bases. These algorithms are based on SAT and MaxSAT encodings of the underlying problem of lexicographic comparisons of classical interpretations and require only a polynomial number of SAT solver calls. In our experimental evaluation we show that our new algorithms signficantly outperform the state of the art.

Existing Programming-By-Example (PBE) systems often rely on simplified benchmarks that fail to capture the high structural complexity of real-world regexes, such as deeper nesting and frequent use of union operations. To overcome the resulting performance drop, we propose ReSyn, a synthesizer-agnostic divide-and-conquer framework that decomposes complex synthesis problem into manageable sub-problems. We also introduce Set2Regex, a parameter-efficient synthesizer capturing the permutation invariance of examples. Experimental results demonstrate that ReSyn significantly boosts accuracy across various synthesizers, and its combination with Set2Regex establishes a new state-of-the-art on challenging real-world benchmark. The complete source code, datasets, and pre-trained model checkpoints are publicly available at https://github.com/mrseongminkim/ReSyn.

C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatically verifying C-RASPs. To this end, we establish a connection to the verification of synchronous dataflow programs in Lustre, which enables us to exploit state-of-the-art model checkers utilizing highly optimized SMT-solvers. Our second contribution addresses learning a C-RASP program in the first place. To this end, we provide a new algorithm for learning a C-RASP from examples using local search. We demonstrate efficacy of our implementation for benchmarks of C-RASPs in the literature, in particular in connection to the following applications: (1) transformer program optimization, and (2) constrained learning of transformer programs (based on a partial specification).

Continual knowledge graph embedding (CKGE) has gained popularity for managing dynamic knowledge graphs. Unlike general graph continual-learning approaches, CKGE focuses on retaining triple-level knowledge, thereby overcoming the inability of static models to accommodate continuously arriving facts. However, as new fact triples come in, real-world knowledge graphs often experience structural distribution shifts: the underlying topology and the way facts interconnect evolve over time. This presents a challenge that the structural distribution of historical data may diverge from that of emerging data, creating a distributional mismatch that complicates the adaptation to new trends. To address this, we propose Pattern-Anchor Alignment (PAAL), which introduces relation-level structural anchors to explicitly model these structural shifts. By quantifying the alignment between the structural distribution of emerging triples and historical anchors, PAAL implements an alignment-modulated optimization strategy. It utilizes a calibrated gating mechanism to precisely regulate the intensity of historical constraints based on structural stability. Experimental results indicate the effectiveness of PAAL, showing average H@1 improvements of 11.77% and 9.29% on pattern-shift and standard CKGE benchmarks, respectively. Our code is available at https://github.com/cangjie553/PAAL.

Temporal Knowledge Graph Reasoning (TKGR) aims at inferring missing (especially future) events from historical data. Current evaluation in TKGR uniformly weights all events, ignoring that most are trivial repetitions, which overestimate the true reasoning ability. Therefore, the rare outstanding events, whose prediction demands deeper reasoning, should be distinguished and emphasized. To this end, we propose a strikingness-aware evaluation framework, which introduces a rule-based strikingness measuring framework (RSMF) to quantify event strikingness by comparing its expected occurrence with peer events derived from temporal rules. Strikingness is then integrated as a weighting factor into metrics like weighted MRR and Hits@k. Experiments on four TKG benchmarks reveal: 1) All representative models perform worse as event strikingness increases, 2) Path-based methods excel on low-strikingness events and representation-based ones on high-strikingness events, 3) We design an ensemble method whose gains stem from fitting trivial events rather than reasoning improvement. Our framework provides a more rigorous evaluation, refocusing the field on predicting outstanding events.

We examine how causal beliefs affect an agent's choices and how feedback on those choices leads to updated causal beliefs. Building on the structural-equations framework for modeling causality, we first examine the general problem of updating causal beliefs in the face of novel (and possibly inexplicable) data. We model an agent who is uncertain of the true causal model, and therefore entertains a probabilistic belief over the set of possible models. We then consider how causal beliefs influence choices by building a model of agency and utility on top of the usual structural-equations framework. Using these two components, we propose a notion of steady state, where the feedback received from an agent's optimal action, given her current beliefs about the true causal model, can be rationalized by those beliefs.

In this paper, we introduce novel tuple inconsistency measures that quantify the extent to which individual tuples contribute to violations of denial constraints in inconsistent databases. Then, we formally show that one of the proposed measures fully satisfies a set of well-motivated axiomatic properties. As an application, we lift tuple inconsistency to the level of query answers, obtaining a principled framework for measuring and explaining the inconsistency inherent in query results. We further investigate the computational complexity of tuple and answer inconsistency measures under denial constraints, identifying tractable cases that make their application to real-world data feasible. Finally, our experimental study on varying dataset- and inconsistency-settings demonstrates that, in comparison to existing methods, the proposed measures yield more fine-grained and informative assessments of inconsistency in databases.

Bounded fitting is an attractive paradigm for learning logical formulas from labeled data examples that offers PAC-style generalization guarantees and can often be implemented leveraging SAT solvers. It has been successfully applied to learning concepts of the description logic ALC. We study bounded fitting for learning concepts in expressive description logics that extend ALC with inverse roles, qualified number restrictions, and feature comparisons. We investigate under which conditions bounded fitting keeps its favorable theoretical properties in this setting, and implement is using a SAT solver. We compare our implementation against state-of-the-art concept learners with encouraging results, demonstrating that it is a practical approach to expressive concept learning.

Argumentation is an important topic of AI for modeling and reasoning about arguments. In abstract argumentation, we consider directed graphs, so-called argumentation frameworks (AF), that express conflicts between arguments. The semantics is defined by the notion of extensions, which are sets of arguments that satisfy particular relationship conditions in the AF. Usually, standard reasoning in argumentation do not reveal how far apart extensions are. We introduce a quantitative notion of diversity of extensions based on the symmetric-difference and provide a systematic complexity classification. Intuitively, diversity captures whether extensions of a framework (accepted viewpoints) differ only marginally or represent fundamentally incompatible sets of arguments. We study whether an AF admits k-diverse extensions, admits k-diverse extensions covering specific arguments, and to compute the largest k for which an AF admits k-diverse extensions. We outline a prototype and provide an evaluation for computing diversity levels.

Computation Tree Logic (CTL) is a fundamental formalism for specifying and reasoning about the behavior of non-terminating systems. Due to the lack of uniform interpolation (UI) property, CTL is usually limited in modular reasoning and system abstraction. This paper studies uniform interpolation in CTL fragments with restricted temporal operators from the point of knowledge forgetting, aiming to identify the minimal logic extensions of these fragments that preserve UI property (referred to as their uniform interpolation closure). Our results demonstrate that: (1) CTL(X), the fragment of CTL allowing only the “neXt” operator, enjoys the UI property; (2) the UI closure of the fragment CTL(F<, X) is the bisimulation-invariant fragment of quantified CTL in prenex-normal-form, where F< is the operator “next Future”; (3) CTL(F<) fails to possess Craig interpolation, and every extension of CTL(F<) that possesses the Craig interpolation property is necessarily an extension of CTL(U) which contains only the “Until” operator. These findings provide a precise characterization of the expressive power required to achieve modularity in CTL.

Incomplete Abstract Argumentation Frameworks (iAAFs) extend Abstract Argumentation Frameworks (AAFs) by allowing arguments and attacks to be specified as uncertain, enabling a compact representation of alternative argumentation scenarios. Despite extensive work on reasoning with iAAFs, their expressive power relative to standard AAFs is still unclear. We address this question by studying whether the reasoning based on possible-extensions in iAAFs can be reduced to classical reasoning on AAFs. Our analysis relates iAAFs and AAFs via two comparison notions: equivalence, where an AAF yields as extensions exactly the possible extensions of an iAAF, and projection-equivalence, where such extensions are obtained by projecting away auxiliary arguments. We characterize the semantics under which these relationships hold, and, in these cases, provide constructive transformations from iAAFs to AAFs, thus also enabling classical argumentation tools to be applied to qualitative-uncertainty reasoning.

Integration of Answer Set Programming (ASP) with neural networks has emerged as a promising tool in Neuro-symbolic AI. While existing approaches extend the capabilities of ASP to real world domains, their reasoning pipelines depend on classical solvers, which is a bottleneck for scalability. To tackle this problem, we propose a new method to compute stable models, called decision-propagation (DProp), which alternates falsity decisions and truth propagations. Successful DProp computations are shown to capture the stable model semantics. We then develop Neural DProp (NDProp), a differentiable extension of DProp with neural computation for decisions and fuzzy evaluation for propagations. We evaluate the capabilities of NDProp for learning decision heuristics as well as neuro-symbolic integration, and compare it with existing neuro-symbolic approaches. The results show that NDProp can learn to efficiently compute stable models, and it improves accuracy and scalability on neuro-symbolic benchmarks.

Bender Decomposition is a well-known solving technique in Operation Research that decomposes a problem into a master and a subproblem, which interact via “cuts". This technique has been extended to Logic-Based Bender Decomposition (LBBD), solving problems specified by logic-based languages and enabling a wider applicability. However, while Bender Decomposition guarantees optimality, LBBD does not: this property is problem-specific and depends on the defined decomposition and cuts. In this paper, we present a theoretical analysis of the conditions under which LBBD, including cuts, can preserve optimality in the context of Answer Set Programming (ASP), a prominent logic-based language in the field of Artificial Intelligence. We also introduce a general-purpose algorithm that employs both minimal unsatisfiable subsets and minimal correction subsets to define cuts in a fully automated, problem-independent way. The algorithm preserves the optimality guarantees of Bender Decomposition. An empirical evaluation on real-world scheduling instances shows that our approach can find significantly more solutions, and more optimal ones, compared to a standard direct ASP encoding, while also consistently reducing the execution time.

Progression, the task of updating a knowledge base to reflect action effects, generally requires second-order logic. Identifying first-order special cases, by restricting either the knowledge base or action effects, has long been a central topic in reasoning about actions. It is known that local-effect, normal, and acyclic actions, three increasingly expressive classes, admit first-order progression. However, a systematic analysis of the size of such progressions, crucial for practical applications, has been missing. In this paper, using the framework of Situation Calculus, we show that under reasonable assumptions, first-order progression for these action classes grows only polynomially. Moreover, we show that when the KB belongs to decidable fragments such as two-variable first-order logic or universal theories with constants, the progression remains within the same fragment, ensuring decidability and practical applicability.

Static benchmarks for LLMs are increasingly compromised by contamination and overfitting, especially on knowledge-intensive reasoning tasks. While recent dynamic benchmarks can alleviate staleness, they often increase difficulty at the expense of answerability and controllability. In this paper, we propose StressEval, a failure-driven data synthesis framework that turns observed model failures into dynamic, challenging, and controlable test instances. StressEval consists of three stages: (i) it constructs a semi-structured difficulty card that identifies the failed reasoning step and its root cause; (ii) it applies a dual-perspective instance-synthesis method that targets both knowledge gaps and reasoning breakdowns while preserving the underlying difficulty factors; and (iii) it applies a gating mechanism to retain only grounded, unambiguous instances. Seeding from multiple knowledge-intensive reasoning datasets, we employ StressEval to build Dynamic-OneEval, a focused suite of challenging dynamic benchmark. Across several state-of-the-art LLMs, Dynamic-OneEval yields substantially larger performance drops than the original benchmarks while retaining explicit difficulty factors, enabling more actionable iteration.