GenAI4ELab/papercli-papers huggingface dataset:
Exact ASP Counting with Compact Encodings
Authors: Mohimenul Kabir; Supratik Chakraborty; Kuldeep S. Meel
Venue: AAAI 2024 (main)

Abstract: Answer Set Programming (ASP) has emerged as a promising
paradigm in knowledge representation and automated reason-
ing owing to its ability to model hard combinatorial problems
from diverse domains in a natural way. Building on advances
in propositional SAT solving, the past two decades have wit-
nessed the emergence of well-engineered systems for solv-
ing the answer set satisfiability problem, i.e., finding mod-
els or answer sets for a given answer set program. In re-
cent years, there has been growing interest in problems be-
yond satisfiability, such as model counting, in the context of
ASP. Akin to the early days of propositional model count-
ing, state-of-the-art exact answer set counters do not scale
well beyond small instances. Exact ASP counters struggle
with handling larger input formulas. The primary contribu-
tion of this paper is a new ASP counting framework, called
sharpASP, which counts answer sets avoiding larger input
formulas. This relies on an alternative way of defining answer
sets that allows lifting of key techniques developed in the con-
text of propositional model counting. Our extensive empirical
analysis over 1470 benchmarks demonstrates significant per-
formance gain over current state-of-the-art exact answer set
counters. Specifically, by using sharpASP, we were able to
solve 1062 benchmarks with PAR2 score of 3082 whereas
using prior state-of-the-art, we could only solve 895 bench-
marks with PAR2 score of 4205, all other experimental con-
ditions being the same.
Minimal Macro-Based Rewritings of Formal Languages: Theory and Applications in Ontology Engineering (and Beyond)
Authors: Christian Kindermann; Anne-Marie George; Bijan Parsia; Uli Sattler
Venue: AAAI 2024 (main)

Abstract: In this paper, we introduce the problem of rewriting finite formal languages using syntactic macros such that the rewriting is minimal in size. We present polynomial-time algorithms to solve variants of this problem and show their correctness. To demonstrate the practical relevance of the proposed problems and the feasibility and effectiveness of our algorithms in practice, we apply these to biomedical ontologies authored in OWL. We find that such rewritings can significantly reduce the size of ontologies by capturing repeated expressions with macros. This approach not only offers valuable assistance in enhancing ontology quality and comprehension but can also be seen as a general methodology for evaluating features of rewriting systems (including syntactic macros, templates, or other forms of rewriting rules), which can be analyzed in terms of their influence on computational problems.
On the Expressivity of Recurrent Neural Cascades
Authors: Nadezda Alexandrovna Knorozova; Alessandro Ronca
Venue: AAAI 2024 (main)

Abstract: Recurrent Neural Cascades (RNCs) are the recurrent neural networks with no cyclic dependencies among recurrent neurons. This class of recurrent networks has received a lot of attention in practice. Besides training methods for a fixed architecture such as backpropagation, the cascade architecture naturally allows for constructive learning methods, where recurrent nodes are added incrementally one at a time, often yielding smaller networks. Furthermore, acyclicity amounts to a structural prior that even for the same number of neurons yields a more favourable sample complexity compared to a fully-connected architecture.
A central question is whether the advantages of the cascade architecture come at the cost of a reduced expressivity. We provide new insights into this question. We show that the regular languages captured by RNCs with sign and tanh activation with positive recurrent weights are the star-free regular languages. In order to establish our results we developed a novel framework where capabilities of RNCs are assessed by analysing which semigroups and groups a single neuron is able to implement. A notable implication of our framework is that RNCs can achieve the expressivity of all regular languages by introducing neurons that can implement groups.
Efficient Axiomatization of OWL 2 EL Ontologies from Data by Means of Formal Concept Analysis
Authors: Francesco Kriegel
Venue: AAAI 2024 (main)

Abstract: We present an FCA-based axiomatization method that produces a complete OWL 2 EL TBox (the terminological part of an OWL 2 EL ontology) from a graph dataset in at most exponential time.  We describe technical details that allow for efficient implementation as well as variations that dispense with the computation of extremely large axioms, thereby rendering the approach applicable albeit some completeness is lost.  Moreover, we evaluate the prototype on real-world datasets.
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
Authors: Sean Lamont; Michael Norrish; Amir Dezfouli; Christian Walder; Paul Montague
Venue: AAAI 2024 (main)

Abstract: Artificial Intelligence for Theorem Proving (AITP) has given
rise to a plethora of benchmarks and methodologies, particularly in Interactive Theorem Proving (ITP). Research in the
area is fragmented, with a diverse set of approaches being
spread across several ITP systems. This presents a significant challenge to the comparison of methods, which are often
complex and difficult to replicate.
Addressing this, we present BAIT, a framework for the fair
and streamlined comparison of learning approaches in ITP.
We demonstrate BAIT’s capabilities with an in-depth comparison, across several ITP benchmarks, of state-of-the-art
architectures applied to the problem of formula embedding.
We find that Structure Aware Transformers perform particularly well, improving on techniques associated with the original problem sets. BAIT also allows us to assess the end-to-end proving performance of systems built on interactive
environments. This unified perspective reveals a novel end-to-end system that improves on prior work. We also provide
a qualitative analysis, illustrating that improved performance
is associated with more semantically-aware embeddings. By
streamlining the implementation and comparison of Machine
Learning algorithms in the ITP context, we anticipate BAIT
will be a springboard for future research.
INFORMEDQX: Informed Conflict Detection for Over-Constrained Problems
Authors: Viet-Man Le; Alexander Felfernig; Thi Ngoc Trang Tran; Mathias Uta
Venue: AAAI 2024 (main)

Abstract: Conflict detection is relevant in various application scenarios, ranging from interactive decision-making to the diagnosis of faulty knowledge bases. Conflicts can be regarded as sets of constraints that cause an inconsistency. In many scenarios (e.g., constraint-based configuration), conflicts are repeatedly determined for the same or similar sets of constraints. This misses out on the valuable opportunity for leveraging knowledge reuse and related potential performance improvements, which are extremely important, specifically interactive constraint-based applications. In this paper, we show how to integrate knowledge reuse concepts into non-instructive conflict detection. We introduce the InformedQX algorithm, which is a reuse-aware variant of QuickXPlain. The results of a related performance analysis with the Linux-2.6.3.33 configuration knowledge base show significant improvements in terms of runtime performance compared to QuickXPlain.
Abstraction of Situation Calculus Concurrent Game Structures
Authors: Yves Lesperance; Giuseppe De Giacomo; Maryam Rostamigiv; Shakil M. Khan
Venue: AAAI 2024 (main)

Abstract: We present a general framework for abstracting agent behavior in multi-agent synchronous games in the situation calculus, which provides a first-order representation of the state and allows us to model how plays depend on the data and objects involved.  We represent such games as action theories of a special form called situation calculus synchronous game structures (SCSGSs), in which we have a single action "tick" whose effects depend on the combination of moves selected by the players.  In our framework, one specifies both an abstract SCSGS and a concrete SCSGS, as well as a refinement mapping that specifies how each abstract move is implemented by a Golog program defined over the concrete SCSGS.  We define notions of sound and complete abstraction with respect to a mapping over such SCSGS.  To express strategic properties on the abstract and concrete games we adopt a first-order variant of alternating-time mu-calculus mu-ATL-FO.  We show that we can exploit abstraction in verifying mu-ATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.
Relational Programming with Foundational Models
Authors: Ziyang Li; Jiani Huang; Jason Liu; Felix Zhu; Eric Zhao; William Dodds; Neelay Velingker; Rajeev Alur; Mayur Naik
Venue: AAAI 2024 (main)

Abstract: Foundation models have vast potential to enable diverse AI applications. The powerful yet incomplete nature of these models has spurred a wide range of mechanisms to augment them with capabilities such as in-context learning, information retrieval, and code interpreting. We propose Vieira, a declarative framework that unifies these mechanisms in a general solution for programming with foundation models. Vieira follows a probabilistic relational paradigm and treats foundation models as stateless functions with relational inputs and outputs. It supports neuro-symbolic applications by enabling the seamless combination of such models with logic programs, as well as complex, multi-modal applications by streamlining the composition of diverse sub-models. We implement Vieira by extending the Scallop compiler with a foreign interface that supports foundation models as plugins. We implement plugins for 12 foundation models including GPT, CLIP, and SAM. We evaluate Vieira on 9 challenging tasks that span language, vision, and structured and vector databases. Our evaluation shows that programs in Vieira are concise, can incorporate modern foundation models, and have comparable or better accuracy than competitive baselines.
MINES: Message Intercommunication for Inductive Relation Reasoning over Neighbor-Enhanced Subgraphs
Authors: Ke Liang; Lingyuan Meng; Sihang Zhou; Wenxuan Tu; Siwei Wang; Yue Liu; Meng Liu; Long Zhao; Xiangjun Dong; Xinwang Liu
Venue: AAAI 2024 (main)

Abstract: GraIL and its variants have shown their promising capacities for inductive relation reasoning on knowledge graphs. However, the uni-directional message-passing mechanism hinders such models from exploiting hidden mutual relations between entities in directed graphs. Besides, the enclosing subgraph extraction in most GraIL-based models restricts the model from extracting enough discriminative information for reasoning. Consequently, the expressive ability of these models is limited. To address the problems, we propose a novel GraIL-based framework, termed MINES, by introducing a Message Intercommunication mechanism on the Neighbor-Enhanced Subgraph. Concretely, the message intercommunication mechanism is designed to capture the omitted hidden mutual information. It introduces bi-directed information interactions between connected entities by inserting an undirected/bi-directed GCN layer between uni-directed RGCN layers. Moreover, inspired by the success of involving more neighbors in other graph-based tasks, we extend the neighborhood area beyond the enclosing subgraph to enhance the information collection for inductive relation reasoning. Extensive experiments prove the promising capacity of the proposed MINES from various aspects, especially for the superiority, effectiveness, and transfer ability.
Auditable Algorithms for Approximate Model Counting
Authors: Kuldeep S. Meel; Supratik Chakraborty; S. Akshay
Venue: AAAI 2024 (main)

Abstract: The problem of model counting, i.e., counting satisfying assignments of a Boolean formula, is a fundamental problem in computer science, with diverse applications. Given #P-hardness of the problem, many algorithms have been developed over the years to provide an approximate model count. Recently, building on the practical success of SAT-solvers used as NP oracles, the focus has shifted from theory to practical implementations of such algorithms. This has brought to focus new challenges. In this paper, we consider one such challenge – that of auditable deterministic approximate model counters wherein a counter should also generate a certificate, which allows a user (often with limited computational power) to independently audit whether the count returned by an invocation of the algorithm is indeed within the promised bounds. 

We start by examining a celebrated approximate model counting algorithm due to Stockmeyer that uses polynomially many calls to a \Sigma^2_P oracle, and show that it can be audited via a \Pi^2_P formula on (n^2 log^2 n) variables, where n is the number of variables in the original formula. Since n is often large (10’s to 100’s of thousands) for typical instances, we ask if the count of variables in the certificate formula can be reduced – a critical question towards potential implementation. We show that this improvement in certification can be achieved with a tradeoff in the counting algorithm’s complexity. Specifically, we develop new deterministic approximate model counting algorithms that invoke a \Sigma^3_P oracle, but can be certified using a \Pi^2_P formula on fewer variables: our final algorithm uses just (n log n) variables.

Our study demonstrates that one can simplify certificate checking significantly if we allow the counting algorithm to access a slightly more powerful oracle. We believe this shows for the first time how the audit complexity can be traded for the complexity of approximate counting.
A General Theoretical Framework for Learning Smallest Interpretable Models
Authors: Sebastian Ordyniak; Giacomo Paesani; Mateusz Rychlicki; Stefan Szeider
Venue: AAAI 2024 (main)

Abstract: We develop a general algorithmic framework that allows us to obtain fixed-parameter tractability for computing smallest symbolic models that represent given data. Our framework applies to all ML model types that admit a certain extension property. By showing this extension property for decision trees, decision sets, decision lists, and binary decision diagrams, we obtain that minimizing these fundamental model types is fixed-parameter tractable. Our framework even applies to ensembles, which combine individual models by majority decision.
Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis
Authors: Julian Parsert; Elizabeth Polgreen
Venue: AAAI 2024 (main)

Abstract: Program synthesis is the task of automatically generating code based on a specification. In Syntax-Guided Synthesis (SyGuS) this specification is a combination of a syntactic template and a logical formula, and the result is guaranteed to satisfy both. We present a reinforcement-learning guided algorithm for SyGuS which uses Monte-Carlo Tree Search (MCTS) to search the space of candidate solutions. Our algorithm learns policy and value functions which, combined with the upper confidence bound for trees, allow it to balance exploration and exploitation. A common challenge in applying machine learning approaches to syntax-guided synthesis is the scarcity of training data. To address this, we present a method for automatically generating training data for SyGuS based on anti-unification of existing first-order satisfiability problems, which we use to train our MCTS policy. We implement and evaluate this setup and demonstrate that learned policy and value improve the synthesis performance over a baseline by over 26 percentage points in the training and testing sets. Our tool outperforms state-of-the-art tool cvc5 on the training set and performs comparably in terms of the total number of problems solved on the testing set (solving 23% of the benchmarks on which cvc5 fails). We make our data set publicly available, to enable further application of machine learning methods to the SyGuS problem.
Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories
Authors: Andoni Rodríguez; César Sánchez
Venue: AAAI 2024 (main)

Abstract: Reactive synthesis is the process of generate correct con- trollers from temporal logic specifications. Typically, synthesis is restricted to Boolean specifications in LTL. Recently, a Boolean abstraction technique allows to translate LTLT specifications that contain literals in theories into equi-realizable LTL specifications, but no full synthesis procedure exists yet. In synthesis modulo theories, the system receives valuations of environment variables (from a first-order theory T ) and outputs valuations of system variables from T . In this paper, we address how to syntheize a full controller using a combination of the static Boolean controller obtained from the Booleanized LTL specification together with on-the-fly queries to a solver that produces models of satisfiable existential T formulae. This is the first synthesis method for LTL modulo theories. Additionally, our method can produce adaptive responses which increases explainability and can improve runtime properties like performance. Our approach is applicable to both LTL modulo theories and LTLf modulo theories.
A Unified View on Forgetting and Strong Equivalence Notions in Answer Set Programming
Authors: Zeynep G. Saribatur; Stefan Woltran
Venue: AAAI 2024 (main)

Abstract: Answer Set Programming (ASP) is a prominent rule-based language for knowledge representation and reasoning with roots in logic programming and non-monotonic reasoning. The aim to capture the essence of removing (ir)relevant details in ASP programs led to the investigation of different notions, from strong persistence (SP) forgetting, to faithful abstractions, and, recently, strong simplifications, where the latter two can be seen as relaxed and strengthened notions of forgetting, respectively. Although it was observed that these notions are related, especially given that they have characterizations through the semantics for strong equivalence, it remained unclear whether they can be brought together. In this work, we bridge this gap by introducing a novel relativized equivalence notion, which is a relaxation of the recent simplification notion, that is able to capture all related notions from the literature. We provide the necessary and sufficient conditions for relativized simplifiability, which shows that the challenging part is for when the context programs do not contain all the atoms to remove. We then introduce an operator that combines projection and a relaxation of SP-forgetting to obtain the relativized simplifications. We furthermore provide complexity results that complete the overall picture.
BeliefFlow: A Framework for Logic-Based Belief Diffusion via Iterated Belief Change
Authors: Nicolas Schwind; Katsumi Inoue; Sébastien Konieczny; Pierre Marquis
Venue: AAAI 2024 (main)

Abstract: This paper presents BeliefFlow, a novel framework for representing how logical beliefs spread among interacting agents within a network. In a Belief Flow Network (BFN), agents communicate asynchronously. The agents' beliefs are represented using epistemic states, which encompass their current beliefs and conditional beliefs guiding future changes. When communication occurs between two connected agents, the receiving agent changes its epistemic state using an improvement operator, a well-known type of rational iterated belief change operator that generalizes belief revision operators. We show that BFNs satisfy appealing properties, leading to two significant outcomes. First, in any BFN with strong network connectivity, the beliefs of all agents converge towards a global consensus. Second, within any BFN, we show that it is possible to compute an optimal strategy for influencing the global beliefs. This strategy, which involves controlling the beliefs of a least number of agents through bribery, can be identified from the topology of the network and can be computed in polynomial time.
NegVSR: Augmenting Negatives for Generalized Noise Modeling in Real-world Video Super-Resolution
Authors: Yexing Song; Meilin Wang; Zhijing Yang; Xiaoyu Xian; Yukai Shi
Venue: AAAI 2024 (main)

Abstract: The capability of video super-resolution (VSR) to synthesize high-resolution (HR) video from ideal datasets has been demonstrated in many works. However, applying the VSR model to real-world video with unknown and complex degradation remains a challenging task. First, existing degradation metrics in most VSR methods are not able to effectively simulate real-world noise and blur. On the contrary, simple combinations of classical degradation are used for real-world noise modeling, which led to the VSR model often being violated by out-of-distribution noise. Second, many SR models focus on noise simulation and transfer. Nevertheless, the sampled noise is monotonous and limited. To address the aforementioned problems, we propose a Negatives augmentation strategy for generalized noise modeling in Video Super-Resolution (NegVSR) task. Specifically, we first propose sequential noise generation toward real-world data to extract practical noise sequences. Then, the degeneration domain is widely expanded by negative augmentation to build up various yet challenging real-world noise sets. We further propose the augmented negative guidance loss to learn robust features among augmented negatives effectively. Extensive experiments on real-world datasets (e.g., VideoLQ and FLIR) show that our method outperforms state-of-the-art methods with clear margins, especially in visual quality. Project page is available at: https://negvsr.github.io/.
Scalable Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming
Authors: Giang Trinh; Belaid Benhamou; Samuel Pastva; Sylvain Soliman
Venue: AAAI 2024 (main)

Abstract: Boolean Networks (BNs) are widely used as a modeling formalism in several domains, notably systems biology and computer science. A fundamental problem in BN analysis is the enumeration of trap spaces, which are hypercubes in the state space that cannot be escaped once entered. Several methods have been proposed for enumerating trap spaces, however they often suffer from scalability and efficiency issues, particularly for large and complex models. To our knowledge, the most efficient and recent methods for the trap space enumeration all rely on Answer Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated by these considerations, our work proposes a new method for enumerating trap spaces in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+ randomly generated BNs, showing that it enables analysis of models beyond the capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).
Non-flat ABA Is an Instance of Bipolar Argumentation
Authors: Markus Ulbricht; Nico Potyka; Anna Rapberger; Francesca Toni
Venue: AAAI 2024 (main)

Abstract: Assumption-based Argumentation (ABA) is a well-known structured argumentation formalism, whereby arguments and attacks between them are drawn from rules, defeasible assumptions and their contraries. 
A common restriction imposed on ABA frameworks (ABAFs) is that they are flat, i.e. each of the defeasible assumptions can only be assumed, but not derived. While it is known that flat ABAFs can be translated into abstract argumentation frameworks (AFs) as proposed by Dung, no translation exists from general, possibly non-flat ABAFs into any kind of abstract argumentation formalism. 
In this paper, we close this gap and show that bipolar AFs (BAFs) can instantiate general ABAFs. To this end we develop suitable, novel BAF semantics which borrow from the notion of deductive support. We investigate basic properties of our BAFs, including computational complexity, and prove the desired relation to ABAFs under several semantics.