In this work, we show how the class of improvement operators --- a general class of iterated belief change operators --- can be used to define a learning model. Focusing on binary classification, we present learning and inference algorithms suited to this learning model and we evaluate them empirically. Our findings highlight two key insights: first, that iterated belief change can be viewed as an effective form of online learning, and second, that the well-established axiomatic foundations of belief change operators offer a promising avenue for the axiomatic study of classification tasks.
论文检索
输入标题、作者或关键词，从 1,280 篇学术成果中精准定位
已筛选
IJCAI 2025
1,280篇论文
第 39 / 64 页
In this paper, we investigate verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs properties, and provide an efficient translation from LVP instances into a logical language. We show that LVP is in PSPACE, for any reasonable activation functions. We provide a proof system. We also prove PSPACE-hardness, indicating that while reasoning about quantized GNNs is feasible, it remains generally computationally challenging.
This paper introduces a game-theoretic framework for restoring consistency in propositional bases. The process is modeled as an interactive dialogue between two agents: a Proponent, who seeks to isolate a unique, consistent subset by posing strategic questions, and an Opponent, who aims to obstruct that goal through adversarial responses. We show that this framework provides a foundation for quantifying the effort involved in restoring consistency, revealing a connection between this effort and entropy in information theory. Focusing on the case where consistency is achieved by isolating a single maximal consistent subset, we establish links between the structure and number of such subsets and the existence of winning strategies. Finally, we demonstrate how the quantified restoration effort can serve as a basis for measuring inconsistency.
There has been substantial progress in the inference of formal behavioural specifications from sample trajectories, for example using Linear Temporal Logic (LTL). However, these techniques cannot handle specifications that correctly characterise systems with stochastic behaviour, which occur commonly in reinforcement learning and formal verification. We consider the passive learning problem of inferring a Boolean combination of probabilistic LTL (PLTL) formulas from a set of Markov chains, classified as either positive or negative. We propose a novel learning algorithm that infers concise PLTL specifications, leveraging grammar-based enumeration, search heuristics, probabilistic model checking and Boolean set-cover procedures. We demonstrate the effectiveness of our algorithm in two use cases: learning from policies induced by RL algorithms and learning from variants of a probabilistic model. In both cases, our method automatically and efficiently extracts PLTL specifications that succinctly characterize the temporal differences between the policies or model variants.
Instantiation-based Formalization of Logical Reasoning Tasks Using Language Models and Logical Solvers
PDF ↗Robustness of reasoning remains a significant challenge for large language models, and addressing it is essential for the practical applicability of AI-driven reasoning systems. We introduce Semantic Self-Verification (SSV), a novel approach that addresses the key challenge in combining language models with the rigor of logical solvers: to accurately formulate the reasoning problem from natural language to the formal language of the solver. SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver. In addition to significantly advancing the overall reasoning accuracy over the state-of-the-art, a key novelty that this approach presents is a feature of verification that has near-perfect precision over a significant coverage of cases, as we demonstrate on open reasoning benchmarks. We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.
Knowledge graphs (KGs) are powerful tools for modelling complex, multi-relational data and supporting hypothesis generation, particularly in applications like drug repurposing. However, for predictive methods to gain acceptance as credible scientific tools, they must ensure not only accuracy but also the capacity to offer meaningful scientific explanations. This paper presents a novel approach REx, for generating scientific explanations based in link prediction in knowledge graphs. It employs reward and policy mechanisms that consider desirable properties of scientific explanation to guide a reinforcement learning agent in the identification of explanatory paths within a KG. The approach further enriches explanatory paths with domain-specific ontologies, ensuring that the explanations are both insightful and grounded in established biomedical knowledge. We evaluate our approach in drug repurposing using three popular knowledge graph benchmarks. The results clearly demonstrate its ability to generate explanations that validate predictive insights against biomedical knowledge and that outperform the state-of-the-art approaches in predictive performance, establishing REx as a relevant contribution to advance AI-driven scientific discovery.
Normative Restraining Bolts (NRBs) adapt the restraining bolt technique (originally developed for safe reinforcement learning) to ensure compliance with social, legal, and ethical norms. While effective, NRBs rely on trial-and-error weight tuning, which hinders their ability to enforce hierarchical norms; moreover, norm updates require retraining. In this paper, we reformulate learning with NRBs as a multi-objective reinforcement learning (MORL) problem, where each norm is treated as a distinct objective. This enables the introduction of Ordered Normative Restraining Bolts (ONRBs), which support algorithmic weight selection, prioritized norms, norm updates, and provide formal guarantees on minimizing norm violations. Case studies show that ONRBs offer a robust and principled foundation for RL-agents to comply with a wide range of norms while achieving their goals.
The responsibility gap is a set of outcomes of a collective decision-making mechanism in which no single agent is individually responsible. In general, when designing a decision-making process, it is desirable to minimise the gap. The paper studies the class of mechanisms for which the gap is empty and proposes a concept of an elected dictatorship. It shows that, in a perfect information setting, the gap is empty if and only if the mechanism is an elected dictatorship. It also proves that in an imperfect information setting, the class of gap-free mechanisms is positioned strictly between two variations of the class of elected dictatorships.
Few-shot knowledge graph reasoning (FS-KGR) try to infer missing facts in a knowledge graphs using limited data (such as only 3/5 samples).Existing strategies have shown good performance by mining more supervised information for few-shot learning through meta-learning and self-supervised learning. However, the problem of insufficient samples has not been fundamentally solved. In this paper, we propose a novel algorithm based on adversarial learning for Enhancing Negative samples in few-shot scenarios of FS-KGR, termed FS-KEN. Specifically, we are the first to use GAN to conduct data augmentation on FS-KGR scenario. FS-KEN uses policy gradient GANs for negative sample augmentation, solving the gradient back-propagation issue in traditional GANs. The generator aims to produce high-quality negative entities. while the objective of the discriminator is to distinguish between generated entities and real entities. Comprehensive experiments conducted on two few-shot knowledge graph completion datasets reveal that FS-KEN surpasses other baseline models, achieving state-of-the-art results.
Traditional logic-based belief revision research focuses on designing rules to constrain the behavior of revision operators. Frameworks have been proposed to characterize iterated revision rules, but they are often too loose, leading to multiple revision operators that all satisfy the rules under the same belief condition. In many practical applications, such as safety critical ones, it is important to specify a definite revision operator to enable agents to iteratively revise their beliefs in a deterministic way. In this paper, we propose a novel framework for iterated belief revision by characterizing belief information through preference relations. Semantically, both beliefs and new evidence are represented as belief algebras, which provide a rich and expressive foundation for belief revision. Building on traditional revision rules, we introduce additional postulates for revision with belief algebra, including an upper-bound constraint on the outcomes of revision. We prove that the revision result is uniquely determined given the current belief state and new evidence. Furthermore, to make the framework more useful in practice, we develop a particular algorithm for performing the proposed revision process. We argue that this approach may offer a more predictable and principled method for belief revision, making it suitable for real-world applications.
Distribution shifts in recommender systems between training and testing in user-item interactions lead to inaccurate recommendations. Despite the promising performance of test-time adaptation technology in various domains, it still faces challenges in recommender systems due to the impracticality of fine-tuning models and the infeasibility of obtaining test-time labels. To address these challenges, we first propose a Test-Time Adaptation framework for Graph-based Recommender system, named TTA-GREC, to dynamically adapt user-item graphs at test time in a data-centric way, handling distribution shifts effectively. Specifically, our TTA-GREC targets KG-enhanced GNN-based recommender systems with three core components: (1) Pseudo-label guided UI graph transformation for adaptive improvement; (2) Rationale score guided KG graph revision for semantic enhancement; and (3) Sampling-based self-supervised adaptation for contrastive learning. Experiments demonstrate TTA-GREC's superiority at test time and provide new data-centric insights on test-time adaptation for better recommender system inference.
Improving Efficiency of Answer Set Planning with Rough Solutions from Large Language Models for Robotic Task Planning
PDF ↗Answer Set Programming (ASP) planning can be used to refine the rough solutions generated by Large Language Models (LLMs) to handle specific restrictions of actions, i.e., reconstruct the rough solutions to be executable, for robotic task planning. However, it is still challenging to efficiently solve ASP programs that have multiple variables with large domains, which prevents the above application of ASP planning from real-world task planning problems. In this paper, we consider how to reduce the domains of variables without losing possible solutions for ASP planning, while given these rough solutions from LLMs. Based on the above reduction, we introduce CLMASP, an approach that couples LLMs with ASP for robotic task planning. We evaluate CLMASP on the VirtualHome platform for common indoor tasks, demonstrating a significant improvement in the executable rate from under 10% to nearly 90% and reducing average ASP planning time from over 2 hours to under 5 seconds. Code is available at https://github.com/CLMASP/CLMASP.
The Boolean satisfiability problem (SAT) is a well-known example of monotonic reasoning, of intense practical interest due to fast solvers, complemented by rigorous fine-grained complexity results. However, for non-monotonic reasoning, e.g., abductive reasoning, comparably little is known outside classic complexity theory. In this paper we take a first step of bridging the gap between monotonic and non-monotonic reasoning by analyzing the complexity of intractable abduction problems under the seemingly overlooked but natural parameter n: the number of variables in the knowledge base. We obtain several positive results for SigmaP2- as well as NP- and coNP-complete fragments, which implies the first example of beating exhaustive search for a SigmaP2-complete problem (to the best of our knowledge). We complement this with lower bounds and for many fragments rule out improvements under the (strong) exponential-time hypothesis.
Reasoning about causality and agent causal knowledge is critical for effective decision-making and planning in multi-agent contexts. Previous work in the area generally assumes that the domain is deterministic, but in fact many agents operate in nondeterministic domains where the outcome of their actions depends on unpredictable environment reactions. In this paper, we propose a situation calculus-based framework for reasoning about causal knowledge in nondeterministic domains. In such domains, the agent may not know the environment reactions to her actions and their outcomes, and may be uncertain about which actions caused a condition to come about. But she can perform sensing actions to acquire knowledge about the state and use it to gain knowledge about causes. Our formalization recognizes sensing actions as causes of both physical and epistemic effects. We also examine how regression can be used to reason about causal knowledge.
Fuzzy logic programming is an established approach for reasoning under uncertainty. Several semantics from classical, two-valued logic programming have been generalized to the case of fuzzy logic programs. In this paper, we show that two of the most prominent classical semantics, namely the stable model and the well-founded semantics, can be reconstructed within the general framework of approximation fixpoint theory (AFT). This not only widens the scope of AFT from two- to many-valued logics, but allows a wide range of existing AFT results to be applied to fuzzy logic programming. As first examples of such applications, we clarify the formal relationship between existing semantics, generalize the notion of stratification from classical to fuzzy logic programs, and devise “more precise” variants of the semantics.
Human-Readable Neuro-Fuzzy Networks from Frequent Yet Discernible Patterns in Reward-Based Environments
PDF ↗We propose self-organizing and simplifying neuro-fuzzy networks (NFNs) to yield transparent human-readable policies by exploiting fuzzy information granulation and graph theory. Deriving from social network analysis, we retain only the frequent-yet-discernible (FYD) patterns in NFNs and apply them to reward-based scenarios. The effectiveness of NFNs from FYD patterns is shown in classic control and a real-world classroom using an intelligent tutoring system to teach students.
We introduce a relational approach to program synthesis. The key idea is to decompose synthesis tasks into simpler relational synthesis subtasks. Specifically, our representation decomposes a training input-output example into sets of input and output facts respectively. We then learn relations between the input and output facts. We demonstrate our approach using an off-the-shelf inductive logic programming (ILP) system on four challenging synthesis datasets. Our results show that (i) our representation can outperform a standard one, and (ii) an off-the-shelf ILP system with our representation can outperform domain-specific approaches.
In group decisions or deliberations, stakeholders are often confronted with conflicting opinions. We investigate a logic-based way of expressing such opinions and a formal general notion of a middle ground between stakeholders. Inspired by the literature on preferences with hierarchical and lexicographic models, we instantiate our general framework to the case where stakeholders express their opinions using preference statements of the form ‘I prefer ‘a’ to ‘b’’, where ‘a’ and ‘b’ are alternatives expressed over some attributes, e.g., in a trolley problem, one can express I prefer to save 1 adult and 1 child to 2 adults (and 0 children). We prove theoretical results on the existence and uniqueness of middle grounds. In particular, we show that, for preference statements, middle grounds may not exist and may not be unique. We provide algorithms for deciding the existence and finding middle grounds.
Fuzzy description logics serve the representation of vague knowledge, typically letting concepts take truth degrees in the unit interval. Expressiveness, logical properties, and complexity vary strongly with the choice of propositional base. The Łukasiewicz propositional base is generally perceived to have preferable logical properties but often entails high complexity or even undecidability. Contrastingly, the less expressive Zadeh propositional base comes with low complexity but entails essentially no change in logical behaviour compared to the classical case. To strike a balance between these poles, we propose non-expansive fuzzy ALC, in which the Zadeh base is extended with Łukasiewicz connectives where one side is restricted to be a rational constant, that is, with constant shift operators. This allows, for instance, modelling dampened inheritance of properties along roles. We present an unlabelled tableau method for non-expansive fuzzy ALC, which allows reasoning over general TBoxes in EXPTime like in two-valued ALC.
Recent advancements in AI have made LLMs valuable tools for automating the interpretation of textual descriptions of business processes and for converting formal process specifications into natural language. However, there are no practical methodologies or systematic assessments to ensure these automatic translations are faithful. This paper proposes a novel approach, based on an auxiliary bidirectional translation task, to assess LLMs performance quantitatively; also, it also empirically evaluates the performance of state-of-the-art LLMs for bidirectional translations between natural language and declarative formal process specifications. The results reveal substantial variability in performance among the LLMs, highlighting the importance of LLM selection and confirming the need for a robust method for assessing LLMs' outputs.