https://arxiv.org/api/VIS9ZzxxesHEVe+C1wSCKBPFEw0 2026-04-19T09:08:20Z 3075 660 15 http://arxiv.org/abs/2405.04022v1 2024-05-07T05:49:08Z

Let $R$ be a commutative ring and let $n \geq 1.$ We study $Γ(s)$, the generating function and Ann$(s)$, the ideal of characteristic polynomials of $s$, an $n$--dimensional sequence over $R$. We express $f(X_1,\ldots,X_n) \cdot Γ(s)(X_1^{-1},\ldots ,X_n^{-1})$ as a partitioned sum. That is, we give (i) a $2^n$--fold ``border'' partition (ii) an explicit expression for the product as a $2^n$--fold sum; the support of each summand is contained in precisely one member of the partition. A key summand is $β_0(f,s)$, the ``border polynomial'' of $f$ and $s$, which is divisible by $X_1\cdots X_n$. We say that $s$ is {\em eventually rectilinear} if the elimination ideals Ann$(s)\cap R[X_i]$ contain an $f_i(X_i)$ for $1 \leq i \leq n$. In this case, we show that $\mbox{Ann}(s)$ is the ideal quotient $(\sum_{i=1}^n(f_i)\ :\ β_0(f,s)/(X_1\cdots X_n)).$ When $R$ and $R[[X_1,X_2, \ldots ,X_n]]$ are factorial domains (e.g. $R$ a principal ideal domain or ${\Bbb F}[X_1,\ldots,X_n]$), we compute {\em the monic generator} $γ_i$ of $\mbox{Ann}(s) \cap R[X_i]$ from known $f_i \in \mbox{Ann}(s) \cap R[X_i]$ or from a finite number of $1$--dimensional linear recurring sequences over $R$. Over a field ${\Bbb F}$ this gives an $O(\prod_{i=1}^n δγ_i^3)$ algorithm to compute an ${\Bbb F}$--basis for $\mbox{Ann}(s)$.

2024-05-07T05:49:08Z This is my original latex document submitted to Journal of Symbolic Computation without the typographical errors which were introduced: 'The Journal apologizes for the typographical errors in Norton (1995) introduced in the subediting process'; see this journal, (1995)20, 769-770 J. Symbolic Computation (1995), 20, 71-92 Graham H. Norton http://arxiv.org/abs/2211.06818v4 2024-05-07T00:00:08Z

This paper presents a new compressed representation of Boolean functions, called CFLOBDDs (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-compatible alternative to BDDs (Binary Decision Diagrams), and hence useful for representing certain classes of functions, matrices, graphs, relations, etc. in a highly compressed fashion. CFLOBDDs share many of the good properties of BDDs, but--in the best case--the CFLOBDD for a Boolean function can be exponentially smaller than any BDD for that function. Compared with the size of the decision tree for a function, a CFLOBDD--again, in the best case--can give a double-exponential reduction in size. They have the potential to permit applications to (i) execute much faster, and (ii) handle much larger problem instances than has been possible heretofore. CFLOBDDs are a new kind of decision diagram that go beyond BDDs (and their many relatives). The key insight is a new way to reuse sub-decision-diagrams: components of CFLOBDDs are structured hierarchically, so that sub-decision-diagrams can be treated as standalone ''procedures'' and reused. We applied CFLOBDDs to the problem of simulating quantum circuits, and found that for several standard problems the improvement in scalability--compared to simulation using BDDs--is quite dramatic. In particular, the number of qubits that could be handled using CFLOBDDs was larger, compared to BDDs, by a factor of 128x for GHZ; 1,024x for BV; 8,192x for DJ; and 128x for Grover's algorithm. (With a 15-minute timeout, the number of qubits that CFLOBDDs can handle are 65,536 for GHZ, 524,288 for BV; 4,194,304 for DJ; and 4,096 for Grover's Algorithm.)

2022-11-13T04:57:29Z 144 pages TOPLAS 2024 Meghana Sistla Swarat Chaudhuri Thomas Reps 10.1145/3651157 http://arxiv.org/abs/2405.03588v1 2024-05-06T15:59:46Z

We provide tools to help automate the error analysis of algorithms that evaluate simple functions over the floating-point numbers. The aim is to obtain tight relative error bounds for these algorithms, expressed as a function of the unit round-off. Due to the discrete nature of the set of floating-point numbers, the largest errors are often intrinsically "arithmetic" in the sense that their appearance may depend on specific bit patterns in the binary representations of intermediate variables, which may be present only for some precisions. We focus on generic (i.e., parameterized by the precision) and analytic over-estimations that still capture the correlations between the errors made at each step of the algorithms. Using methods from computer algebra, which we adapt to the particular structure of the polynomial systems that encode the errors, we obtain bounds with a linear term in the unit round-off that is sharp in manycases. An explicit quadratic bound is given, rather than the $O()$-estimate that is more common in this area. This is particularly important when using low precision formats, which are increasingly common in modern processors. Using this approach, we compare five algorithms for computing the hypotenuse function, ranging from elementary to quite challenging.

2024-05-06T15:59:46Z Jean-Michel Muller Bruno Salvy http://arxiv.org/abs/2403.02160v2 2024-05-02T16:41:59Z

Let $M$ be an $n\times n$ matrix of homogeneous linear forms over a field $\Bbbk$. If the ideal $\mathcal{I}_{n-2}(M)$ generated by minors of size $n-1$ is Cohen-Macaulay, then the Gulliksen-Negård complex is a free resolution of $\mathcal{I}_{n-2}(M)$. It has recently been shown that by taking into account the syzygy modules for $\mathcal{I}_{n-2}(M)$ which can be obtained from this complex, one can derive a refined signature-based Gröbner basis algorithm DetGB which avoids reductions to zero when computing a grevlex Gröbner basis for $\mathcal{I}_{n-2}(M)$. In this paper, we establish sharp complexity bounds on DetGB. To accomplish this, we prove several results on the sizes of reduced grevlex Gröbner bases of reverse lexicographic ideals, thanks to which we obtain two main complexity results which rely on conjectures similar to that of Fröberg. The first one states that, in the zero-dimensional case, the size of the reduced grevlex Gröbner basis of $\mathcal{I}_{n-2}(M)$ is bounded from below by $n^{6}$ asymptotically. The second, also in the zero-dimensional case, states that the complexity of DetGB is bounded from above by $n^{2ω+3}$ asymptotically, where $2\leω\le 3$ is any complexity exponent for matrix multiplication over $\Bbbk$.

2024-03-04T16:08:33Z 26 pages, 2 algorithms; updated remarks after Theorem 6.5 Sriram Gopalakrishnan http://arxiv.org/abs/2403.14844v2 2024-05-01T19:04:28Z

PHCpack is a software package for polynomial homotopy continuation, which provides a robust path tracker [Telen, Van Barel, Verschelde, SISC 2020]. This tracker computes the radius of convergence of Newton's method, estimates the distance to the nearest path, and then applies Padé approximants to predict the next point on the path. A priori step size control is less sensitive to finely tuned tolerances than a posteriori step size control, and is therefore robust. The Python interface phcpy is extended with a new step-by-step tracker and is applied to experiment with extrapolation methods to accurately locate the singular points at the end of solution paths.

2024-03-21T21:28:47Z Accepted by the 8th International Congress on Mathematical Software 2024 Jan Verschelde Kylash Viswanathan http://arxiv.org/abs/2308.09474v3 2024-04-29T13:46:56Z

The discovery of scientific formulae that parsimoniously explain natural phenomena and align with existing background theory is a key goal in science. Historically, scientists have derived natural laws by manipulating equations based on existing knowledge, forming new equations, and verifying them experimentally. In recent years, data-driven scientific discovery has emerged as a viable competitor in settings with large amounts of experimental data. Unfortunately, data-driven methods often fail to discover valid laws when data is noisy or scarce. Accordingly, recent works combine regression and reasoning to eliminate formulae inconsistent with background theory. However, the problem of searching over the space of formulae consistent with background theory to find one that best fits the data is not well-solved. We propose a solution to this problem when all axioms and scientific laws are expressible via polynomial equalities and inequalities and argue that our approach is widely applicable. We model notions of minimal complexity using binary variables and logical constraints, solve polynomial optimization problems via mixed-integer linear or semidefinite optimization, and prove the validity of our scientific discoveries in a principled manner using Positivstellensatz certificates. The optimization techniques leveraged in this paper allow our approach to run in polynomial time with fully correct background theory under an assumption that the complexity of our derivation is bounded), or non-deterministic polynomial (NP) time with partially correct background theory. We demonstrate that some famous scientific laws, including Kepler's Third Law of Planetary Motion, the Hagen-Poiseuille Equation, and the Radiated Gravitational Wave Power equation, can be derived in a principled manner from axioms and experimental data.

2023-08-18T11:19:41Z Revised version, including a significant number of new experiments+supplementary material in appendix, and a title change Nature Communications 15:5922, 2024 Ryan Cory-Wright Cristina Cornelio Sanjeeb Dash Bachir El Khadir Lior Horesh 10.1038/s41467-024-50074-w http://arxiv.org/abs/2404.18117v1 2024-04-28T08:54:57Z

This paper tackles the problem of constructing Bezout matrices for Newton polynomials in a basis-preserving approach that operates directly with the given Newton basis, thus avoiding the need for transformation from Newton basis to monomial basis. This approach significantly reduces the computational cost and also mitigates numerical instability caused by basis transformation. For this purpose, we investigate the internal structure of Bezout matrices in Newton basis and design a basis-preserving algorithm that generates the Bezout matrix in the specified basis used to formulate the input polynomials. Furthermore, we show an application of the proposed algorithm on constructing confederate resultant matrices for Newton polynomials. Experimental results demonstrate that the proposed methods perform superior to the basis-transformation-based ones.

2024-04-28T08:54:57Z Jing Yang Wei Yang http://arxiv.org/abs/2404.17508v1 2024-04-26T16:20:04Z

We present a new methodology for utilising machine learning technology in symbolic computation research. We explain how a well known human-designed heuristic to make the choice of variable ordering in cylindrical algebraic decomposition may be represented as a constrained neural network. This allows us to then use machine learning methods to further optimise the heuristic, leading to new networks of similar size, representing new heuristics of similar complexity as the original human-designed one. We present this as a form of ante-hoc explainability for use in computer algebra development.

2024-04-26T16:20:04Z Accepted for presentation at ICMS 2024 Dorian Florescu Matthew England http://arxiv.org/abs/2404.16361v1 2024-04-25T06:42:32Z

This study proposes Evolutionary Causal Discovery (ECD) for causal discovery that tailors response variables, predictor variables, and corresponding operators to research datasets. Utilizing genetic programming for variable relationship parsing, the method proceeds with the Relative Impact Stratification (RIS) algorithm to assess the relative impact of predictor variables on the response variable, facilitating expression simplification and enhancing the interpretability of variable relationships. ECD proposes an expression tree to visualize the RIS results, offering a differentiated depiction of unknown causal relationships compared to conventional causal discovery. The ECD method represents an evolution and augmentation of existing causal discovery methods, providing an interpretable approach for analyzing variable relationships in complex systems, particularly in healthcare settings with Electronic Health Record (EHR) data. Experiments on both synthetic and real-world EHR datasets demonstrate the efficacy of ECD in uncovering patterns and mechanisms among variables, maintaining high accuracy and stability across different noise levels. On the real-world EHR dataset, ECD reveals the intricate relationships between the response variable and other predictive variables, aligning with the results of structural equation modeling and shapley additive explanations analyses.

2024-04-25T06:42:32Z Ou Deng Shoji Nishimura Atsushi Ogihara Qun Jin http://arxiv.org/abs/2404.14973v1 2024-04-23T12:27:20Z

Computer Algebra Systems (e.g. Maple) are used in research, education, and industrial settings. One of their key functionalities is symbolic integration, where there are many sub-algorithms to choose from that can affect the form of the output integral, and the runtime. Choosing the right sub-algorithm for a given problem is challenging: we hypothesise that Machine Learning can guide this sub-algorithm choice. A key consideration of our methodology is how to represent the mathematics to the ML model: we hypothesise that a representation which encodes the tree structure of mathematical expressions would be well suited. We trained both an LSTM and a TreeLSTM model for sub-algorithm prediction and compared them to Maple's existing approach. Our TreeLSTM performs much better than the LSTM, highlighting the benefit of using an informed representation of mathematical expressions. It is able to produce better outputs than Maple's current state-of-the-art meta-algorithm, giving a strong basis for further research.

2024-04-23T12:27:20Z Rashid Barket Matthew England Jürgen Gerhard http://arxiv.org/abs/2404.13672v1 2024-04-21T14:22:53Z

This volume contains * The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems. * The post-proceedings of the Tenth Workshop on Horn clauses for Verification and Synthesis (HCVS 2023). The meeting was held on April 23, 2023 at the Institut Henri Poincaré in Paris. HCVS aims to bring together researchers working in the two communities of constraint/ logic programming (e.g., ICLP and CP), program verification (e.g., CAV, TACAS, and VMCAI), and automated deduction (e.g., CADE, IJCAR), on the topics of Horn clause based analysis, verification, and synthesis.

2024-04-21T14:22:53Z EPTCS 402, 2024 Temur Kutsia RISC, Johannes Kepler University Linz Daniel Ventura INF, Universidade Federal de Goiás David Monniaux CNRS - Verimag José F. Morales IMDEA 10.4204/EPTCS.402 http://arxiv.org/abs/2401.00256v2 2024-04-19T15:18:24Z

We introduce hypergeometric-type sequences. They are linear combinations of interlaced hypergeometric sequences (of arbitrary interlacements). We prove that they form a subring of the ring of holonomic sequences. An interesting family of sequences in this class are those defined by trigonometric functions with linear arguments in the index and $π$, such as Chebyshev polynomials, $\left(\sin^2\left(n\,π/4\right)\cdot\cos\left(n\,π/6\right)\right)_n$, and compositions like $\left(\sin\left(\cos(nπ/3)π\right)\right)_n$. We describe an algorithm that computes a hypergeometric-type normal form of a given holonomic $n\text{th}$ term whenever it exists. Our implementation enables us to generate several identities for terms defined via trigonometric functions.

2023-12-30T15:00:54Z 23 pages. To appear in the Journal of Symbolic Computation Bertrand Teguia Tabuguia http://arxiv.org/abs/2309.08002v2 2024-04-17T00:39:42Z

Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations.

2023-09-14T19:24:57Z in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2024 Aruna Jayasena Prabhat Mishra 10.1109/TCAD.2024.3383961 http://arxiv.org/abs/2404.10906v1 2024-04-16T20:53:17Z

Embracing the pursuit of intrinsically explainable reinforcement learning raises crucial questions: what distinguishes explainability from interpretability? Should explainable and interpretable agents be developed outside of domains where transparency is imperative? What advantages do interpretable policies offer over neural networks? How can we rigorously define and measure interpretability in policies, without user studies? What reinforcement learning paradigms,are the most suited to develop interpretable agents? Can Markov Decision Processes integrate interpretable state representations? In addition to motivate an Interpretable RL community centered around the aforementioned questions, we propose the first venue dedicated to Interpretable RL: the InterpPol Workshop.

2024-04-16T20:53:17Z Hector Kohler Quentin Delfosse Paul Festor Philippe Preux http://arxiv.org/abs/2404.10482v1 2024-04-16T11:42:19Z

We propose an effective method for primary decomposition of symmetric ideals. Let $K[X]=K[x_1,\ldots,x_n]$ be the $n$-valuables polynomial ring over a field $K$ and $\mathfrak{S}_n$ the symmetric group of order $n$. We consider the canonical action of $\mathfrak{S}_n$ on $K[X]$ i.e. $σ(f(x_1,\ldots,x_n))=f(x_{σ(1)},\ldots,x_{σ(n)})$ for $σ\in \mathfrak{S}_n$. For an ideal $I$ of $K[X]$, $I$ is called {\em symmetric} if $σ(I)=I$ for any $σ\in \mathfrak{S}_n$. For a minimal primary decomposition $I=Q_1\cap \cdots \cap Q_r$ of a symmetric ideal $I$, $σ(I)=σ(Q_1)\cap \cdots \cap σ(Q_r)$ is a minimal primary decomposition of $I$ for any $σ\in \mathfrak{S}_n$. We utilize this property to compute a full primary decomposition of $I$ efficiently from partial primary components. We investigate the effectiveness of our algorithm by implementing it in the computer algebra system Risa/Asir.

2024-04-16T11:42:19Z Yuki Ishihara