https://arxiv.org/api/OVUC/j3T+gFHnUJBDps1sEI4iF8 2026-04-15T09:35:36Z 3075 645 15 http://arxiv.org/abs/2401.08455v2 2024-05-23T19:16:28Z

This paper proposes ideas to speed up the process of creative telescoping, particularly when the telescoper is reducible. One can interpret telescoping as computing an annihilator $L \in D$ for an element $m$ in a $D$-module $M$. The main idea is to look for submodules of $M$. If $N$ is a non-trivial submodule of $M$, constructing the minimal operator $R$ of the image of $m$ in $M/N$ gives a right-factor of $L$ in $D$. Then $L = L' R$ where the left-factor $L'$ is the telescoper of $R(m) \in N$. To expedite computing $L'$, compute the action of $D$ on a natural basis of $N$, then obtain $L'$ with a cyclic vector computation. The next main idea is that when $N$ has automorphisms, use them to construct submodules. An automorphism with distinct eigenvalues can be used to decompose $N$ as a direct sum $N_1 \oplus \cdots \oplus N_k$. Then $L'$ is the LCLM (Least Common Left Multiple) of $L_1, \ldots, L_k$ where $L_i$ is the telescoper of the projection of $R(m)$ on $N_i$. An LCLM can greatly increase the degrees of coefficients, so $L'$ and $L$ can be much larger expressions than the factors $L_1,\ldots,L_k$ and $R$. Examples show that computing each factor $L_i$ and $R$ seperately can save a lot of CPU time compared to computing $L$ in expanded form with standard creative telescoping.

2024-01-16T15:59:40Z 10 pages Mark van Hoeij http://arxiv.org/abs/2405.14133v1 2024-05-23T03:12:49Z

Class-imbalanced node classification tasks are prevalent in real-world scenarios. Due to the uneven distribution of nodes across different classes, learning high-quality node representations remains a challenging endeavor. The engineering of loss functions has shown promising potential in addressing this issue. It involves the meticulous design of loss functions, utilizing information about the quantities of nodes in different categories and the network's topology to learn unbiased node representations. However, the design of these loss functions heavily relies on human expert knowledge and exhibits limited adaptability to specific target tasks. In this paper, we introduce a high-performance, flexible, and generalizable automated loss function search framework to tackle this challenge. Across 15 combinations of graph neural networks and datasets, our framework achieves a significant improvement in performance compared to state-of-the-art methods. Additionally, we observe that homophily in graph-structured data significantly contributes to the transferability of the proposed framework.

2024-05-23T03:12:49Z ICML 2024 Xinyu Guo Kai Wu Xiaoyu Zhang Jing Liu http://arxiv.org/abs/2403.04919v2 2024-05-22T21:43:39Z

We study the identification of causal effects, motivated by two improvements to identifiability which can be attained if one knows that some variables in a causal graph are functionally determined by their parents (without needing to know the specific functions). First, an unidentifiable causal effect may become identifiable when certain variables are functional. Second, certain functional variables can be excluded from being observed without affecting the identifiability of a causal effect, which may significantly reduce the number of needed variables in observational data. Our results are largely based on an elimination procedure which removes functional variables from a causal graph while preserving key properties in the resulting causal graph, including the identifiability of causal effects.

2024-03-07T22:04:35Z Yizuo Chen Adnan Darwiche http://arxiv.org/abs/2405.11412v1 2024-05-18T23:17:00Z

Recent attention to relational knowledge bases has sparked a demand for understanding how relations change between entities. Petri nets can represent knowledge structure and dynamically simulate interactions between entities, and thus they are well suited for achieving this goal. However, logic programs struggle to deal with extensive Petri nets due to the limitations of high-level symbol manipulations. To address this challenge, we introduce a novel approach called Boolean Matrix Logic Programming (BMLP), utilising boolean matrices as an alternative computation mechanism for Prolog to evaluate logic programs. Within this framework, we propose two novel BMLP algorithms for simulating a class of Petri nets known as elementary nets. This is done by transforming elementary nets into logically equivalent datalog programs. We demonstrate empirically that BMLP algorithms can evaluate these programs 40 times faster than tabled B-Prolog, SWI-Prolog, XSB-Prolog and Clingo. Our work enables the efficient simulation of elementary nets using Prolog, expanding the scope of analysis, learning and verification of complex systems with logic programming techniques.

2024-05-18T23:17:00Z arXiv admin note: text overlap with arXiv:2405.06724 Lun Ai Stephen H. Muggleton Shi-Shun Liang Geoff S. Baldwin http://arxiv.org/abs/2405.10215v1 2024-05-16T16:05:21Z

SMLP: Symbolic Machine Learning Prover an open source tool for exploration and optimization of systems represented by machine learning models. SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint and NN solvers. In addition its exploration methods are guided by probabilistic and statistical methods. SMLP is a general purpose tool that requires only data suitable for ML modelling in the csv format (usually samples of the system's input/output). SMLP has been applied at Intel for analyzing and optimizing hardware designs at the analog level. Currently SMLP supports NNs, polynomial and tree models, and uses SMT solvers for reasoning and optimization at the backend, integration of specialized NN solvers is in progress.

2024-05-16T16:05:21Z arXiv admin note: text overlap with arXiv:2402.01415 Franz Brauße Zurab Khasidashvili Konstantin Korovin http://arxiv.org/abs/2405.10188v1 2024-05-16T15:31:37Z

Interactive theorem provers, like Isabelle/HOL, Coq and Lean, have expressive languages that allow the formalization of general mathematical objects and proofs. In this context, an important goal is to reduce the time and effort needed to prove theorems. A significant means of achieving this is by improving proof automation. We have implemented an early prototype of proof automation for equational reasoning in Lean by using equality saturation. To achieve this, we need to bridge the gap between Lean's expression semantics and the syntactically driven e-graphs in equality saturation. This involves handling bound variables, implicit typing, as well as Lean's definitional equality, which is more general than syntactic equality and involves notions like $α$-equivalence, $β$-reduction, and $η$-reduction. In this extended abstract, we highlight how we attempt to bridge this gap, and which challenges remain to be solved. Notably, while our techniques are partially unsound, the resulting proof automation remains sound by virtue of Lean's proof checking.

2024-05-16T15:31:37Z Accepted for EGRAPHS-2024 Marcus Rossel Andrés Goens http://arxiv.org/abs/2405.09689v1 2024-05-15T20:37:48Z

Deep learning has achieved remarkable success in recent years. Central to its success is its ability to learn representations that preserve task-relevant structure. However, massive energy, compute, and data costs are required to learn general representations. This paper explores Hyperdimensional Computing (HDC), a computationally and data-efficient brain-inspired alternative. HDC acts as a bridge between connectionist and symbolic approaches to artificial intelligence (AI), allowing explicit specification of representational structure as in symbolic approaches while retaining the flexibility of connectionist approaches. However, HDC's simplicity poses challenges for encoding complex compositional structures, especially in its binding operation. To address this, we propose Generalized Holographic Reduced Representations (GHRR), an extension of Fourier Holographic Reduced Representations (FHRR), a specific HDC implementation. GHRR introduces a flexible, non-commutative binding operation, enabling improved encoding of complex data structures while preserving HDC's desirable properties of robustness and transparency. In this work, we introduce the GHRR framework, prove its theoretical properties and its adherence to HDC properties, explore its kernel and binding characteristics, and perform empirical experiments showcasing its flexible non-commutativity, enhanced decoding accuracy for compositional structures, and improved memorization capacity compared to FHRR.

2024-05-15T20:37:48Z Calvin Yeung Zhuowen Zou Mohsen Imani http://arxiv.org/abs/2405.09232v1 2024-05-15T10:26:24Z

Loop invariants are properties of a program loop that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, the generation of invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this work, we study the more general case where the polynomials exhibit arbitrary degrees. Applying tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants for a while loop, up to a specified degree. These algorithms differ based on whether the initial values of the loop variables are given or treated as parameters. Furthermore, we introduce various methods to address cases where the algebraic problem exceeds the computational capabilities of our methods. In such instances, we identify alternative approaches to generate specific polynomial invariants.

2024-05-15T10:26:24Z 10 pages, 1 figure Erdenebayar Bayarmagnai Fatemeh Mohammadi Rémi Prébet http://arxiv.org/abs/2405.08964v1 2024-05-14T21:10:16Z

The ideal of the arc scheme of a double point or, equivalently, the differential ideal generated by the ideal of a double point is a primary ideal in an infinite-dimensional polynomial ring supported at the origin. This ideal has a rich combinatorial structure connecting it to singularity theory, partition identities, representation theory, and differential algebra. Macaulay inverse system is a powerful tool for studying the structure of primary ideals which describes an ideal in terms of certain linear differential operators. In the present paper, we show that the inverse system of the ideal of the arc scheme of a double point is precisely a vector space spanned by all the Wronskians of the variables and their formal derivatives. We then apply this characterization to extend our recent result on Poincaré-type series for such ideals.

2024-05-14T21:10:16Z Rida Ait El Manssour Gleb Pogudin http://arxiv.org/abs/2405.06387v2 2024-05-13T12:57:38Z

Real-time systems (RTSs) are at the heart of numerous safety-critical applications. An RTS typically consists of a set of real-time tasks (the software) that execute on a multicore shared-memory platform (the hardware) following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events produced by tasks on different cores, is crucial. While efficient techniques to over-approximate such bounds exist, little has been proposed to compute their exact values. Given an RTS with a set of cores C and a set of tasks T , under partitioned fixed-priority scheduling with limited preemption, a recent work by Foughali, Hladik and Zuepke (FHZ) models tasks with affinity c (i.e., allocated to core c in C) as a Uppaal timed automata (TA) network Nc. For each core c in C, Nc integrates blocking (due to data sharing) using tight analytical formulae. Through compositional model checking, FHZ achieved a substantial gain in scalability for bounds local to a core. However, computing inter-core bounds for some events of interest E, produced by a subset of tasks TE with different affinities CE, requires model checking the parallel composition of all TA networks Nc for each c in CE, which produces a large, often intractable, state space. In this paper, we present a new scalable approach based on exact abstractions to compute exact inter-core bounds in a schedulable RTS, under the assumption that tasks in TE have distinct affinities. We develop a novel algorithm, leveraging a new query that we implement in Uppaal, that computes for each TA network Nc in NE an abstraction A(Nc) preserving the exact intervals within which events occur on c, therefore drastically reducing the state space. The scalability of our approach is demonstrated on the WATERS 2017 industrial challenge, for which we efficiently compute various types of inter-core bounds where FHZ fails to scale.

2024-05-10T10:49:41Z To appear in the proceedings of the 48th IEEE International Conference on Computers, Software, and Applications (COMPSAC 2024) Mohammed Aristide Foughali Marius Mikučionis Maryline Zhang 10.1109/COMPSAC61105.2024.00019 http://arxiv.org/abs/2311.03783v2 2024-05-11T14:58:59Z

Embodied AI is one of the most popular studies in artificial intelligence and robotics, which can effectively improve the intelligence of real-world agents (i.e. robots) serving human beings. Scene knowledge is important for an agent to understand the surroundings and make correct decisions in the varied open world. Currently, knowledge base for embodied tasks is missing and most existing work use general knowledge base or pre-trained models to enhance the intelligence of an agent. For conventional knowledge base, it is sparse, insufficient in capacity and cost in data collection. For pre-trained models, they face the uncertainty of knowledge and hard maintenance. To overcome the challenges of scene knowledge, we propose a scene-driven multimodal knowledge graph (Scene-MMKG) construction method combining conventional knowledge engineering and large language models. A unified scene knowledge injection framework is introduced for knowledge representation. To evaluate the advantages of our proposed method, we instantiate Scene-MMKG considering typical indoor robotic functionalities (Manipulation and Mobility), named ManipMob-MMKG. Comparisons in characteristics indicate our instantiated ManipMob-MMKG has broad superiority in data-collection efficiency and knowledge quality. Experimental results on typical embodied tasks show that knowledge-enhanced methods using our instantiated ManipMob-MMKG can improve the performance obviously without re-designing model structures complexly. Our project can be found at https://sites.google.com/view/manipmob-mmkg

2023-11-07T08:06:27Z 14 pages, 6 figures Song Yaoxian Sun Penglei Liu Haoyu Li Zhixu Song Wei Xiao Yanghua Zhou Xiaofang http://arxiv.org/abs/2405.05294v1 2024-05-08T10:03:50Z

Many aspects of human learning have been proposed as a process of constructing mental programs: from acquiring symbolic number representations to intuitive theories about the world. In parallel, there is a long-tradition of using information processing to model human cognition through Rate Distortion Theory (RDT). Yet, it is still poorly understood how to apply RDT when mental representations take the form of programs. In this work, we adapt RDT by proposing a three way trade-off among rate (description length), distortion (error), and computational costs (search budget). We use simulations on a melody task to study the implications of this trade-off, and show that constructing a shared program library across tasks provides global benefits. However, this comes at the cost of sensitivity to curricula, which is also characteristic of human learners. Finally, we use methods from partial information decomposition to generate training curricula that induce more effective libraries and better generalization.

2024-05-08T10:03:50Z CogSci 2024 Hanqi Zhou David G. Nagy Charley M. Wu http://arxiv.org/abs/2405.04842v1 2024-05-08T06:31:14Z

We reexamine Smale's alpha theory as a way to certify a numerical solution to an analytic system. For a given point and a system, Smale's alpha theory determines whether Newton's method applied to this point shows the quadratic convergence to an exact solution. We introduce the alpha theory computation using interval arithmetic to avoid costly exact arithmetic. As a straightforward variation of the alpha theory, our work improves computational efficiency compared to software employing the traditional alpha theory.

2024-05-08T06:31:14Z Accepted for the Proceedings of ICMS 2024 Kisun Lee http://arxiv.org/abs/2405.04297v1 2024-05-07T13:12:49Z

Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.

2024-05-07T13:12:49Z Nils Froleyks Emily Yu Armin Biere Keijo Heljanko http://arxiv.org/abs/2112.05023v2 2024-05-07T07:24:37Z

Solving a system of $m$ multivariate quadratic equations in $n$ variables over finite fields (the MQ problem) is one of the important problems in the theory of computer science. The XL algorithm (XL for short) is a major approach for solving the MQ problem with linearization over a coefficient field. Furthermore, the hybrid approach with XL (h-XL) is a variant of XL guessing some variables beforehand. In this paper, we present a variant of h-XL, which we call the \textit{polynomial XL (PXL)}. In PXL, the whole $n$ variables are divided into $k$ variables to be fixed and the remaining $n-k$ variables as ``main variables'', and we generate a Macaulay matrix with respect to the $n-k$ main variables over a polynomial ring of the $k$ (sub-)variables. By eliminating some columns of the Macaulay matrix over the polynomial ring before guessing $k$ variables, the amount of operations required for each guessed value can be reduced compared with h-XL. Our complexity analysis of PXL (under some practical assumptions and heuristics) gives a new theoretical bound, and it indicates that PXL could be more efficient than other algorithms in theory on the random system with $n=m$, which is the case of general multivariate signatures. For example, on systems over the finite field with ${2^8}$ elements with $n=m=80$, the numbers of operations deduced from the theoretical bounds of the hybrid approaches with XL and Wiedemann XL, Crossbred, and PXL with optimal $k$ are estimated as $2^{252}$, $2^{234}$, $2^{237}$, and $2^{220}$, respectively.

2021-12-09T16:30:48Z 35 pages, 1 figure Proceedings of PQCrypto 2024 Hiroki Furue Momonari Kudo