https://arxiv.org/api/Xpzy3NGLXWDTRWqQslS/IxiU8hI 2026-06-14T18:28:11Z 3138 450 15 http://arxiv.org/abs/2504.14990v1 2025-04-21T09:41:01Z

Quaternionic polynomials occur naturally in applications of quaternions in science and engineering, and normalization of quaternionic polynomials is a basic manipulation. Once a Groebner basis is certified for the defining ideal I of the quaternionic polynomial algebra, the normal form of a quaternionic polynomial can be computed by routine top reduction with respect to the Groebner basis. In the literature, a Groebner basis under the conjugate-alternating order of quaternionic variables was conjectured for I in 2013, but no readable and convincing proof was found. In this paper, we present the first readable certification of the conjectured Groebner basis. The certification is based on several novel techniques for reduction in free associative algebras, which enables to not only make reduction to S-polynomials more efficiently, but also reduce the number of S-polynomials needed for the certification.

2025-04-21T09:41:01Z 43 pages, 3 figures Hongbo Li Zhengyang Wang Yue Liu Lei Huang Changpeng Shao http://arxiv.org/abs/2309.03138v6 2025-04-18T08:52:09Z

In this paper we present a quantifier elimination method for conjunctions of linear real arithmetic constraints. Our algorithm is based on the Fourier-Motzkin variable elimination procedure, but by case splitting we are able to reduce the worst-case complexity from doubly to singly exponential. The adaption of the procedure for SMT solving has strong correspondence to the simplex algorithm, therefore we name it FMplex. Besides the theoretical foundations, we provide an experimental evaluation in the context of SMT solving. This is an extended version of the authors' work previously published at the fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023).

2023-09-06T16:22:01Z Logical Methods in Computer Science, Volume 21, Issue 2 (April 21, 2025) lmcs:13362 Valentin Promies Jasper Nalbach Erika Ábrahám Paul Kobialka 10.46298/lmcs-21(2:6)2025 http://arxiv.org/abs/2504.13506v1 2025-04-18T06:57:38Z

Given a number field with absolute Galois group $\mathcal{G}$, a finite Galois module $M$, and a Selmer system $\mathcal{L}$, this article gives a method to compute Sel$_\mathcal{L}$, the Selmer group of $M$ attached to $\mathcal{L}$. First we describe an algorithm to obtain a resolution of $M$ where the morphisms are given by Hecke operators. Then we construct another group $H^1_S(\mathcal{G}, M)$ and we prove, using the properties of Hecke operators, that $H^1_S(\mathcal{G}, M)$ is a Selmer group containing Sel$_\mathcal{L}$. Then, we discuss the time complexity of this method.

2025-04-18T06:57:38Z Fabrice Etienne UB, CANARI, IMB http://arxiv.org/abs/2504.12465v1 2025-04-16T20:01:00Z

The intersection of deep learning and symbolic mathematics has seen rapid progress in recent years, exemplified by the work of Lample and Charton. They demonstrated that effective training of machine learning models for solving mathematical problems critically depends on high-quality, domain-specific datasets. In this paper, we address the computation of Gröbner basis using Transformers. While a dataset generation method tailored to Transformer-based Gröbner basis computation has previously been proposed, it lacked theoretical guarantees regarding the generality or quality of the generated datasets. In this work, we prove that datasets generated by the previously proposed algorithm are sufficiently general, enabling one to ensure that Transformers can learn a sufficiently diverse range of Gröbner bases. Moreover, we propose an extended and generalized algorithm to systematically construct datasets of ideal generators, further enhancing the training effectiveness of Transformer. Our results provide a rigorous geometric foundation for Transformers to address a mathematical problem, which is an answer to Lample and Charton's idea of training on diverse or representative inputs.

2025-04-16T20:01:00Z 19 pages Yuta Kambe Yota Maeda Tristan Vaccon http://arxiv.org/abs/2504.10253v1 2025-04-14T14:14:27Z

Over the years, genetic programming (GP) has evolved, with many proposed variations, especially in how they represent a solution. Being essentially a program synthesis algorithm, it is capable of tackling multiple problem domains. Current benchmarking initiatives are fragmented, as the different representations are not compared with each other and their performance is not measured across the different domains. In this work, we propose a unified framework, dubbed TinyverseGP (inspired by tinyGP), which provides support to multiple representations and problem domains, including symbolic regression, logic synthesis and policy search.

2025-04-14T14:14:27Z Accepted for presentation as a poster at the Genetic and Evolutionary Computation Conference (GECCO) and will appear in the GECCO'25 companion. GECCO'25 will be held July 14-18, 2025 in Málaga, Spain GECCO'25 Companion: Genetic and Evolutionary Computation Conference Companion, July 14-18, 2025, Malaga, Spain Roman Kalkreuth Fabricio Olivetti de França Julian Dierkes Marie Anastacio Anja Jankovic Zdenek Vasicek Holger Hoos 10.1145/3712255.3726697 http://arxiv.org/abs/2505.02261v1 2025-04-14T08:41:30Z

This paper introduces a structured decoding framework for the Voynich Manuscript, based on mathematical rhythm, symbolic transformation, and glyph-level recursion. Rather than interpret symbols phonetically, this method decodes them by structural roles and spatial pacing. Using scroll-wide sequencing, the system tracks prime number grouping, Fibonacci clustering, and golden ratio alignment. These symbolic structures are validated using a ten-part chi-squared test suite and Boolean logic. The method is falsifiable and reproducible. Scroll sections like f57v, f88v, and f91r are used to demonstrate glyph flow, breath-segment patterns, and tri-dot alignment. This decoding strategy challenges assumptions about pre-phonetic manuscripts and proposes a new lens for interpreting symbolic logic.

2025-04-14T08:41:30Z 29 pages; includes glyph mapping, golden ratio alignment, and boolean-chi-squared validation protocols Suhaib A. Jama http://arxiv.org/abs/2504.09790v1 2025-04-14T01:30:44Z

The field of analytic combinatorics in several variables (ACSV) develops techniques to compute the asymptotic behaviour of multivariate sequences from analytic properties of their generating functions. When the generating function under consideration is rational, its set of singularities forms an algebraic variety -- called the singular variety -- and asymptotic behaviour depends heavily on the geometry of the singular variety. By combining a recent algorithm for the Whitney stratification of algebraic varieties with methods from ACSV, we present the first software that rigorously computes asymptotics of sequences whose generating functions have non-smooth singular varieties (under other assumptions on local geometry). Our work is built on the existing sage_acsv package for the SageMath computer algebra system, which previously gave asymptotics under a smoothness assumption. We also report on other improvements to the package, such as an efficient technique for determining higher order asymptotic expansions using Newton iteration, the ability to use more efficient backends for algebraic computations, and a method to compute so-called critical points for any multivariate rational function through Whitney stratification.

2025-04-14T01:30:44Z Accepted to proceedings of FPSAC 2025 Benjamin Hackl Andrew Luo Stephen Melczer Éric Schost http://arxiv.org/abs/2502.16783v2 2025-04-13T19:52:35Z

Linear algebra's main concerns are sets of vectors, linear functions, subspaces, linear systems, matrices and concepts about those, such as whether the solution of linear system exists or is unique; a set of vectors is linearly independent or spans the whole space; a linear function has a right or a left inverse; a linear function is surjective or injective; and the kernel of a matrix is trivial or the its image is full. The Invertible Matrix Theorem ties all these ideas and many others together. Many modern linear algebra books use this theorem as a guiding principle to explain many connections in linear algebra. The main idea is to separately characterize whether the linear function is surjective or injective. The proof usually uses a matrix decomposition as the key step. However, the invertible matrix theorem deals with a single linear function, a single set of vectors, a single subspace, and a single matrix. In this work, we generalize part of the invertible matrix theorem to results about a pair of linear functions, a pair of sets of vectors, a pair of subspaces, and a single linear relation. The main idea is to separately characterize the linear relation's fundamental properties -- whether it is surjective, injective, deterministic and total. Our proof uses a decomposition of a linear relation as the key step. Unfortunately, reasoning with linear relations in classical notation requires applying many rules besides shuffling quantifiers and variables around, which can obscure the symmetries in the results. Therefore, this work employs graphical linear algebra, a two-dimensional diagrammatic syntax with the fundamental rules of linear relations built-in.

2025-02-24T02:29:40Z 43 pages; updated title and abstract Iago Leal de Freitas Júlia Mota João Paixão Lucas Rufino http://arxiv.org/abs/2304.09094v2 2025-04-11T18:33:59Z

We propose the K-series estimation approach for the recovery of unknown univariate and multivariate distributions given knowledge of a finite number of their moments. Our method is directly applicable to the probabilistic analysis of systems that can be represented as probabilistic loops; i.e., algorithms that express and implement non-deterministic processes ranging from robotics to macroeconomics and biology to software and cyber-physical systems. K-series statically approximates the joint and marginal distributions of a vector of continuous random variables updated in a probabilistic non-nested loop with nonlinear assignments given a finite number of moments of the unknown density. Moreover, K-series automatically derives the distribution of the systems' random variables symbolically as a function of the loop iteration. K-series density estimates are accurate, easy and fast to compute. We demonstrate the feasibility and performance of our approach on multiple benchmark examples from the literature.

2023-04-17T14:46:38Z Accepted for publication in ACM Transactions on Probabilistic Machine Learning, 37 page Andrey Kofnov Ezio Bartocci Efstathia Bura 10.1145/3728648 http://arxiv.org/abs/2405.16167v2 2025-04-10T14:12:22Z

A reformulation of the three circles theorem of Johnson with distance coordinates to the vertices of a triangle is explicitly represented in a polynomial system and solved by symbolic computation. A similar polynomial system in distance coordinates to the vertices of a tetrahedron $T \subset \mathbb{R}^3$ is introduced to represent the configurations of four spheres of radius $R^*$, which intersect in one point, each sphere containing three vertices of $T$ but not the fourth one. This problem is related to that of computing the largest value $R$ for which the set of vertices of $T$ is an $R$-body. For triangular pyramids we completely describe the set of geometric configurations with the required four balls of radius $R^*$. The solutions obtained by symbolic computation show that triangular pyramids are splitted into two different classes: in the first one $R^*$ is unique, in the second one three values $R^*$ there exist. The first class can be itself subdivided into two subclasses, one of which is related to the family of $R$-bodies.

2024-05-25T10:25:38Z 24 pages, 6 figures, 3 appendices Marco Longinetti Simone Naldi http://arxiv.org/abs/2405.16936v2 2025-04-06T06:26:47Z

We provide effective methods to construct and manipulate trilinear birational maps $φ:(\mathbb{P}^1)^3\dashrightarrow \mathbb{P}^3$ by establishing a novel connection between birationality and tensor rank. These yield four families of nonlinear birational transformations between 3D spaces that can be operated with enough flexibility for applications in computer-aided geometric design. More precisely, we describe the geometric constraints on the defining control points of the map that are necessary for birationality, and present constructions for such configurations. For adequately constrained control points, we prove that birationality is achieved if and only if a certain $2\times 2\times 2$ tensor has rank one. As a corollary, we prove that the locus of weights that ensure birationality is $\mathbb{P}^1\times\mathbb{P}^1\times\mathbb{P}^1$. Additionally, we provide formulas for the inverse $φ^{-1}$ as well as the explicit defining equations of the irreducible components of the base loci. Finally, we introduce a notion of "distance to birationality" for trilinear rational maps, and explain how to continuously deform birational maps.

2024-05-27T08:28:09Z 30 pages, 12 figures. To appear in the SIAM Journal on Applied Algebra and Geometry (SIAGA) Laurent Busé Pablo Mazón http://arxiv.org/abs/2504.03913v1 2025-04-04T20:23:33Z

While most modern machine learning methods offer speed and accuracy, few promise interpretability or explainability -- two key features necessary for highly sensitive industries, like medicine, finance, and engineering. Using eight datasets representative of one especially sensitive industry, nuclear power, this work compares a traditional feedforward neural network (FNN) to a Kolmogorov-Arnold Network (KAN). We consider not only model performance and accuracy, but also interpretability through model architecture and explainability through a post-hoc SHAP analysis. In terms of accuracy, we find KANs and FNNs comparable across all datasets, when output dimensionality is limited. KANs, which transform into symbolic equations after training, yield perfectly interpretable models while FNNs remain black-boxes. Finally, using the post-hoc explainability results from Kernel SHAP, we find that KANs learn real, physical relations from experimental data, while FNNs simply produce statistically accurate results. Overall, this analysis finds KANs a promising alternative to traditional machine learning methods, particularly in applications requiring both accuracy and comprehensibility.

2025-04-04T20:23:33Z 35 pages, 11 Figures, 14 Tables Nataly R. Panczyk Omer F. Erdem Majdi I. Radaideh http://arxiv.org/abs/2504.02630v1 2025-04-03T14:28:13Z

The understanding and modeling of complex physical phenomena through dynamical systems has historically driven scientific progress, as it provides the tools for predicting the behavior of different systems under diverse conditions through time. The discovery of dynamical systems has been indispensable in engineering, as it allows for the analysis and prediction of complex behaviors for computational modeling, diagnostics, prognostics, and control of engineered systems. Joining recent efforts that harness the power of symbolic regression in this domain, we propose a novel framework for the end-to-end discovery of ordinary differential equations (ODEs), termed Grammar-based ODE Discovery Engine (GODE). The proposed methodology combines formal grammars with dimensionality reduction and stochastic search for efficiently navigating high-dimensional combinatorial spaces. Grammars allow us to seed domain knowledge and structure for both constraining, as well as, exploring the space of candidate expressions. GODE proves to be more sample- and parameter-efficient than state-of-the-art transformer-based models and to discover more accurate and parsimonious ODE expressions than both genetic programming- and other grammar-based methods for more complex inference tasks, such as the discovery of structural dynamics. Thus, we introduce a tool that could play a catalytic role in dynamics discovery tasks, including modeling, system identification, and monitoring tasks.

2025-04-03T14:28:13Z Karin L. Yu Eleni Chatzi Georgios Kissas 10.1016/j.ymssp.2025.113395 http://arxiv.org/abs/2504.00889v1 2025-04-01T15:18:28Z

We introduce the Brackets package for the computer algebra system Macaulay2, which provides convenient syntax for computations involving the classical invariants of the special linear group. We describe our implementation of bracket rings and Grassmann-Cayley algebras, and illustrate basic functionality such as the straightening algorithm on examples from projective and enumerative geometry.

2025-04-01T15:18:28Z 9 pages Dalton Bidleman Timothy Duff Jack Kendrick Michael Zeng http://arxiv.org/abs/2504.00263v1 2025-03-31T22:14:51Z

Conway's Game of Life (GOL) is a cellular automaton that has captured the interest of hobbyists and mathematicians alike for more than 50 years. The Game of Life is Turing complete, and people have been building increasingly sophisticated constructions within GOL, such as 8-bit displays, Turing machines, and even an implementation of GOL itself. In this paper, we report on a project to build an implementation of GOL within GOL, via logic circuits, fully formally verified within the HOL4 theorem prover. This required a combination of interactive tactic proving, symbolic simulation, and semi-automated forward proof to assemble the components into an infinite circuit which can calculate the next step of the simulation while respecting signal propagation delays. The result is a verified "GOL in GOL compiler" which takes an initial GOL state and returns a mega-cell version of it that can be passed to off-the-shelf GOL simulators, such as Golly. We believe these techniques are also applicable to other cellular automata, as well as for hardware verification which takes into account both the physical configuration of components and wire delays.

2025-03-31T22:14:51Z 17 pages, 5 figures, submitted to ITP 2025 Magnus O. Myreen Mario Carneiro