https://arxiv.org/api/tH61kuKG0h3PKlfhHs7eNOctzCU 2026-04-12T10:09:30Z 3074 315 15 http://arxiv.org/abs/2506.08767v1 2025-06-10T13:07:04Z

A complete reduction on a difference field is a linear operator that enables one to decompose an element of the field as the sum of a summable part and a remainder such that the given element is summable if and only if the remainder is equal to zero. In this paper, we present a complete reduction in a tower of $Σ^*$-extensions that turns to a new efficient framework for the parameterized telescoping problem. Special instances of such $Σ^*$-extensions cover iterative sums such as the harmonic numbers and generalized versions that arise, e.g., in combinatorics, computer science or particle physics. Moreover, we illustrate how these new ideas can be used to reduce the depth of the given sum and provide structural theorems that connect complete reductions to Karr's Fundamental Theorem of symbolic summation.

2025-06-10T13:07:04Z Shaoshi Chen Yiman Gao Hui Huang Carsten Schneider http://arxiv.org/abs/2506.08600v1 2025-06-10T09:06:41Z

Recent advances in artificial intelligence have demonstrated the learnability of symbolic computation through end-to-end deep learning. Given a sufficient number of examples of symbolic expressions before and after the target computation, Transformer models - highly effective learners of sequence-to-sequence functions - can be trained to emulate the computation. This development opens up several intriguing challenges and new research directions, which require active contributions from the symbolic computation community. In this work, we introduce Computer Algebra with Transformer (CALT), a user-friendly Python library designed to help non-experts in deep learning train models for symbolic computation tasks.

2025-06-10T09:06:41Z ISSAC 2025 Short Communications Hiroshi Kera Shun Arakawa Yuta Sato http://arxiv.org/abs/2405.02430v2 2025-06-08T03:31:43Z

Wilf-Zeilberger pairs are fundamental in the algorithmic theory of Wilf and Zeilberger for computer-generated proofs of combinatorial identities. Wilf-Zeilberger forms are their high-dimensional generalizations, which can be used for proving and discovering convergence acceleration formulas. This paper presents a structural description of all possible rational such forms, which can be viewed as an additive analog of the classical Ore-Sato theorem. Based on this analog, we show a structural decomposition of so-called multivariate hyperarithmetic terms, which extend multivariate hypergeometric terms to the additive setting.

2024-05-03T18:52:23Z Shaoshi Chen Christoph Koutschan Yisen Wang http://arxiv.org/abs/2505.17309v2 2025-06-06T08:30:09Z

Genetic Programming (GP) has traditionally entangled the evolution of symbolic representations with their performance-based evaluation, often relying solely on raw fitness scores. This tight coupling makes GP solutions more fragile and prone to overfitting, reducing their ability to generalize. In this work, we propose LaSER (Latent Semantic Representation Regression)} -- a general framework that decouples representation evolution from lifetime learning. At each generation, candidate programs produce features which are passed to an external learner to model the target task. This approach enables any function approximator, from linear models to neural networks, to serve as a lifetime learner, allowing expressive modeling beyond conventional symbolic forms. Here we show for the first time that LaSER can outcompete standard GP and GP followed by linear regression when it employs non-linear methods to fit coefficients to GP-generated equations against complex data sets. Further, we explore how LaSER enables the emergence of innate representations, supporting long-standing hypotheses in evolutionary learning such as the Baldwin Effect. By separating the roles of representation and adaptation, LaSER offers a principled and extensible framework for symbolic regression and classification.

2025-05-22T21:59:38Z Accepted to Genetic Programming Theory and Practice (GPTP) 2025. The final revised version will be uploaded following the workshop Nam H. Le Josh Bongard http://arxiv.org/abs/2506.05835v1 2025-06-06T07:58:23Z

Narrowing is a well-known technique that adds to term rewriting mechanisms the required power to search for solutions to equational problems. Rewriting and narrowing are well-studied in first-order term languages, but several problems remain to be investigated when dealing with languages with binders using nominal techniques. Applications in programming languages and theorem proving require reasoning modulo alpha-equivalence considering structural congruences generated by equational axioms, such as commutativity. This paper presents the first definitions of nominal rewriting and narrowing modulo an equational theory. We establish a property called nominal E-coherence and demonstrate its role in identifying normal forms of nominal terms. Additionally, we prove the nominal E-Lifting theorem, which ensures the correspondence between sequences of nominal equational rewriting steps and narrowing, crucial for developing a correct algorithm for nominal equational unification via nominal equational narrowing. We illustrate our results using the equational theory for commutativity.

2025-06-06T07:58:23Z In Proceedings LSFA 2024, arXiv:2506.05219. arXiv admin note: substantial text overlap with arXiv:2505.14895 EPTCS 421, 2025, pp. 80-97 Mauricio Ayala-Rincón University of Brasília, Brazil Maribel Fernández King's College London, UK Daniele Nantes-Sobrinho University of Brasília, Brazil and Imperial College London, UK Daniella Santaguida University of Brasília, Brazil 10.4204/EPTCS.421.5 http://arxiv.org/abs/2505.22652v2 2025-06-05T17:13:19Z

We present PyRigi, a novel Python package designed to study the rigidity properties of graphs and frameworks. Among many other capabilities, PyRigi can determine whether a graph admits only finitely many ways, up to isometries, of being drawn in the plane once the edge lengths are fixed, whether it has a unique embedding, or whether it satisfied such properties even after the removal of any of its edges. By implementing algorithms from the scientific literature, PyRigi enables the exploration of rigidity properties of structures that would be out of reach for computations by hand. With reliable and robust algorithms, as well as clear, well-documented methods that are closely connected to the underlying mathematical definitions and results, PyRigi aims to be a practical and powerful general-purpose tool for the working mathematician interested in rigidity theory. PyRigi is open source and easy to use, and awaits researchers to benefit from its computational potential.

2025-05-28T17:58:25Z 23 pages, 5 figures Matteo Gallet Georg Grasegger Matthias Himmelmann Jan Legerský http://arxiv.org/abs/2506.05219v1 2025-06-05T16:35:22Z

This volume contains the post-proceedings of the 19th LSFA, which was held in Goiânia, the capital of Goiás state in Brazil, from September 18 to September 20, 2024. Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning. The aim of this series is bringing together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. LSFA includes areas such as proof and type theory, equational deduction and rewriting systems, automated reasoning and concurrency theory.

2025-06-05T16:35:22Z EPTCS 421, 2025 Cynthia Kop Radboud Universiteit Nijmegen Helida Salles Santos Universidade Federal do Rio Grande 10.4204/EPTCS.421 http://arxiv.org/abs/2504.08472v2 2025-06-05T12:01:47Z

In this paper, we extend the work of (Abbondati et al., 2024) on decoding simultaneous rational number codes by addressing two important scenarios: multiplicities and the presence of bad primes (divisors of denominators). First, we generalize previous results to multiplicity rational codes by considering modular reductions with respect to prime power moduli. Then, using hybrid analysis techniques, we extend our approach to vectors of fractions that may present bad primes. Our contributions include: a decoding algorithm for simultaneous rational number reconstruction with multiplicities, a rigorous analysis of the algorithm's failure probability that generalizes several previous results, an extension to a hybrid model handling situations where not all errors can be assumed random, and a unified approach to handle bad primes within multiplicities. The theoretical results provide a comprehensive probabilistic analysis of reconstruction failure in these more complex scenarios, advancing the state of the art in error correction for rational number codes.

2025-04-11T12:01:41Z Matteo Abbondati LIRMM | ECO Eleonora Guerrini LIRMM | ECO Romain Lebreton LIRMM | ECO http://arxiv.org/abs/2506.04436v1 2025-06-04T20:38:31Z

We introduce beyond-worst-case analysis into symbolic computation. This is an extensive field which almost entirely relies on worst-case bit complexity, and we start from a basic problem in the field: isolating the real roots of univariate polynomials. This is a fundamental problem in symbolic computation and it is arguably one of the most basic problems in computational mathematics. The problem has a long history decorated with numerous ingenious algorithms and furnishes an active area of research. However, most available results in literature either focus on worst-case analysis in the bit complexity model or simply provide experimental benchmarking without any theoretical justifications of the observed results. We aim to address the discrepancy between practical performance of root isolation algorithms and prescriptions of worst-case complexity theory: We develop a smoothed analysis framework for polynomials with integer coefficients to bridge this gap. We demonstrate (quasi-)linear (expected and smoothed) complexity bounds for Descartes algorithm, that is one most well know symbolic algorithms for isolating the real roots of univariate polynomials with integer coefficients. Our results explain the surprising efficiency of Descartes solver in comparison to sophisticated algorithms that have superior worst-case complexity. We also analyse the Sturm solver, ANewDsc a symbolic-numeric algorithm that combines Descartes with Newton operator, and a symbolic algorithm for sparse polynomials.

2025-06-04T20:38:31Z 27 pages. Extended journal-version of arXiv:2202.06428 Alperen A. Ergür Josué Tonelli-Cueto Elias Tsigaridas http://arxiv.org/abs/2502.02014v3 2025-06-04T20:16:54Z

Despite advances in learning-based methods, finding valid Lyapunov functions for nonlinear dynamical systems remains challenging. Current neural network approaches face two main issues: challenges in scalable verification and limited interpretability. To address these, we propose an end-to-end framework using transformers to construct analytical Lyapunov functions (local), which simplifies formal verification, enhances interpretability, and provides valuable insights for control engineers. Our framework consists of a transformer-based trainer that generates candidate Lyapunov functions and a falsifier that verifies candidate expressions and refines the model via risk-seeking policy gradient. Unlike Alfarano et al. (2024), which utilizes pre-training and seeks global Lyapunov functions for low-dimensional systems, our model is trained from scratch via reinforcement learning (RL) and succeeds in finding local Lyapunov functions for high-dimensional and non-polynomial systems. Given the analytical nature of the candidates, we employ efficient optimization methods for falsification during training and formal verification tools for the final verification. We demonstrate the efficiency of our approach on a range of nonlinear dynamical systems with up to ten dimensions and show that it can discover Lyapunov functions not previously identified in the control literature. Full implementation is available on \href{https://github.com/JieFeng-cse/Analytical-Lyapunov-Function-Discovery}{Github}

2025-02-04T05:04:15Z 26 pages (8+18), preprint for discussion. Haohan and Jie contribute equally Haohan Zou Jie Feng Hao Zhao Yuanyuan Shi http://arxiv.org/abs/2502.16975v2 2025-06-03T07:43:06Z

Though Mahler equations have been introduced nearly one century ago, the study of their solutions is still a fruitful topic for research. In particular, the Galois theory of Mahler equations has been the subject of many recent papers. Nevertheless, long is the way to a complete understanding of relations between solutions of Mahler equations. One step along this way is the study of singularities. Mahler equations with a regular singularity at 0 have rather "nice" solutions: they can be expressed with the help of Puiseux series and solutions of equations with constant coefficients. In a previous paper, the authors described an algorithm to determine whether an equation is regular singular at 0 or not. Exploiting information from the Frobenius method and Newton polygons, we improve this algorithm by significantly reducing its complexity, by providing some simple criterion for an equation to be regular singular at 0, and by extending its scope to equations with Puiseux coefficients.

2025-02-24T09:04:18Z Colin Faverjon ICJ, CTN Marina Poulet IF http://arxiv.org/abs/2506.01087v1 2025-06-01T17:09:55Z

The rule $\mathrm{Defeated}(x) \leftarrow \mathrm{Attacks}(y,x),\, \neg \, \mathrm{Defeated}(y)$, evaluated under the well-founded semantics (WFS), yields a unique 3-valued (skeptical) solution of an abstract argumentation framework (AF). An argument $x$ is defeated ($\mathrm{OUT}$) if there exists an undefeated argument $y$ that attacks it. For 2-valued (stable) solutions, this is the case iff $y$ is accepted ($\mathrm{IN}$), i.e., if all of $y$'s attackers are defeated. Under WFS, arguments that are neither accepted nor defeated are undecided ($\mathrm{UNDEC}$). As shown in prior work, well-founded solutions (a.k.a. grounded labelings) "explain themselves": The provenance of arguments is given by subgraphs (definable via regular path queries) rooted at the node of interest. This provenance is closely related to winning strategies of a two-player argumentation game. We present a novel approach for extending this provenance to stable AF solutions. Unlike grounded solutions, which can be constructed via a bottom-up alternating fixpoint procedure, stable models often involve non-deterministic choice as part of the search for models. Thus, the provenance of stable solutions is of a different nature, and reflects a more expressive generate & test paradigm. Our approach identifies minimal sets of critical attacks, pinpointing choices and assumptions made by a stable model. These critical attack edges provide additional insights into the provenance of an argument's status, combining well-founded derivation steps with choice steps. Our approach can be understood as a form of diagnosis that finds minimal "repairs" to an AF graph such that the well-founded solution of the repaired graph coincides with the desired stable model of the original AF graph.

2025-06-01T17:09:55Z International Workshop on the Theory and Practice of Provenance (TaPP) and ProvenanceWeek'25 @SIGMOD, June 27, 2025. Berlin, Germany Bertram Ludäscher Yilin Xia Shawn Bowers http://arxiv.org/abs/2505.24533v1 2025-05-30T12:40:01Z

We introduce a novel framework consisting of a class of algebraic structures that generalize one-dimensional monoidal systems into higher dimensions by defining per-axis composition operators subject to non-commutativity and a global interchange law. These structures, defined recursively from a base case of vector-matrix pairs, model directional composition in multiple dimensions while preserving structural coherence through commutative linear operators. We show that the framework that unifies several well-known linear transforms in signal processing and data analysis. In this framework, data indices are embedded into a composite structure that decomposes into simpler components. We show that classic transforms such as the Discrete Fourier Transform (DFT), the Walsh transform, and the Hadamard transform are special cases of our algebraic structure. The framework provides a systematic way to derive these transforms by appropriately choosing vector and matrix pairs. By subsuming classical transforms within a common structure, the framework also enables the development of learnable transformations tailored to specific data modalities and tasks.

2025-05-30T12:40:01Z Mahesh Godavarti http://arxiv.org/abs/2505.23696v1 2025-05-29T17:35:25Z

Solving systems of polynomial equations, particularly those with finitely many solutions, is a crucial challenge across many scientific fields. Traditional methods like Gröbner and Border bases are fundamental but suffer from high computational costs, which have motivated recent Deep Learning approaches to improve efficiency, albeit at the expense of output correctness. In this work, we introduce the Oracle Border Basis Algorithm, the first Deep Learning approach that accelerates Border basis computation while maintaining output guarantees. To this end, we design and train a Transformer-based oracle that identifies and eliminates computationally expensive reduction steps, which we find to dominate the algorithm's runtime. By selectively invoking this oracle during critical phases of computation, we achieve substantial speedup factors of up to 3.5x compared to the base algorithm, without compromising the correctness of results. To generate the training data, we develop a sampling method and provide the first sampling theorem for border bases. We construct a tokenization and embedding scheme tailored to monomial-centered algebraic computations, resulting in a compact and expressive input representation, which reduces the number of tokens to encode an $n$-variate polynomial by a factor of $O(n)$. Our learning approach is data efficient, stable, and a practical enhancement to traditional computer algebra algorithms and symbolic computation.

2025-05-29T17:35:25Z 13+19 pages (3+9 figures, 2+7 tables) Hiroshi Kera Nico Pelleriti Yuki Ishihara Max Zimmer Sebastian Pokutta http://arxiv.org/abs/2503.07148v3 2025-05-29T13:21:50Z

We present a hierarchical neuro-symbolic control framework that tightly couples a classical symbolic planner with a transformer-based policy to address long-horizon decision-making under uncertainty. At the high level, the planner assembles an interpretable sequence of operators that guarantees logical coherence with task constraints, while at the low level each operator is rendered as a sub-goal token that conditions a decision transformer to generate fine-grained actions directly from raw observations. This bidirectional interface preserves the combinatorial efficiency and explainability of symbolic reasoning without sacrificing the adaptability of deep sequence models, and it permits a principled analysis that tracks how approximation errors from both planning and execution accumulate across the hierarchy. Empirical studies in stochastic grid-world domains demonstrate that the proposed method consistently surpasses purely symbolic, purely neural and existing hierarchical baselines in both success and efficiency, highlighting its robustness for sequential tasks.

2025-03-10T10:22:13Z Ali Baheri Cecilia O. Alm