https://arxiv.org/api/eyHbIMb1lBfjiTGmhsWmZMumGMo 2026-06-14T07:35:39Z 3138 285 15 http://arxiv.org/abs/2510.11561v1 2025-10-13T16:04:06Z

In this paper, we present Ontolearn-a framework for learning OWL class expressions over large knowledge graphs. Ontolearn contains efficient implementations of recent stateof-the-art symbolic and neuro-symbolic class expression learners including EvoLearner and DRILL. A learned OWL class expression can be used to classify instances in the knowledge graph. Furthermore, Ontolearn integrates a verbalization module based on an LLM to translate complex OWL class expressions into natural language sentences. By mapping OWL class expressions into respective SPARQL queries, Ontolearn can be easily used to operate over a remote triplestore. The source code of Ontolearn is available at https://github.com/dice-group/Ontolearn.

2025-10-13T16:04:06Z Journal of Machine Learning Research 26 (2025) 1-6 Caglar Demir Alkid Baci N'Dah Jean Kouagou Leonie Nora Sieger Stefan Heindorf Simon Bin Lukas Blübaum Alexander Bigerl Axel-Cyrille Ngonga Ngomo http://arxiv.org/abs/2510.11212v1 2025-10-13T09:46:33Z

Motivated by better understanding the bideterminant (=product of minors) basis on the polynomial ring in $n \times m$ variables, we develop theory \& algorithms for Gröbner bases in not only algebras with straightening law (ASLs or Hodge algebras), but in any commutative algebra over a field that comes equipped with a notion of "monomial" (generalizing the standard monomials of ASLs) and a suitable term order. Rather than treating such an algebra $A$ as a quotient of a polynomial ring and then "lifting" ideals from $A$ to ideals in the polynomial ring, the theory we develop is entirely "native" to $A$ and its given notion of monomial. When applied to the case of bideterminants, this enables us to package several standard results on bideterminants in a clean way that enables new results. In particular, once the theory is set up, it lets us give an almost-trivial proof of a universal Gröbner basis (in our sense) for the ideal of $t$-minors for any $t$. We note that here it was crucial that theory be native to $A$ and its given monomial structure, as in the standard monomial structure given by bideterminants each $t$-minor is a single variable rather than a sum of $t!$ many terms (in the "ordinary monomial" structure).

2025-10-13T09:46:33Z 107 pages, 0 figures Joshua A. Grochow Abhiram Natarajan http://arxiv.org/abs/2412.20630v2 2025-10-09T20:02:32Z

A sequence is difference algebraic (or D-algebraic) if finitely many shifts of its general term satisfy a polynomial relationship; that is, they are the coordinates of a generic point on an affine hypersurface. The corresponding equations are denoted algebraic difference equations (ADEs). We propose a formal definition of D-algebraicity for sequences and investigate algorithms for their closure properties. We show that subsequences of D-algebraic sequences, indexed by arithmetic progressions, satisfy ADEs of the same orders as the original sequences. Additionally, we discuss the special difference-algebraic nature of holonomic and $C^2$-finite sequences.

2024-12-30T00:39:57Z 29 pages, 1 figure. More comprehensive version. Specific results for $C^2$-finite sequences Bertrand Teguia Tabuguia http://arxiv.org/abs/2510.08336v1 2025-10-09T15:23:49Z

Tensors are fundamental in mathematics, computer science, and physics. Their study through algebraic geometry and representation theory has proved very fruitful in the context of algebraic complexity theory and quantum information. In particular, moment polytopes have been understood to play a key role. In quantum information, moment polytopes (also known as entanglement polytopes) provide a framework for the single-particle quantum marginal problem and offer a geometric characterization of entanglement. In algebraic complexity, they underpin quantum functionals that capture asymptotic tensor relations. More recently, moment polytopes have also become foundational to the emerging field of scaling algorithms in computer science and optimization. Despite their fundamental role and interest from many angles, much is still unknown about these polytopes, and in particular for tensors beyond $\mathbb{C}^2\otimes\mathbb{C}^2\otimes\mathbb{C}^2$ and $\mathbb{C}^2\otimes\mathbb{C}^2\otimes\mathbb{C}^2\otimes\mathbb{C}^2$ only sporadically have they been computed. We give a new algorithm for computing moment polytopes of tensors (and in fact moment polytopes for the general class of reductive algebraic groups) based on a mathematical description by Franz (J. Lie Theory 2002). This algorithm enables us to compute moment polytopes of tensors of dimension an order of magnitude larger than previous methods, allowing us to compute with certainty, for the first time, all moment polytopes of tensors in $\mathbb{C}^3\otimes\mathbb{C}^3\otimes\mathbb{C}^3$, and with high probability those in $\mathbb{C}^4\otimes\mathbb{C}^4\otimes\mathbb{C}^4$ (which includes the $2\times 2$ matrix multiplication tensor). We discuss how these explicit moment polytopes have led to several new theoretical directions and results.

2025-10-09T15:23:49Z Maxim van den Berg Matthias Christandl Vladimir Lysikov Harold Nieuwboer Michael Walter Jeroen Zuiddam http://arxiv.org/abs/2309.15458v4 2025-10-09T05:36:43Z

Integrating first-order logic constraints (FOLCs) with neural networks is a crucial but challenging problem since it involves modeling intricate correlations to satisfy the constraints. This paper proposes a novel neural layer, LogicMP, whose layers perform mean-field variational inference over an MLN. It can be plugged into any off-the-shelf neural network to encode FOLCs while retaining modularity and efficiency. By exploiting the structure and symmetries in MLNs, we theoretically demonstrate that our well-designed, efficient mean-field iterations effectively mitigate the difficulty of MLN inference, reducing the inference from sequential calculation to a series of parallel tensor operations. Empirical results in three kinds of tasks over graphs, images, and text show that LogicMP outperforms advanced competitors in both performance and efficiency.

2023-09-27T07:52:30Z 28 pages, 14 figures, 12 tables Weidi Xu Jingwei Wang Lele Xie Jianshan He Hongting Zhou Taifeng Wang Xiaopei Wan Jingdong Chen Chao Qu Wei Chu http://arxiv.org/abs/2510.05863v1 2025-10-07T12:32:29Z

We develop a Koopman operator framework for studying the {computational properties} of dynamical systems. Specifically, we show that the resolvent of the Koopman operator provides a natural abstraction of halting, yielding a ``Koopman halting problem that is recursively enumerable in general. For symbolic systems, such as those defined on Cantor space, this operator formulation captures the reachability between clopen sets, while for equicontinuous systems we prove that the Koopman halting problem is decidable. Our framework demonstrates that absorbing (halting) states {in finite automata} correspond to Koopman eigenfunctions with eigenvalue one, while cycles in the transition graph impose algebraic constraints on spectral properties. These results provide a unifying perspective on computation in symbolic and analog systems, showing how computational universality is reflected in operator spectra, invariant subspaces, and algebraic structures. Beyond symbolic dynamics, this operator-theoretic lens opens pathways to analyze {computational power of} a broader class of dynamical systems, including polynomial and analog models, and suggests that computational hardness may admit dynamical signatures in terms of Koopman spectral structure.

2025-10-07T12:32:29Z 13 pages double column; two figures Francesco Caravelli Jean-Charles Delvenne http://arxiv.org/abs/2411.03070v2 2025-10-06T09:49:30Z

The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cylindrical algebraic covering method to allow for checking the truth of arbitrary non-linear arithmetic formulas, adding support for both quantifiers and Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. After introducing the algorithm, we elaborate on various extensions, optimizations and heuristics. Finally, we present an experimental evaluation of our implementation and provide a comparison with state-of-the-art SMT solvers and quantifier elimination tools.

2024-11-05T13:06:52Z Jasper Nalbach Gereon Kremer http://arxiv.org/abs/2510.03103v1 2025-10-03T15:31:30Z

An efficient method is proposed for computing the structure of Jordan blocks of a matrix of integers or rational numbers by exact computation. We have given a method for computing Jordan chains of a matrix with exact computation. However, for deriving just the structure of Jordan chains, the algorithm can be reduced to increase its efficiency. We propose a modification of the algorithm for that purpose. Results of numerical experiments are given.

2025-10-03T15:31:30Z 19 pages Shinichi Tajima Katsuyoshi Ohara Akira Terui http://arxiv.org/abs/2510.01568v2 2025-10-03T00:34:35Z

This paper presents a novel algorithm for constructing a sum-of-squares (SOS) decomposition for positive semi-definite polynomials with rational coefficients. Unlike previous methods that typically yield SOS decompositions with floating-point coefficients, our approach ensures that all coefficients in the decomposition remain rational. This is particularly useful in formal verification and symbolic computation, where exact arithmetic is required. We introduce a stepwise reduction technique that transforms a given polynomial into a sum of ladder-like squares while preserving rationality. Experimental results demonstrate the effectiveness of our method compared to existing numerical approaches. This artical is an extension of the following Chinnese paper: HUANG Yong , ZENG Zhenbing , YANG Lu , RAO Yongsheng. An Algorithm to Represent Positive Semi-Definite Polynomials to Sum of Lader-Like Squares of Polynomials with Rational Coefficients (in Chinese). Journal of Systems Science and Mathematical Sciences, 2024, 44(5): 1241-1271 https://doi.org/10.12341/jssms23584CM

2025-10-02T01:26:40Z 37 pages Zhenbing Zeng Yong Huang Lu Yang Yongsheng Rao http://arxiv.org/abs/2510.02551v1 2025-10-02T20:40:09Z

This paper presents a novel approach to finding analytical approximations for bright-soliton solutions in strongly magnetized plasmas. We leverage Physics-Informed Symbolic Regression (PISR) to discover closed-form expressions for the vector potential and number density profiles, governed by a reduced-order model derived from Maxwell-fluid equations. The PISR framework combines symbolic regression with physics-based constraints, boundary conditions, and available simulation data to guide the search for solutions. We demonstrate the effectiveness of the approach by rediscovering approximate solutions consistent with previously published numerical results, showcasing the potential of PISR for reducing simulation costs of reduced-order models in plasma physics.

2025-10-02T20:40:09Z 16 pages, 2 figures, 1 table, 7 sections, 53 referenced works Edward Finkelstein http://arxiv.org/abs/2510.01436v1 2025-10-01T20:19:28Z

The symmetric product of two ordinary linear differential operators $L_1,L_2$ is an operator whose solution set contains the product $f_1f_2$ of any solution $f_1$ of $L_1$ and any solution $f_2$ of~$L_2$. It is well known how to compute the symmetric product of two given operators $L_1,L_2$. In this paper we consider the corresponding division problem: given a symmetric product $L$ and one of its factors, what can we say about the other factors?

2025-10-01T20:19:28Z Lixin Du Manuel Kauers http://arxiv.org/abs/2509.25757v1 2025-09-30T04:22:42Z

Modern Vision-Language Models (VLMs) have achieved impressive performance in various tasks, yet they often struggle with compositional reasoning, the ability to decompose and recombine concepts to solve novel problems. While neuro-symbolic approaches offer a promising direction, they are typically constrained by crisp logical execution or predefined predicates, which limit flexibility. In this work, we introduce NePTune, a neuro-symbolic framework that overcomes these limitations through a hybrid execution model that integrates the perception capabilities of foundation vision models with the compositional expressiveness of symbolic reasoning. NePTune dynamically translates natural language queries into executable Python programs that blend imperative control flow with soft logic operators capable of reasoning over VLM-generated uncertainty. Operating in a training-free manner, NePTune, with a modular design, decouples perception from reasoning, yet its differentiable operations support fine-tuning. We evaluate NePTune on multiple visual reasoning benchmarks and various domains, utilizing adversarial tests, and demonstrate a significant improvement over strong base models, as well as its effective compositional generalization and adaptation capabilities in novel environments.

2025-09-30T04:22:42Z Danial Kamali Parisa Kordjamshidi http://arxiv.org/abs/2509.25662v1 2025-09-30T01:58:59Z

Artificial intelligence (AI) systems in high-stakes domains raise concerns about proxy discrimination, unfairness, and explainability. Existing audits often fail to reveal why unfairness arises, particularly when rooted in structural bias. We propose a novel framework using formal abductive explanations to explain proxy discrimination in individual AI decisions. Leveraging background knowledge, our method identifies which features act as unjustified proxies for protected attributes, revealing hidden structural biases. Central to our approach is the concept of aptitude, a task-relevant property independent of group membership, with a mapping function aligning individuals of equivalent aptitude across groups to assess fairness substantively. As a proof of concept, we showcase the framework with examples taken from the German credit dataset, demonstrating its applicability in real-world cases.

2025-09-30T01:58:59Z Accepted at AJCAI 2025 AI 2025: Advances in Artificial Intelligence Belona Sonna Alban Grastien 10.1007/978-981-95-4969-6_20 http://arxiv.org/abs/2509.25114v1 2025-09-29T17:41:16Z

Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial invariants are properties of a program loop that hold before and after each iteration. Generating such invariants is a crucial task in loop analysis, but it is undecidable in the general case. Recently, an alternative approach to this problem has emerged, focusing on synthesizing loops from invariants. However, existing methods only synthesize affine loops without guard conditions from polynomial invariants. In this paper, we address a more general problem, allowing loops to have polynomial update maps with a given structure, inequations in the guard condition, and polynomial invariants of arbitrary form. We use algebraic geometry tools to design and implement an algorithm that computes a finite set of polynomial equations whose solutions correspond to all nondeterministic branching loops satisfying the given invariants. Furthermore, we introduce a new class of invariants for which we present a significantly more efficient algorithm. In other words, we reduce the problem of synthesizing loops to find solutions of multivariate polynomial systems with rational entries. This final step is handled in our software using an SMT solver.

2025-09-29T17:41:16Z Erdenebayar Bayarmagnai Fatemeh Mohammadi Rémi Prébet http://arxiv.org/abs/2406.02122v4 2025-09-26T20:04:14Z

The Model-Constructing Satisfiability Calculus (MCSAT) framework has been applied to SMT problems over various arithmetic theories. NLSAT, an implementation using cylindrical algebraic decomposition (CAD) for explanation, is especially competitive for nonlinear real arithmetic (NRA) constraints. However, current Conflict-Driven Clause Learning (CDCL)-style algorithms only consider literal information when making decisions, and thus ignore the influence of clauses on arithmetic variables. This limitation may lead NLSAT to encounter unnecessary conflicts due to suboptimal literal choices. To address this issue, we analyze conflicts caused by literal decisions and incorporate clause-level information that directly affects arithmetic variables. We propose two main algorithmic improvements: a clause-level feasible-set-based look-ahead mechanism and an arithmetic propagation-based branching heuristic. We implement our solver, named clauseSMT, based on a dynamic variable ordering framework. Experiments indicate that clauseSMT is competitive on nonlinear real arithmetic problems compared with existing SMT solvers (CVC5, Z3, YICES2), and it outperforms all of them on satisfiable instances of SMT(QF_NRA) in SMT-LIB. We also evaluate the effectiveness of our proposed methods.

2024-06-04T09:05:09Z Final version of ASE'2025 Zhonghan Wang