Search

The problem of finding a nonzero solution of a linear recurrence $Ly = 0$ with polynomial coefficients where $y$ has the form of a definite hypergeometric sum, related to the Inverse Creative Telescoping Problem of [14][Sec. 8], has now been open for three decades. Here we present an algorithm (implemented in a SageMath package) which, given such a recurrence and a quasi-triangular, shift-compatible factorial basis $\mathcal{B} = \langle P_k(n)\rangle_{k=0}^\infty$ of the polynomial space $\mathbb{K}[n]$ over a field $\mathbb{K}$ of characteristic zero, computes a recurrence satisfied by the coefficient sequence $c = \langle c_k\rangle_{k=0}^\infty$ of the solution $y_n = \sum_{k=0}^\infty c_kP_k(n)$ (where, thanks to the quasi-triangularity of $\mathcal{B}$, the sum on the right terminates for each $n \in \mathbb{N}$). More generally, if $\mathcal{B}$ is $m$-sieved for some $m \in \mathbb{N}$, our algorithm computes a system of $m$ recurrences satisfied by the $m$-sections of the coefficient sequence $c$. If an explicit nonzero solution of this system can be found, we obtain an explicit nonzero solution of $Ly = 0$., 62 pages

We study the relation between the Galois group $G$ of a linear difference-differential system and two classes $\mathcal{C}_1$ and $\mathcal{C}_2$ of groups that are the Galois groups of the specializations of the linear difference equation and the linear differential equation in this system respectively. We show that almost all groups in $\mathcal{C}_1\cup \mathcal{C}_2$ are algebraic subgroups of $G$, and there is a nonempty subset of $\mathcal{C}_1$ and a nonempty subset of $\mathcal{C}_2$ such that $G$ is the product of any pair of groups from these two subsets. These results have potential application to the computation of the Galois group of a linear difference-differential system. We also give a criterion for testing linear dependence of elements in a simple difference-differential ring, which generalizes Kolchin's criterion for partial differential fields., 32 pages

A Las Vegas randomized algorithm is given to compute the Smith multipliers for a nonsingular integer matrix $A$, that is, unimodular matrices $U$ and $V$ such that $AV=US$, with $S$ the Smith normal form of $A$. The expected running time of the algorithm is about the same as required to multiply together two matrices of the same dimension and size of entries as $A$. Explicit bounds are given for the size of the entries in both unimodular multipliers. The main tool used by the algorithm is the Smith massager, a relaxed version of $V$, the unimodular matrix specifying the column operations of the Smith computation. From the perspective of efficiency, the main tools used are fast linear solving and partial linearization of integer matrices. As an application of the Smith with multipliers algorithm, a fast algorithm is given to find the fractional part of the inverse of the input matrix., 41 pages

We propose a new symbolic algorithm and a C++ program for generating and calculating supersymmetric Feynman diagrams for ${\cal N}=1$ supersymmetric electrodynamics regularized by higher derivatives in four dimensions. According to standard rules, the program generates all diagrams that are necessary to calculate a specific contribution to the two-point Green function of matter superfields in the needed order, and then reduces the answer to the sum of Euclidean momentum integrals. At the moment, the program was used to calculate the anomalous dimension in ${\cal N}=1$ supersymmetric quantum electrodynamics, regularized by higher derivatives, in the three-loop approximation., 14 pages, 1 figure, accepted for publication in "Programming and Computer Software"

The second-order cone (SOC) is a class of simple convex cones and optimizing over them can be done more efficiently than with semidefinite programming. It is interesting both in theory and in practice to investigate which convex cones admit a representation using SOCs, given that they have a strong expressive ability. In this paper, we prove constructively that the cone of sums of nonnegative circuits (SONC) admits a SOC representation. Based on this, we give a new algorithm for unconstrained polynomial optimization via SOC programming. We also provide a hybrid numeric-symbolic scheme which combines the numerical procedure with a rounding-projection algorithm to obtain exact nonnegativity certificates. Numerical experiments demonstrate the efficiency of our algorithm for polynomials with fairly large degree and number of variables., 29 pages, 7 tables, 6 figures, extended version of the article published in the proceedings of ISSAC 2020. arXiv admin note: text overlap with arXiv:1906.06179

We consider the problem of computing the topology and describing the geometry of a parametric curve in $\mathbb{R}^n$. We present an algorithm, PTOPO, that constructs an abstract graph that is isotopic to the curve in the embedding space. Our method exploits the benefits of the parametric representation and does not resort to implicitization. Most importantly, we perform all computations in the parameter space and not in the implicit space. When the parametrization involves polynomials of degree at most $d$ and maximum bitsize of coefficients $\tau$, then the worst case bit complexity of PTOPO is $ \tilde{\mathcal{O}}_B(nd^6+nd^5\tau+d^4(n^2+n\tau)+d^3(n^2\tau+ n^3)+n^3d^2\tau)$. This bound matches the current record bound $\tilde{\mathcal{O}}_B(d^6+d^5\tau)$ for the problem of computing the topology of a plane algebraic curve given in implicit form. For plane and space curves, if $N = \max\{d, \tau \}$, the complexity of PTOPO becomes $\tilde{\mathcal{O}}_B(N^6)$, which improves the state-of-the-art result, due to Alc\'azar and D\'iaz-Toca [CAGD'10], by a factor of $N^{10}$. In the same time complexity, we obtain a graph whose straight-line embedding is isotopic to the curve. However, visualizing the curve on top of the abstract graph construction, increases the bound to $\tilde{\mathcal{O}}_B(N^7)$. For curves of general dimension, we can also distinguish between ordinary and non-ordinary real singularities and determine their multiplicities in the same expected complexity of PTOPO by employing the algorithm of Blasco and P\'erez-D\'iaz [CAGD'19]. We have implemented PTOPO in Maple for the case of plane and space curves. Our experiments illustrate its practical nature.

Signature-based algorithms have become a standard approach for computing Gr\"obner bases in commutative polynomial rings. However, so far, it was not clear how to extend this concept to the setting of noncommutative polynomials in the free algebra. In this paper, we present a signature-based algorithm for computing Gr\"obner bases in precisely this setting. The algorithm is an adaptation of Buchberger's algorithm including signatures. We prove that our algorithm correctly enumerates a signature Gr\"obner basis as well as a Gr\"obner basis of the module generated by the leading terms of the generators' syzygies, and that it terminates whenever the ideal admits a finite signature Gr\"obner basis. Additionally, we adapt well-known signature-based criteria eliminating redundant reductions, such as the syzygy criterion, the F5 criterion and the singular criterion, to the case of noncommutative polynomials. We also generalize reconstruction methods from the commutative setting that allow to recover, from partial information about signatures, the coordinates of elements of a Gr\"obner basis in terms of the input polynomials, as well as a basis of the syzygy module of the generators. We have written a toy implementation of all the algorithms in the Mathematica package OperatorGB and we compare our signature-based algorithm to the classical Buchberger algorithm for noncommutative polynomials., Comment: 31 pages, 2 pages appendix, 1 figure

We consider the problem of answering connectivity queries on a real algebraic curve. The curve is given as the real trace of an algebraic curve, assumed to be in generic position, and being defined by some rational parametrizations. The query points are given by a zero-dimensional parametrization. We design an algorithm which counts the number of connected components of the real curve under study, and decides which query point lie in which connected component, in time log-linear in $N^6$, where $N$ is the maximum of the degrees and coefficient bit-sizes of the polynomials given as input. This matches the currently best-known bound for computing the topology of real plane curves. The main novelty of this algorithm is the avoidance of the computation of the complete topology of the curve., Comment: 10 pages, 2 figures

This paper addresses the computational problem of deciding invertibility (or one to one-ness) of a Boolean map $F$ in $n$-Boolean variables. This problem has a special case of deciding invertibilty of a map $F:\mathbb{F}_{2}^n\rightarrow\mathbb{F}_{2}^n$ over the binary field $\mathbb{F}_2$. Further the problem can be extended and stated over a finite field $\mathbb{F}$ instead of $\mathbb{F}_2$. Algebraic condition for invertibility of $F$ in this special case over a finite field is well known to be equivalent to invertibility of the Koopman operator of $F$ as shown in \cite{RamSule}. In this paper a condition for invertibility is derived in the special case of Boolean maps $F:B_0^n\rightarrow B_0^n$ where $B_0$ is the two element Boolean algebra in terms of \emph{implicants} of Boolean equations. This condition is then extended to the case of general maps in $n$ variables. Hence this condition answers the special case of invertibility of the map $F$ defined over the binary field $\mathbb{F}_2$ alternatively, in terms of implicants instead of the Koopman operator. The problem of deciding invertibility of a map $F$ (or that of finding its $GOE$) over finite fields appears to be distinct from the satisfiability problem (SAT) or the problem of deciding consistency of polynomial equations over finite fields. Hence the well known algorithms for deciding SAT or of solvability using Grobner basis for checking membership in an ideal generated by polynomials is not known to answer the question of invertibility of a map. Similarly it appears that algorithms for satisfiability or polynomial solvability are not useful for computation of $GOE(F)$ even for maps over the binary field $\mathbb{F}_2$., 15 pages

In classical logic, nonBoolean fluents, such as the location of an object, can be naturally described by functions. However, this is not the case in answer set programs, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions -- functions that are specified by a logic program just like predicates are specified. We show that many known properties of the stable model semantics are naturally extended to this formalism and compare it with other related approaches to incorporating intensional functions. Furthermore, we use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT), analogous to the way that Satisfiability Modulo Theories (SMT) is defined, allowing for SMT-like effective first-order reasoning in the context of ASP. Using SMT solving techniques involving functions, ASPMT can be applied to domains containing real numbers and alleviates the grounding problem. We show that other approaches to integrating ASP and CSP/SMT can be related to special cases of ASPMT in which functions are limited to non-intensional ones., 69 pages

Large language models (LLMs), such as GPT-3 and GPT-4, have demonstrated exceptional performance in various natural language processing tasks and have shown the ability to solve certain reasoning problems. However, their reasoning capabilities are limited and relatively shallow, despite the application of various prompting techniques. In contrast, formal logic is adept at handling complex reasoning, but translating natural language descriptions into formal logic is a challenging task that non-experts struggle with. This paper proposes a neuro-symbolic method that combines the strengths of large language models and answer set programming. Specifically, we employ an LLM to transform natural language descriptions of logic puzzles into answer set programs. We carefully design prompts for an LLM to convert natural language descriptions into answer set programs in a step by step manner. Surprisingly, with just a few in-context learning examples, LLMs can generate reasonably complex answer set programs. The majority of errors made are relatively simple and can be easily corrected by humans, thus enabling LLMs to effectively assist in the creation of answer set programs., 17 pages, KR 2023

While large language models (LLMs), such as GPT-3, appear to be robust and general, their reasoning ability is not at a level to compete with the best models trained for specific natural language reasoning problems. In this study, we observe that a large language model can serve as a highly effective few-shot semantic parser. It can convert natural language sentences into a logical form that serves as input for answer set programs, a logic-based declarative knowledge representation formalism. The combination results in a robust and general system that can handle multiple question-answering tasks without requiring retraining for each new task. It only needs a few examples to guide the LLM's adaptation to a specific task, along with reusable ASP knowledge modules that can be applied to multiple tasks. We demonstrate that this method achieves state-of-the-art performance on several NLP benchmarks, including bAbI, StepGame, CLUTRR, and gSCAN. Additionally, it successfully tackles robot planning tasks that an LLM alone fails to solve., 32 pages, Findings of the Association for Computational Linguistics: ACL 2023, 5186-5219

This paper discusses and evaluates ideas of data balancing and data augmentation in the context of mathematical objects: an important topic for both the symbolic computation and satisfiability checking communities, when they are making use of machine learning techniques to optimise their tools. We consider a dataset of non-linear polynomial problems and the problem of selecting a variable ordering for cylindrical algebraic decomposition to tackle these with. By swapping the variable names in already labelled problems, we generate new problem instances that do not require any further labelling when viewing the selection as a classification problem. We find this augmentation increases the accuracy of ML models by 63% on average. We study what part of this improvement is due to the balancing of the dataset and what is achieved thanks to further increasing the size of the dataset, concluding that both have a very significant effect. We finish the paper by reflecting on how this idea could be applied in other uses of machine learning in mathematics., 10 pages. To be presented at the 2023 SC-Square Workshop

This paper presents the main features of a system that aims to transform regular expressions into shorter equivalent expressions. The system is also capable of computing other operations useful for simplification, such as checking the inclusion of regular languages. The main novelty of this work is that it combines known but distinct ways of representing regular languages into a global unified data structure that makes the operations more efficient. In addition, representations of regular languages are dynamically reduced as operations are performed on them. Expressions are normalized and represented by a unique identifier (an integer). Expressions found to be equivalent (i.e. denoting the same regular language) are grouped into equivalence classes from which a shortest representative is chosen. The article briefly describes the main algorithms working on the global data structure. Some of them are direct adaptations of well-known algorithms, but most of them incorporate new ideas, which are really necessary to make the system efficient. Finally, to show its usefulness, the system is applied to some examples from the literature. Statistics on randomly generated sets of expressions are also provided., rejected at ATVA 2023

In this work, following the intuition that adverbs describing scene-sequences are best identified by reasoning over high-level concepts of object-behavior, we propose the design of a new framework that reasons over object-behaviours extracted from raw-video-clips to recognize the clip's corresponding adverb-types. Importantly, while previous works for general scene adverb-recognition assume knowledge of the clips underlying action-types, our method is directly applicable in the more general problem setting where the action-type of a video-clip is unknown. Specifically, we propose a novel pipeline that extracts human-interpretable object-behaviour-facts from raw video clips and propose novel symbolic and transformer based reasoning methods that operate over these extracted facts to identify adverb-types. Experiment results demonstrate that our proposed methods perform favourably against the previous state-of-the-art. Additionally, to support efforts in symbolic video-processing, we release two new datasets of object-behaviour-facts extracted from raw video clips - the MSR-VTT-ASP and ActivityNet-ASP datasets.

We introduce a just-in-time runtime program transformation based on repeated recursion unfolding. Our online polyvariant program specialization generates several versions of a recursion differentiated by the minimal number of recursive steps covered. The base case of the recursion is ignored in our technique. Our method is presented here on the basis of linear direct recursive rules. When a recursive call is encountered at runtime, first an unfolder creates specializations of the associated recursive rule on-the-fly and then an interpreter applies these rules to the call. Our approach reduces the number of recursive rule applications to its logarithm at the expense of introducing a logarithmic number of unfolded rules. Each rule is applied at most once. We prove correctness of our technique and determine its worst-case time complexity. For recursions that solve tractable problems and which have enough unfoldings that can sufficiently simplified, we prove a super-linear speedup theorem, i.e. speedup by more than a constant factor. The simplification is problem-specific and has to be provided at compile-time. In the best case, the complexity of the given recursion is reduced to that of its first recursive step. We have implemented the necessary unfolder and meta-interpreter for runtime repeated recursion unfolding in Constraint Handling Rules (CHR) with just five rules. We illustrate the feasibility of our approach with complexity results and benchmarks for several classical algorithms. The runtime improvement quickly reaches several orders of magnitude., Submitted to Journal Fundamenta Informaticae

Fuchs' Theorem on the solutions of ordinary linear differential equations with regular singularities is extended to positive characteristic by proving a normal form theorem for the respective linear differential operators. This yields an explicit algorithm to compute a basis of solutions in characteristic p., 40 pages

The solution set of a system of polynomial equations typically contains ill-behaved, singular points. Resolution is a fundamental process in geometry in which we replace singular points with smooth points, while keeping the rest of the solution set unchanged. Resolutions are not unique: the usual way to describe them involves repeatedly performing a fundamental operation known as "blowing-up", and the complexity of the resolution highly depends on certain choices. The process can be translated into various versions of a 2-player game, the so-called Hironaka game, and a winning strategy for the first player provides a solution to the resolution problem. In this paper we introduce a new approach to the Hironaka game that uses reinforcement learning agents to find optimal resolutions of singularities. In certain domains, the trained model outperforms state-of-the-art selection heuristics in total number of polynomial additions performed, which provides a proof-of-concept that recent developments in machine learning have the potential to improve performance of algorithms in symbolic computation., To appear in Proceedings of the 40th International Conference on Machine Learning TAG Workshop (ICML-TAG 2023)

We propose a symbolic-numeric algorithm to count the number of solutions of a polynomial system within a local region. More specifically, given a zero-dimensional system $f_1=\cdots=f_n=0$, with $f_i\in\mathbb{C}[x_1,\ldots,x_n]$, and a polydisc $\mathbf{\Delta}\subset\mathbb{C}^n$, our method aims to certify the existence of $k$ solutions (counted with multiplicity) within the polydisc. In case of success, it yields the correct result under guarantee. Otherwise, no information is given. However, we show that our algorithm always succeeds if $\mathbf{\Delta}$ is sufficiently small and well-isolating for a $k$-fold solution $\mathbf{z}$ of the system. Our analysis of the algorithm further yields a bound on the size of the polydisc for which our algorithm succeeds under guarantee. This bound depends on local parameters such as the size and multiplicity of $\mathbf{z}$ as well as the distances between $\mathbf{z}$ and all other solutions. Efficiency of our method stems from the fact that we reduce the problem of counting the roots in $\mathbf{\Delta}$ of the original system to the problem of solving a truncated system of degree $k$. In particular, if the multiplicity $k$ of $\mathbf{z}$ is small compared to the total degrees of the polynomials $f_i$, our method considerably improves upon known complete and certified methods. For the special case of a bivariate system, we report on an implementation of our algorithm, and show experimentally that our algorithm leads to a significant improvement, when integrated as inclusion predicate into an elimination method.

Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of systems from integrated circuits to cyber-physical systems. Typically, BMC is performed by checking satisfiability of a possibly long, but quantifier-free formula. However, BMC problems can naturally be encoded as quantified formulas over the number of BMC steps. In this approach, we then use decision procedures supporting quantifiers to check satisfiability of these quantified formulas. This approach has previously been applied to perform BMC using a Quantified Boolean Formula (QBF) encoding for purely discrete systems, and then discharges the QBF checks using QBF solvers. In this paper, we present a new quantified encoding of BMC for rectangular hybrid automata (RHA), which requires using more general logics due to the real (dense) time and real-valued state variables modeling continuous states. We have implemented a preliminary experimental prototype of the method using the HyST model transformation tool to generate the quantified BMC (QBMC) queries for the Z3 SMT solver. We describe experimental results on several timed and hybrid automata benchmarks, such as the Fischer and Lynch-Shavit mutual exclusion algorithms. We compare our approach to quantifier-free BMC approaches, such as those in the dReach tool that uses the dReal SMT solver, and the HyComp tool built on top of nuXmv that uses the MathSAT SMT solver. Based on our promising experimental results, QBMC may in the future be an effective and scalable analysis approach for RHA and other classes of hybrid automata as further improvements are made in quantifier handling in SMT solvers such as Z3., Comment: In Proceedings SNR 2021, arXiv:2207.04391

This paper presents an approach for verifying the behaviour of nonlinear Artificial Neural Networks (ANNs) found in cyber-physical safety-critical systems. We implement a dedicated interval constraint propagator for the sigmoid function into the SMT solver iSAT and compare this approach with a compositional approach encoding the sigmoid function by basic arithmetic features available in iSAT and an approximating approach. Our experimental results show that the dedicated and the compositional approach clearly outperform the approximating approach. Throughout all our benchmarks, the dedicated approach showed an equal or better performance compared to the compositional approach., In Proceedings SNR 2021, arXiv:2207.04391

We provide an algorithm to compute an effective description of the homology of complex projective hypersurfaces relying on Picard-Lefschetz theory. Next, we use this description to compute high-precision numerical approximations of the periods of the hypersurface. This is an improvement over existing algorithms as this new method allows for the computation of periods of smooth quartic surfaces in an hour on a laptop, which could not be attained with previous methods. The general theory presented in this paper can be generalised to varieties other than just hypersurfaces, such as elliptic fibrations as showcased on an example coming from Feynman graphs. Our algorithm comes with a SageMath implementation., 35 pages

We present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra -- fral -- and a free extension -- frex -- of an algebra by a set of variables. The library's dependently-typed API guarantees simplification modules, even user-defined ones, are terminating, sound, and complete with respect to a well-specified class of equations. Completeness offers intangible benefits in practice -- our main contribution is the novel design. Cleanly separating between the interface and implementation of simplification modules provides two new modularity axes. First, simplification modules share thousands of lines of infrastructure code dealing with term-representation, pretty-printing, certification, and macros/reflection. Second, new simplification modules can reuse existing ones. We demonstrate this design by developing simplification modules for monoid varieties: ordinary, commutative, and involutive. We implemented this design in the new Idris2 dependently-typed programming language, and in Agda.

We investigate the role of attention and memory in complex reasoning tasks. We analyze Transformer-based self-attention as a model and extend it with memory. By studying a synthetic visual reasoning test, we refine the taxonomy of reasoning tasks. Incorporating self-attention with ResNet50, we enhance feature maps using feature-based and spatial attention, achieving efficient solving of challenging visual reasoning tasks. Our findings contribute to understanding the attentional needs of SVRT tasks. Additionally, we propose GAMR, a cognitive architecture combining attention and memory, inspired by active vision theory. GAMR outperforms other architectures in sample efficiency, robustness, and compositionality, and shows zero-shot generalization on new reasoning tasks., PhD Thesis, 152 pages, 32 figures, 6 tables

We address univariate root isolation when the polynomial's coefficients are in a multiple field extension. We consider a polynomial $F \in L[Y]$, where $L$ is a multiple algebraic extension of $\mathbb{Q}$. We provide aggregate bounds for $F$ and algorithmic and bit-complexity results for the problem of isolating its roots. For the latter problem we follow a common approach based on univariate root isolation algorithms. For the particular case where $F$ does not have multiple roots, we achieve a bit-complexity in $\tilde{\mathcal{O}}_B(n d^{2n+2}(d+n\tau))$, where $d$ is the total degree and $\tau$ is the bitsize of the involved polynomials.In the general case we need to enhance our algorithm with a preprocessing step that determines the number of distinct roots of $F$. We follow a numerical, yet certified, approach that has bit-complexity $\tilde{\mathcal{O}}_B(n^2d^{3n+3}\tau + n^3 d^{2n+4}\tau)$.

For various $2\leq n,m \leq 6$, we propose some new algorithms for multiplying an $n\times m$ matrix with an $m \times 6$ matrix over a possibly noncommutative coefficient ring., 9 pages

This tutorial paper provides a general overview of symbolic regression (SR) with specific focus on standards of interpretability. We posit that interpretable modeling, although its definition is still disputed in the literature, is a practical way to support the evaluation of successful information fusion. In order to convey the benefits of SR as a modeling technique, we demonstrate an application within the field of health and nutrition using publicly available National Health and Nutrition Examination Survey (NHANES) data from the Centers for Disease Control and Prevention (CDC), fusing together anthropometric markers into a simple mathematical expression to estimate body fat percentage. We discuss the advantages and challenges associated with SR modeling and provide qualitative and quantitative analyses of the learned models.

Inequalities among symmetric functions are fundamental questions in mathematics and have various applications in science and engineering. In this paper, we tackle a conjecture about inequalities among the complete homogeneous symmetric function $H_{n,\lambda}$, that is, the inequality $H_{n,\lambda}\leq H_{n,\mu}$ implies majorization order $\lambda\preceq\mu$. This conjecture was proposed by Cuttler, Greene and Skandera in 2011. The conjecture is a close analogy with other known results on Muirhead-type inequalities. In 2021, Heaton and Shankar disproved the conjecture by showing a counterexample for degree $d=8$ and number of variables $n=3$. They then asked whether the conjecture is true when~ the number of variables, $n$, is large enough? In this paper, we answer the question by proving that the conjecture does not hold when $d\geq8$ and $n\geq2$. A crucial step of the proof relies on variables reduction. Inspired by this, we propose a new conjecture for $H_{n,\lambda}\leq H_{n,\mu}$., Comment: 14 pages

Computational modeling of neurodynamical systems often deploys neural networks and symbolic dynamics. A particular way for combining these approaches within a framework called vector symbolic architectures leads to neural automata. An interesting research direction we have pursued under this framework has been to consider mapping symbolic dynamics onto neurodynamics, represented as neural automata. This representation theory, enables us to ask questions, such as, how does the brain implement Turing computations. Specifically, in this representation theory, neural automata result from the assignment of symbols and symbol strings to numbers, known as G\"odel encoding. Under this assignment symbolic computation becomes represented by trajectories of state vectors in a real phase space, that allows for statistical correlation analyses with real-world measurements and experimental data. However, these assignments are usually completely arbitrary. Hence, it makes sense to address the problem question of, which aspects of the dynamics observed under such a representation is intrinsic to the dynamics and which are not. In this study, we develop a formally rigorous mathematical framework for the investigation of symmetries and invariants of neural automata under different encodings. As a central concept we define patterns of equality for such systems. We consider different macroscopic observables, such as the mean activation level of the neural network, and ask for their invariance properties. Our main result shows that only step functions that are defined over those patterns of equality are invariant under recodings, while the mean activation is not. Our work could be of substantial importance for related regression studies of real-world measurements with neurosymbolic processors for avoiding confounding results that are dependant on a particular encoding and not intrinsic to the dynamics., Comment: 28 pages, 8 figures

It is shown how to compute quotients efficiently in non-commutative univariate polynomial rings. This extends earlier work where efficient generic quotients were studied with a primary focus on commutative domains. Fast algorithms are given for left and right quotients of polynomials where the variable commutes with coefficients. These algorithms are based on the concept of the ``whole shifted inverse'', which is a specialized quotient where the dividend is a power of the polynomial variable. It is also shown that when the variable does not commute with coefficients, that is for skew polynomials, left and right whole shifted inverses are defined and may be used to compute right and left quotients. In this case their computation is not asymptotically fast, but once obtained, they may be used to compute multiple quotients, each with one multiplication. Examples are shown of polynomials with matrix coefficients, differential operators and difference operators. In addition, a proof-of-concept generic Maple implementations is given.

From the literature it is known that orthogonal polynomials as the Jacobi polynomials can be expressed by hypergeometric series. In this paper, the authors derive several contiguous relations for terminating multivariate hypergeometric series. With these contiguous relations one can prove several recursion formulas of those series. This theoretical result allows to compute integrals over products of Jacobi polynomials in a very efficient recursive way. Moreover, the authors present an application to numerical analysis where it can be used in algorithms which compute the approximate solution of boundary value problem of partial differential equations by means of the finite elements method. With the aid of the contiguous relations, the approximate solution can be computed much faster than using numerical integration. A numerical example illustrates this effect.

A piecewise linear function can be described in different forms: as an arbitrarily nested expression of $\min$- and $\max$-functions, as a difference of two convex piecewise linear functions, or as a linear combination of maxima of affine-linear functions. In this paper, we provide two main results: first, we show that for every piecewise linear function there exists a linear combination of $\max$-functions with at most $n+1$ arguments, and give an algorithm for its computation. Moreover, these arguments are contained in the finite set of affine-linear functions that coincide with the given function in some open set. Second, we prove that the piecewise linear function $\max(0, x_{1}, \ldots, x_{n})$ cannot be represented as a linear combination of maxima of less than $n+1$ affine-linear arguments. This was conjectured by Wang and Sun in 2005 in a paper on representations of piecewise linear functions as linear combination of maxima.

We tackle the problem of neural machine translation of mathematical formulae between ambiguous presentation languages and unambiguous content languages. Compared to neural machine translation on natural language, mathematical formulae have a much smaller vocabulary and much longer sequences of symbols, while their translation requires extreme precision to satisfy mathematical information needs. In this work, we perform the tasks of translating from LaTeX to Mathematica as well as from LaTeX to semantic LaTeX. While recurrent, recursive, and transformer networks struggle with preserving all contained information, we find that convolutional sequence-to-sequence networks achieve 95.1% and 90.7% exact matches, respectively., Published at ACL 2023

In nature, the behaviors of many complex systems can be described by parsimonious math equations. Automatically distilling these equations from limited data is cast as a symbolic regression process which hitherto remains a grand challenge. Keen efforts in recent years have been placed on tackling this issue and demonstrated success in symbolic regression. However, there still exist bottlenecks that current methods struggle to break when the discrete search space tends toward infinity and especially when the underlying math formula is intricate. To this end, we propose a novel Reinforcement Symbolic Regression Machine (RSRM) that masters the capability of uncovering complex math equations from only scarce data. The RSRM model is composed of three key modules: (1) a Monte Carlo tree search (MCTS) agent that explores optimal math expression trees consisting of pre-defined math operators and variables, (2) a Double Q-learning block that helps reduce the feasible search space of MCTS via properly understanding the distribution of reward, and (3) a modulated sub-tree discovery block that heuristically learns and defines new math operators to improve representation ability of math expression trees. Biding of these modules yields the state-of-the-art performance of RSRM in symbolic regression as demonstrated by multiple sets of benchmark examples. The RSRM model shows clear superiority over several representative baseline models., 18 pages

This paper is devoted to the study of infinitesimal limit cycles that can bifurcate from zero-Hopf equilibria of differential systems based on the averaging method. We develop an efficient symbolic program using Maple for computing the averaged functions of any order for continuous differential systems in arbitrary dimension. The program allows us to systematically analyze zero-Hopf bifurcations of polynomial differential systems using symbolic computation methods. We show that for the first-order averaging, $\ell\in\{0,1,\ldots,2^{n-3}\}$ limit cycles can bifurcate from the zero-Hopf equilibrium for the general class of perturbed differential systems and up to the second-order averaging, the maximum number of limit cycles can be determined by computing the mixed volume of a polynomial system obtained from the averaged functions. A number of examples are presented to demonstrate the effectiveness of the proposed algorithmic approach., The 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023). arXiv admin note: text overlap with arXiv:2205.14450

We propose a two-step Newton's method for refining an approximation of a singular zero whose deflation process terminates after one step, also known as a deflation-one singularity. Given an isolated singular zero of a square analytic system, our algorithm exploits an invertible linear operator obtained by combining the Jacobian and a projection of the Hessian in the direction of the kernel of the Jacobian. We prove the quadratic convergence of the two-step Newton method when it is applied to an approximation of a deflation-one singular zero. Also, the algorithm requires a smaller size of matrices than the existing methods, making it more efficient. We demonstrate examples and experiments to show the efficiency of the method., 22pages, 1 figure, 4 tables

We survey recent progress on efficient algorithms for approximately diagonalizing a square complex matrix in the models of rational (variable precision) and finite (floating point) arithmetic. This question has been studied across several research communities for decades, but many mysteries remain. We present several open problems which we hope will be of broad interest., 11pp. Invited survey for ISSAC 2023. Comments welcome

We describe a recently developed algebraic framework for proving first-order statements about linear operators by computations with noncommutative polynomials. Furthermore, we present our new SageMath package operator_gb, which offers functionality for automatising such computations. We aim to provide a practical understanding of our approach and the software through examples, while also explaining the completeness of the method in the sense that it allows to find algebraic proofs for every true first-order operator statement. We illustrate the capability of the framework in combination with our software by a case study on statements about the Moore-Penrose inverse, including classical facts and recent results, presented in an online notebook., 22 pages, plus 8 additional pages appendix

In this paper we study power series with coefficients equal to a product of a generic sequence and an explicitly given function of a positive parameter expressible in terms of the Pochhammer symbols. Four types of such series are treated. We show that logarithmic concavity (convexity) of the generic sequence leads to logarithmic concavity (convexity) of the sum of the series with respect to the argument of the explicitly given function. The logarithmic concavity (convexity) is derived from a stronger property, \ie, positivity (negativity) of the power series coefficients of the so-called generalized Tur\'{a}nian. Applications to special functions such as the generalized hypergeometric function and the Fox-Wright function are also discussed., Comment: 20 pages; no figures

We study polynomial systems with prescribed monomial supports in the Cox rings of toric varieties built from complete polyhedral fans. We present combinatorial formulas for the dimensions of their associated subvarieties under genericity assumptions on the coefficients of the polynomials. Using these formulas, we identify at which degrees generic systems in polytopal algebras form regular sequences. Our motivation comes from sparse elimination theory, where knowing the expected dimension of these subvarieties leads to specialized algorithms and to large speed-ups for solving sparse polynomial systems. As a special case, we classify the degrees at which regular sequences defined by weighted homogeneous polynomials can be found, answering an open question in the Gr\"obner bases literature. We also show that deciding whether a sparse system is generically a regular sequence in a polytopal algebra is hard from the point of view of theoretical computational complexity.

We establish how the coefficients of a sparse polynomial system influence the sum (or the trace) of its zeros. As an application, we develop numerical tests for verifying whether a set of solutions to a sparse system is complete. These algorithms extend the classical trace test in numerical algebraic geometry. Our results rely on both the analysis of the structure of sparse resultants as well as an extension of Esterov’s results on monodromy groups of sparse systems.

In recent years, several reaction templates-based and template-free approaches have been reported for single-step retrosynthesis prediction. Even though many of these approaches perform well from traditional data-driven metrics standpoint, there is a disconnect between model architectures used and underlying chemistry principles governing retrosynthesis. Here, we propose a novel chemistry-aware retrosynthesis prediction framework that combines powerful data-driven models with chemistry knowledge. We report a tree-to-sequence transformer architecture based on hierarchical SMILES grammar trees as input containing underlying chemistry information that is otherwise ignored by models based on purely SMILES-based representations. The proposed framework, grammar-based molecular attention tree transformer (G-MATT), achieves significant performance improvements compared to baseline retrosynthesis models. G-MATT achieves a top-1 accuracy of 51% (top-10 accuracy of 79.1%), invalid rate of 1.5%, and bioactive similarity rate of 74.8%. Further analyses based on attention maps demonstrate G-MATT's ability to preserve chemistry knowledge without having to use extremely complex model architectures.

Polynomial factorization and root finding are among the most standard themes of computational mathematics. Yet still, little has been done for polynomials over quaternion algebras, with the single exception of Hamiltonian quaternions for which there are known numerical methods for polynomial root approximation. The sole purpose of the present paper is to present a polynomial factorization algorithm for division quaternion algebras over number fields, together with its adaptation for root finding.

We study the Lüroth problem for partial differential fields. The main result is the following partial differential analog of generalized Lüroth's theorem: Let $\mathcal{F}$ be a differential field of characteristic 0 with $m$ derivation operators, $\textbf{u}=u_1,\ldots,u_n$ a set of differential indeterminates over $\mathcal{F}$. We prove that an intermediate differential field $\mathcal{G}$ between $\mathcal{F}$ and $\mathcal{F}\langle \textbf{u}\rangle$ is a simple differential extension of $\mathcal{F}$ if and only if the differential dimension polynomial of $\textbf{u}$ over $\mathcal{G}$ is of the form $ω_{\textbf{u}/\mathcal{G}}(t)=n{t+m\choose m}-{t+m-s\choose m}$ for some $s\in\mathbb N$. This result generalizes the classical differential Lüroth's theorem proved by Ritt and Kolchin in the case $m=n=1$. We then present an algorithm to decide whether a given finitely generated differential extension field of $\mathcal{F}$ contained in $\mathcal{F}\langle \textbf{u}\rangle$ is a simple extension, and in the affirmative case, to compute a Lüroth generator. As an application, we solve the proper re-parameterization problem for unirational differential curves., 19 pages

We present the first implementation of Drinfeld modules fully integrated in the SageMath ecosystem. First features will be released with SageMath 10.0.

This paper focuses on the study of the order of power series that are linear combinations of a given finite set of power series. The order of a formal power series, known as $\textrm{ord}(f)$, is defined as the minimum exponent of $x$ that has a non-zero coefficient in $f(x)$. Our first result is that the order of the Wronskian of these power series is equivalent up to a polynomial factor, to the maximum order which occurs in the linear combination of these power series. This implies that the Wronskian approach used in (Kayal and Saha, TOCT'2012) to upper bound the order of sum of square roots is optimal up to a polynomial blowup. We also demonstrate similar upper bounds, similar to those of (Kayal and Saha, TOCT'2012), for the order of power series in a variety of other scenarios. We also solve a special case of the inequality testing problem outlined in (Etessami et al., TOCT'2014). In the second part of the paper, we study the equality variant of the sum of square roots problem, which is decidable in polynomial time due to (Bl\"omer, FOCS'1991). We investigate a natural generalization of this problem when the input integers are given as straight line programs. Under the assumption of the Generalized Riemann Hypothesis (GRH), we show that this problem can be reduced to the so-called ``one dimensional'' variant. We identify the key mathematical challenges for solving this ``one dimensional'' variant.

In this paper we introduce a multistep generalization of the guess-and-determine or hybrid strategy for solving a system of multivariate polynomial equations over a finite field. In particular, we propose performing the exhaustive evaluation of a subset of variables stepwise, that is, by incrementing the size of such subset each time that an evaluation leads to a polynomial system which is possibly unfeasible to solve. The decision about which evaluation to extend is based on a preprocessing consisting in computing an incomplete Grobner basis after the current evaluation, which possibly generates linear polynomials that are used to eliminate further variables. If the number of remaining variables in the system is deemed still too high, the evaluation is extended and the preprocessing is iterated. Otherwise, we solve the system by a Grobner basis computation. Having in mind cryptanalytic applications, we present an implementation of this strategy in an algorithm called MultiSolve which is designed for polynomial systems having at most one solution. We prove explicit formulas for its complexity which are based on probability distributions that can be easily estimated by performing the proposed preprocessing on a testset of evaluations for different subsets of variables. We prove that an optimal complexity of MultiSolve is achieved by using a full multistep strategy with a maximum number of steps and in turn the classical guess-and-determine strategy, which essentially is a strategy consisting of a single step, is the worst choice. Finally, we extensively study the behaviour of MultiSolve when performing an algebraic attack on the well-known stream cipher Trivium., 27 pages

Given a linear differential equation with coefficients in $\mathbb{Q}(x)$, an important question is to know whether its full space of solutions consists of algebraic functions, or at least if one of its specific solutions is algebraic. After presenting motivating examples coming from various branches of mathematics, we advertise in an elementary way a beautiful local-global arithmetic approach to these questions, initiated by Grothendieck in the late sixties. This approach has deep ramifications and leads to the still unsolved Grothendieck-Katz $p$-curvature conjecture., 47 pages

Recent work on neuro-symbolic inductive logic programming has led to promising approaches that can learn explanatory rules from noisy, real-world data. While some proposals approximate logical operators with differentiable operators from fuzzy or real-valued logic that are parameter-free thus diminishing their capacity to fit the data, other approaches are only loosely based on logic making it difficult to interpret the learned ``rules". In this paper, we propose learning rules with the recently proposed logical neural networks (LNN). Compared to others, LNNs offer a strong connection to classical Boolean logic thus allowing for precise interpretation of learned rules while harboring parameters that can be trained with gradient-based optimization to effectively fit the data. We extend LNNs to induce rules in first-order logic. Our experiments on standard benchmarking tasks confirm that LNN rules are highly interpretable and can achieve comparable or higher accuracy due to their flexible parameterization.

Linear recurrence equations with constant coefficients define the power series coefficients of rational functions. However, one usually prefers to have an explicit formula for the sequence of coefficients, provided that such a formula is "simple" enough. Simplicity is related to the compactness of the formula due to the presence of algebraic numbers: "the smaller, the simpler". This poster showcases the capacity of recent updates on the Formal Power Series (FPS) algorithm, implemented in Maxima and Maple (convert/FormalPowerSeries), to find simple formulas for sequences like those from https://oeis.org/A307717, https://oeis.org/A226782, or https://oeis.org/A226784 by computing power series representations of their correctly guessed generating functions. We designed the algorithm for the more general context of univariate $P$-recursive sequences. Our implementations are available at http://www.mathematik.uni-kassel.de/~bteguia/FPS_webpage/FPS.htm, 5 pages, 15 references, ISSAC'22 poster presentation