https://arxiv.org/api/At3DqQg4d1VTfhnxvLlMuaV8//g 2026-06-14T19:30:55Z 3138 465 15 http://arxiv.org/abs/2503.21731v2 2025-03-31T08:24:19Z

CylindricalAlgebraicDecomposition.m2 is the first implementation of Cylindrical Algebraic Decomposition (CAD) in Macaulay2. CAD decomposes space into 'cells' where input polynomials are sign-invariant. This package computes an Open CAD (full-dimensional cells only) for sets of real polynomials with rational coefficients, enabling users to solve existential problems involving strict inequalities. With the construction of a full CAD (cells of all dimensions), this tool could be extended to solve any real quantifier elimination problem. The current implementation employs the Lazard projection and introduces a new heuristic for choosing the variable ordering.

2025-03-27T17:46:24Z 16 pages, 9 figures Corin Lee Tereso del Río Hamid Rahkooy http://arxiv.org/abs/2503.22848v1 2025-03-28T19:56:27Z

Working in the multitape Turing model, we show how to reduce the problem of matrix transposition to the problem of integer multiplication. If transposing an $n \times n$ binary matrix requires $Ω(n^2 \log n)$ steps on a Turing machine, then our reduction implies that multiplying $n$-bit integers requires $Ω(n \log n)$ steps. In other words, if matrix transposition is as hard as expected, then integer multiplication is also as hard as expected.

2025-03-28T19:56:27Z 28 pages David Harvey Joris van der Hoeven http://arxiv.org/abs/2503.20849v2 2025-03-28T10:05:27Z

Logic programs, more specifically, Answer-set programs, can be annotated with probabilities on facts to express uncertainty. We address the problem of propagating weight annotations on facts (eg probabilities) of an ASP to its standard models, and from there to events (defined as sets of atoms) in a dataset over the program's domain. We propose a novel approach which is algebraic in the sense that it relies on an equivalence relation over the set of events. Uncertainty is then described as polynomial expressions over variables. We propagate the weight function in the space of models and events, rather than doing so within the syntax of the program. As evidence that our approach is sound, we show that certain facts behave as expected. Our approach allows us to investigate weight annotated programs and to determine how suitable a given one is for modeling a given dataset containing events.

2025-03-26T16:21:34Z Francisco Coelho Bruno Dinis Dietmar Seipel Salvador Abreu http://arxiv.org/abs/2311.10515v5 2025-03-28T08:51:02Z

Cylindrical algebraic decomposition is a classical construction in real algebraic geometry. Although there are many algorithms to compute a cylindrical algebraic decomposition, their practical performance is still very limited. In this paper, we revisit this problem from a more geometric perspective, where the construction of cylindrical algebraic decomposition is related to the study of morphisms between real varieties. It is showed that the geometric fiber cardinality (geometric property) decides the existence of semi-algebraic continuous sections (semi-algebraic property). As a result, all equations can be systematically exploited in the projection phase, leading to a new simple algorithm whose efficiency is demonstrated by experimental results.

2023-11-17T13:36:57Z Minor Revision, 34 Pages. Math. Comp., electronically published on June 3, 2025 Rizeng Chen 10.1090/mcom/4099 http://arxiv.org/abs/2503.21535v1 2025-03-27T14:26:31Z

The Deligne-Ogus-Shioda theorem guarantees the existence of isomorphisms between products of supersingular elliptic curves over finite fields. In this paper, we present methods for explicitly computing these isomorphisms in polynomial time, given the endomorphism rings of the curves involved. Our approach leverages the Deuring correspondence, enabling us to reformulate computational isogeny problems into algebraic problems in quaternions. Specifically, we reduce the computation of isomorphisms to solving systems of quadratic and linear equations over the integers derived from norm equations. We develop $\ell$-adic techniques for solving these equations when we have access to a low discriminant subring. Combining these results leads to the description of an efficient probabilistic Las Vegas algorithm for computing the desired isomorphisms. Under GRH, it is proved to run in expected polynomial time.

2025-03-27T14:26:31Z Pierrick Gaudry Julien Soumier Pierre-Jean Spaenlehauer http://arxiv.org/abs/2308.10977v2 2025-03-27T03:14:54Z

Christol's theorem states that a power series with coefficients in a finite field is algebraic if and only if its coefficient sequence is automatic. A natural question is how the size of a polynomial describing such a sequence relates to the size of an automaton describing the same sequence. Bridy used tools from algebraic geometry to bound the size of the minimal automaton for a sequence, given its minimal polynomial. We produce a new proof of Bridy's bound by embedding algebraic sequences as diagonals of rational functions.

2023-08-21T18:48:24Z 31 pages, 2 figures, 2 tables; publication version Eric Rowland Manon Stipulanti Reem Yassawi 10.1016/j.ffa.2025.102621 http://arxiv.org/abs/2503.20071v1 2025-03-25T21:13:06Z

A central question in mathematics and computer science is the question of determining whether a given ideal $I$ is prime, which geometrically corresponds to the zero set of $I$, denoted $Z(I)$, being irreducible. The case of principal ideals (i.e., $m=1$) corresponds to the more familiar absolute irreducibility testing of polynomials, where the seminal work of (Kaltofen 1995) yields a randomized, polynomial time algorithm for this problem. However, when $m > 1$, the complexity of the primality testing problem seems much harder. The current best algorithms for this problem are only known to be in EXPSPACE. In this work, we significantly reduce the complexity-theoretic gap for the ideal primality testing problem for the important families of ideals $I$ (namely, radical ideals and equidimensional Cohen-Macaulay ideals). For these classes of ideals, assuming the Generalized Riemann Hypothesis, we show that primality testing lies in $Σ_3^p \cap Π_3^p$. This significantly improves the upper bound for these classes, approaching their lower bound, as the primality testing problem is coNP-hard for these classes of ideals. Another consequence of our results is that for equidimensional Cohen-Macaulay ideals, we get the first PSPACE algorithm for primality testing, exponentially improving the space and time complexity of prior known algorithms.

2025-03-25T21:13:06Z 36 pages. Accepted in STOC 2025 Abhibhav Garg Rafael Oliveira Nitin Saxena 10.1145/3717823.3718167 http://arxiv.org/abs/2401.08470v3 2025-03-25T00:58:20Z

We extend Petkovšek's algorithm for computing hypergeometric solutions of scalar difference equations to the case of difference systems $τ(Y) = M Y$, with $M \in {\rm GL}_n(C(x))$, where $τ$ is the shift operator. Hypergeometric solutions are solutions of the form $γP$ where $P \in C(x)^n$ and $γ$ is a hypergeometric term over $C(x)$, i.e. ${τ(γ)}/γ \in C(x)$. Our contributions concern efficient computation of a set of candidates for ${τ(γ)}/γ$ which we write as $λ= c\frac{A}{B}$ with monic $A, B \in C[x]$, $c \in C^*$. Factors of the denominators of $M^{-1}$ and $M$ give candidates for $A$ and $B$, while another algorithm is needed for $c$. We use the super-reduction algorithm to compute candidates for $c$, as well as other ingredients to reduce the list of candidates for $A/B$. To further reduce the number of candidates $A/B$, we bound the so-called type of $A/B$ by bounding local types. Our algorithm has been implemented in Maple and experiments show that our implementation can handle systems of high dimension, which is useful for factoring operators.

2024-01-16T16:19:09Z 24 pages Moulay Barkatou Mark van Hoeij Johannes Middeke Yi Zhou http://arxiv.org/abs/2503.19043v1 2025-03-24T18:13:49Z

This paper presents QDSR, an advanced symbolic Regression (SR) system that integrates genetic programming (GP), a quality-diversity (QD) algorithm, and a dimensional analysis (DA) engine. Our method focuses on exact symbolic recovery of known expressions from datasets, with a particular emphasis on the Feynman-AI benchmark. On this widely used collection of 117 physics equations, QDSR achieves an exact recovery rate of 91.6~$\%$, surpassing all previous SR methods by over 20 percentage points. Our method also exhibits strong robustness to noise. Beyond QD and DA, this high success rate results from a profitable trade-off between vocabulary expressiveness and search space size: we show that significantly expanding the vocabulary with precomputed meaningful variables (e.g., dimensionless combinations and well-chosen scalar products) often reduces equation complexity, ultimately leading to better performance. Ablation studies will also show that QD alone already outperforms the state-of-the-art. This suggests that a simple integration of QD, by projecting individuals onto a QD grid, can significantly boost performance in existing algorithms, without requiring major system overhauls.

2025-03-24T18:13:49Z 23 pages, 1 figure, submitted to Journal of Machine Learning research J. -P. Bruneton http://arxiv.org/abs/2503.18030v1 2025-03-23T11:07:24Z

Parameterized systems play a crucial role in the computer field, and their security is of great significance. Formal verification of parameterized protocols is especially challenging due to its "parameterized" feature, which brings complexity and undecidability. Existing automated parameterized verification methods have limitations, such as facing difficulties in automatically deriving parameterized invariants constrained by mixed Forall and Exists quantifiers, or having challenges in completing the parameterized verification of large and complex protocols. This paper proposes a formal verification framework for parameterized systems based on induction, named wiseParaverifier. It starts from small concretizations of protocols, analyzes inductive counterexamples, and constructs counterexample formulas to guide the entire process of parameterized verification. It also presents a heuristic Generalize method to quickly find auxiliary invariants, a method for promoting complex mixed quantifiers and merging parameterized invariants, and uses symmetric reduction ideas to accelerate the verification process. Experimental results show that wiseParaverifier can successfully complete automatic inductive verification on 7 cache coherence protocols and 10 distributed protocols. It has strong verification capabilities and migration capabilities, and can provide concise and readable verification results, which is helpful for learners to understand protocol behaviors.

2025-03-23T11:07:24Z 9 pages,2 figures Jiaqi Xiu Yongjian Li http://arxiv.org/abs/2503.15636v1 2025-03-19T18:46:26Z

A rational function $f(x)$ is rationally summable if there exists a rational function $g(x)$ such that $f(x)=g(x+1)-g(x)$. Detecting whether a given rational function is summable is an important and basic computational subproblem that arises in algorithms to study diverse aspects of shift difference equations. The discrete residues introduced by Chen and Singer in 2012 enjoy the obstruction-theoretic property that a rational function is summable if and only if all its discrete residues vanish. However, these discrete residues are defined in terms of the data in the complete partial fraction decomposition of the given rational function, which cannot be accessed computationally in general. We explain how to efficiently compute (a rational representation of) the discrete residues of any rational function, relying only on gcd computations, linear algebra, and a black box algorithm to compute the autodispersion set of the denominator polynomial. We also explain how to apply our algorithms to serial summability and creative telescoping problems, and how to apply these computations to compute Galois groups of difference equations.

2025-03-19T18:46:26Z Submitted. arXiv admin note: substantial text overlap with arXiv:2402.07328 Carlos E. Arreche Hari P. Sitaula http://arxiv.org/abs/2503.14264v1 2025-03-18T13:54:46Z

Deciding the positivity of a sequence defined by a linear recurrence and initial conditions is, in general, a hard problem. When the coefficients of the recurrences are constants, decidability has only been proven up to order 5. The difficulty arises when the characteristic polynomial of the recurrence has several roots of maximal modulus, called dominant roots of the recurrence. We study the positivity problem for recurrences with polynomial coefficients, focusing on sequences of Poincaré type, which are perturbations of constant-coefficient recurrences. The dominant eigenvalues of a recurrence in this class are the dominant roots of the associated constant-coefficient recurrence. Previously, we have proved the decidability of positivity for recurrences having a unique, simple, dominant eigenvalue, under a genericity assumption. The associated algorithm proves positivity by constructing a positive cone contracted by the recurrence operator. We extend this cone-based approach to a larger class of recurrences, where a contracted cone may no longer exist. The main idea is to construct a sequence of cones. Each cone in this sequence is mapped by the recurrence operator to the next. This construction can be applied to prove positivity by induction. For recurrences with several simple dominant eigenvalues, we provide a condition that ensures that these successive inclusions hold. Additionally, we demonstrate the applicability of our method through examples, including recurrences with a double dominant eigenvalue.

2025-03-18T13:54:46Z Alaa Ibrahim http://arxiv.org/abs/2503.13640v1 2025-03-17T18:43:10Z

The matrix LU factorization algorithm is a fundamental algorithm in linear algebra. We propose a generalization of the LU and LEU algorithms to accommodate the case of a commutative domain and its field of quotients. This algorithm decomposes any matrix A into a product of three matrices A=LSU, where each element of the triangular matrices L and U is a minor of matrix A. The number of non-zero elements in matrix S is equal to rank(A), and each of them is the inverse of the product of a specific pair of matrix A minors. The algorithm's complexity is equivalent to that of matrix multiplication.

2025-03-17T18:43:10Z 7 pages, 1 figures 2023 International Conference on Computational Science and Computational Intelligence (CSCI), Las Vegas, NV, USA, 2023, pp. 472-478 Gennadi Malaschonok 10.1109/CSCI62032.2023.00083 http://arxiv.org/abs/2505.03740v1 2025-03-17T16:14:01Z

The article provides a brief description of the MathPartner service. This freely available cloud-based Mathematics is a universal system for symbolic-numeric calculations. Its Mathpar language is a subset of the LaTeX language, but allows you to create mathematical texts that contain "computable" mathematical operators. This opens up completely new opportunities for improving the educational process for all natural science disciplines, for the use of mathematics in scientific and engineering calculations. To save and freely exchange educational and other texts in the Mathpar language, a GitHub repository has been created. It is concluded that cloud mathematics MathPartner is a new breakthrough technology for school and university natural science education, for scientific and engineering applications.

2025-03-17T16:14:01Z 12 pages, conference proceedings Information and Communication Technologies in Education, Research, and Industrial Applications. ICTERI 2024. Com- munications in Computer and Information Science, vol 2359. Springer, Cham Gennadi Malaschonok Roman Sakh 10.1007/978-3-031-81372-6_15 http://arxiv.org/abs/2204.06968v3 2025-03-17T12:19:53Z

Symbolic summation as an active research topic of symbolic computation provides efficient algorithmic tools for evaluating and simplifying different types of sums arising from mathematics, computer science, physics and other areas. Most of existing algorithms in symbolic summation are mainly applicable to the problem with univariate inputs. A long-term project in symbolic computation is to develop theories, algorithms and software for the symbolic summation of multivariate functions. This paper will give complete solutions to two challenging problems in symbolic summation of multivariate rational functions, namely the rational summability problem and the existence problem of telescopers for multivariate rational functions. Our approach is based on the structure of Sato's isotropy groups of polynomials, which enables us to reduce the problems to testing the shift equivalence of polynomials. Our results provide a complete solution to the discrete analogue of Picard's problem on differential forms and can be used to detect the applicability of the Wilf-Zeilberger method to multivariate rational functions.

2022-04-14T13:48:52Z 55 pages, to appear in Foundations of Computational Mathematics Shaoshi Chen Lixin Du Hanqian Fang