https://arxiv.org/api/8Zk4sefjC2r6dumx1igh9OOa2mw 2026-09-10T20:14:51Z 3239 60 15 http://arxiv.org/abs/2608.01976v1 2026-08-03T09:40:10Z

Given an algebraic statistical model, a challenging problem is classifying the data according to the number of positive critical points of the likelihood function. The positive critical points are the positive solutions to an algebraic system, say likelihood equations. So, identifying the number of positive critical points is a real root classification problem for the likelihood equations. A discriminant variety of a likelihood-equation system geometrically describes the data for which the number of real solutions becomes unusual. As an essential component of the discriminant variety, the nonproperness set collects the data such that the likelihood-equation system has a solution at infinity. So, the number of real solutions varies when the data passes the nonproperness set, and identifying the nonproperness set plays a crucial role in the real root classification. In this work, we develop a novel method for computing nonproperness sets of likelihood-equation systems. We prove the correctness of this method. We show experimentally that it is far more efficient than the known methods in the literature.

2026-08-03T09:40:10Z Xiaoxian Tang Bican Xia Tianqi Zhao http://arxiv.org/abs/2607.22524v2 2026-08-01T20:58:23Z

We formalize in Lean 4 the Kannan-Bachem Smith normal form algorithm for nonsingular square integer matrices. The program returns $S,U,U^{-1},V,V^{-1}$ and proves $UAV=S$, $U^{-1}SV^{-1}=A$, four inverse identities, the Smith divisibility conditions, and equality of $S$ with a canonical reference matrix. Stabilization terminates because each recursive pass strictly decreases the binary size of the active pivot; the outer algorithm recurses on the lower-right block. The computation also emits a flat trace of designated sign-magnitude arithmetic leaves. Branch conditions, quotients, Bezout data, and matrix entries are taken from the recorded primitive runs. Composite phases form their traces by concatenating the charge lists returned by the executed children. Verified self-delimiting codecs define the input and output sizes. Coefficient and work recurrences, closed by a kernel-checked polynomial-envelope calculus, give fixed polynomial bounds for both trace cost and the encoded length of the five output matrices. The theorem concerns these arithmetic primitives; structural operations and compiled Lean runtime are outside the model.

2026-07-24T17:56:21Z 20 pages. Revised and streamlined exposition. Accompanying Lean 4 formalization: https://github.com/JJYYY-JJY/lean-normal-forms Junye Ji University of Washington http://arxiv.org/abs/2608.00668v1 2026-08-01T13:43:15Z

We give a deterministic algorithm for finding all integer roots of a square-free polynomial $f\in\mathbb Z[x]$ of degree $n$ with $\lVert f\rVert_\infty<2^b$. The running time is $$ \tilde{O}(n^{3/2}b), $$ improving the $\tilde{O}(n^2b)$ bound of Harvey and Hittmeir (Research in Number Theory, 2022). The algorithm follows the classical $p$-adic framework: find roots modulo a prime $p$, lift them modulo a high power of $p$, and verify the lifted candidates. The main new idea is to avoid searching for a prime for which $f\bmod p$ is square-free. Instead, we find a prime for which the total multiplicity of repeated roots modulo $p$ is small. This requires lifting repeated roots, which we handle using a weighted lifting tree. We also give a faster deterministic candidate-verification algorithm: given $n$ candidate integers smaller in absolute value than $2^b$, we decide which are roots of $f$ in $$ \tilde{O}(nb+\min(n^2,nb^2)) $$ bit operations. Together, these ingredients give the first deterministic subquadratic-in-$n$ improvement for integer root finding in the square-free case.

2026-08-01T13:43:15Z Itamar Nir http://arxiv.org/abs/2607.06372v3 2026-08-01T03:34:51Z

A standard way to control expression swell in computer algebra is to use multi-modular or evaluation-interpolation methods. In computations involving Gröbner bases, these techniques typically require repeatedly computing Gröbner bases of specializations of the same ideal. These repeated computations can be accelerated through precomputation, notably using Traverso's tracing. We present Groebner$.$jl (https://github.com/sumiya11/Groebner.jl), a Julia implementation of the F4 algorithm that exposes Traverso's tracing through a reusable public interface. The implementation supports SIMD-friendly coefficient types, such as tuples of machine integers, which Julia compiles to efficient code with little manual intervention. This lets other Julia software leverage tracing to obtain speedups in applications such as structural identifiability of ordinary differential equation models and polynomial system solving.

2026-07-07T15:11:07Z In proceedings of ICMS 2026 Alexander Demin http://arxiv.org/abs/2602.10878v3 2026-08-01T03:23:04Z

Consider a subfield of the field of rational functions in several indeterminates. We present an algorithm that, given a set of generators of such a subfield, finds a simple generating set. We provide an implementation of the algorithm and show that it improves upon the state of the art both in efficiency and the quality of the results. Furthermore, we demonstrate the utility of simplified generators through several case studies from different application domains, such as structural parameter identifiability. The main algorithmic novelties include performing only partial Gröbner basis computation via sparse interpolation and efficient search for polynomials of a fixed degree in a subfield of the rational function field.

2026-02-11T14:07:00Z Alexander Demin Gleb Pogudin http://arxiv.org/abs/2607.29308v1 2026-07-31T11:34:02Z

For a system of $s$ homogeneous polynomials of degree $d$ in $n$ variables, say ${\bf{f}} = 0$, we consider the problem of constructing resultant systems. A resultant system is a finite set of polynomials in the coefficients of the input polynomials, the vanishing of which characterizes the systems $\bf{f}$ with a common non-zero solution. The classical approaches for constructing resultant systems rely either on maximal minors of large coefficient matrices or on the coefficients of a resultant of generic linear combinations of the input polynomials. Typically, they produce resultant systems containing a very large number of polynomials. We develop new constructions based on taking resultants of linear combinations of the input polynomials; this results in resultant systems of small cardinality. Our main results are: 1) We prove that a resultant system with ${d+n-1 \choose n-1} s-n^2+1$ polynomials exists; each polynomial is the resultant of $n$ linear combinations of the input polynomials. This improves the previously known upper bounds, even for systems of bivariate homogeneous polynomials. 2) Under the assumption that the input polynomials are non-zero, we construct explicit resultant systems with cardinality $\mathrm{poly}(s,d)$, when $n$ is fixed.

2026-07-31T11:34:02Z M. Levent Doğan Elias Tsigaridas Zafeirakis Zafeirakopoulos http://arxiv.org/abs/2607.29291v1 2026-07-31T11:09:22Z

The matrix-multiplication SAT benchmark of Heule, Kauers, and Seidl asks, among other tasks, for solutions of ten known-satisfiable rank-23 formulas, proofs of unsatisfiability for ten formulas expected to be unsatisfiable, and a rank-23 scheme over $\mathbb{F}_2$ having a summand with no type-3 monomial. We give complete satisfying assignments for the 21 CNFs in the repository's top-level challenge1/, challenge2/, and challenge3/ directories at commit 150b2e2f. The principal finding is that all ten top-level Challenge-2 formulas are satisfiable. A direct audit shows that their hardcoded type-3 pairings are imposed by positive unit clauses on the 621 base variables: the formulas require selected incidences but do not forbid additional type-3 incidences. Starting from exact 23-summand schemes, we use the $\mathrm{GL}(3,2)^3$ isotropy action, cyclic trace symmetry, and perfect matching of transformed summands to constrained slots to construct witnesses for all ten files. For Challenge 3, we combine a locked semantic repair with a two-term identity over $\mathbb{F}_2$ to obtain a distinguished summand of type-3 count zero. Every semantic decomposition has zero residual in all 729 Brent equations. The accompanying DIMACS models assign all 26,541 variables of each formula and satisfy all 2,461,316 clauses across the 21 instances. A separate parser and clause evaluator rechecks the emitted models. A deterministic one-file Python reproducer regenerates the 21 certificates from the original CNFs in approximately nine seconds on the reported test host.

2026-07-31T11:09:22Z Nick Palladinos http://arxiv.org/abs/2607.28897v1 2026-07-30T23:37:20Z

We report on GPU implementations of block-level addition, subtraction, multiplication and division for midsize integers, with operands of $2^{15}$ to $2^{19}$ bits using the high-level functional language Futhark. Comparing with hand-written C++/CUDA versions and CGBN, we identify which functional constructs compile well, where memory placement and sequentialization are effective, and what compiler support is needed. The results show that high-level code can express the algorithms compactly while approaching competitive performance after certain compiler improvements. In particular, we find that automated placement of arrays in GPU register memory is critical for performance.

2026-07-30T23:37:20Z Cosmin E. Oancea Stephen M. Watt http://arxiv.org/abs/2508.20607v2 2026-07-30T17:42:36Z

We refine the bit complexity analysis of an algorithm for the computation of at least one point per connected component of a smooth real algebraic set, yielding exponential speedup (with respect to the number of variables) compared to prior works. The algorithm which is analyzed is based on the critical point method, reducing the problem to computations of critical points associated to the restriction of generic projections on lines to the studied variety. Our refinement, and the subsequent improved complexity statement, comes from a better utilization of the multi-affine structure of polynomial systems encoding these sets of critical points. The bit-size estimates on the size of the output produced by this algorithm are also improved by this refinement.

2025-08-28T09:52:21Z Journal of Symbolic Computation, 2026, 138 Jesse Elliott PolSys Mark Giesbrecht PolSys Edern Gillot PolSys Mohab Safey El Din PolSys Éric Schost http://arxiv.org/abs/2607.28287v1 2026-07-30T14:34:41Z

ARC-AGI-3 turns abstraction into an interactive problem of skill acquisition. A player must infer an unfamiliar game's rules, hidden state, and goal while maintaining action efficiency because every move counts. We formalize these environments as parameterized rendered deterministic Moore machines and introduce Tycho, a coding-agent system that constructs and uses game-specific models during interaction. Tycho separates actionable observations from intermediate animation, level-completion, and game-over frames. From this structured history, an agent can model, test, plan with, repair, or bypass a free-form executable hypothesis. In one matched public-set run per policy, we compare four orchestration policies on all 25 public games using Claude Opus 4.8 under matched inference budgets. Actor-requested delegation to a model builder obtains the highest observed mean Relative Human Action Efficiency (RHAE), 88.49. With this selected policy, GPT-5.6 Sol and Opus 5 both reach 100.00 RHAE and complete all 183 levels. Their game-balanced first-run human-replay midranks are 98.5 and 100.0. Opus 5 uses 61% fewer scored actions than the aggregate official human baselines. Automatic repair after verification failures produces models that reproduce observed transitions much more accurately, yet reaches only 83.07 RHAE. Transition match indicates whether a simulator reproduces observed dynamics, not whether it has identified the objective or improves the next action. Strong play also requires deciding when to construct, repair, use, or bypass a model. We call this joint problem active abstraction: generating a testable model from costly interaction and deciding when acquiring or using it is worth its cost.

2026-07-30T14:34:41Z 52 pages, 18 figures, 17 tables. Open-source implementation: https://github.com/NIMI-research/Tycho Jens Lehmann Andrei Aioanei Sahar Vahdati http://arxiv.org/abs/2607.27003v1 2026-07-29T14:59:38Z

We describe an implementation in Scratchpad II of linear ordinary differential operators over a differential ring, acting on a module equipped with a compatible derivation. The abstract data type facilities of the system allow such operators to be represented and manipulated as first-class objects while retaining the usual notation for operator application. For coefficients in a field, we give constructive algorithms for left and right division, greatest common divisors, least common multiples, and an extended Euclidean algorithm; the right-hand constructions may be obtained from the corresponding left-hand constructions in the opposite ring. We also discuss pseudo-division over polynomial coefficient rings and an Ore localization yielding a right field of fractions. Finally, we apply this operator arithmetic to factorization of ordinary differential equations, using the associated Riccati equation and Newton polygons to analyze possible singular parts of factors. Examples include operators with constant, elementary-function, rational-function, and matrix coefficients.

2026-07-29T14:59:38Z This article is posted for historical archival. It was accepted for presentation and publication in the "Conference on Computers and Mathematics'', held at Stanford, California, 30 July--1 August 1986. The proceedings, however, did not appear. This is a translation of the contemporaneous Script/VM to LaTeX Jean Della Dora Stephen M. Watt http://arxiv.org/abs/2603.18699v3 2026-07-29T10:17:10Z

We propose a more accurate variant of an algorithm for multiplying 4x4 matrices using 48 multiplications over any ring containing an inverse of 2. This algorithm achieves an error bound exponent of only log4($γ$$\infty$,2) $\approx$2.335. In practice, it also reaches a better accuracy w.r.t. max-norm, when compared to previously known such fast algorithms. Furthermore, we propose a straight line program of this algorithm, giving a leading constant in its complexity bound of $316/32 n^{2+log\_4(3)} + o(n^{2+log\_4(3))$ operations over any ring containing an inverse of 2.

2026-03-19T09:58:19Z Jean-Guillaume Dumas CASC Clément Pernet CASC Alexandre Sedoglavic CRIStAL http://arxiv.org/abs/2607.25793v1 2026-07-28T14:43:55Z

Automatic deduction tools such as automatic theorem provers, SAT (satisfiability) solvers, SMT (satisfiability modulo theories) solvers, and termination analyzers can be connected to proof assistants using various approaches, notably by certification and verification. This chapter reviews and compares the approaches available, and mentions several successful applications.

2026-07-28T14:43:55Z This is Chapter 20 of the Book "Proof Assistants and Their Applications in Mathematics and Computer Science" René Thiemann http://arxiv.org/abs/2605.04330v2 2026-07-28T13:38:20Z

We investigate the scaling properties of implicit deductive reasoning over Horn clauses in depth-bounded Transformers. By systematically decorrelating provability from spurious features and enforcing algorithmic alignment, we find that in sufficiently deep models with a bidirectional prefix mask, implicit reasoning approaches explicit CoT performance across graph topologies and problem widths, though CoT remains necessary for depth extrapolation.

2026-05-05T22:35:46Z preprint Enrico Vompa Tanel Tammet http://arxiv.org/abs/2506.13242v7 2026-07-27T09:06:58Z

The quest for non-commutative matrix multiplication algorithms over non-commutative rings in small dimensions has recently seen significant progress. Specifically, the number of scalar multiplications required to multiply two 4x4 matrices was reduced in \cite{Fawzi:2022aa} from 49 (using two recursion levels of Strassen's algorithm) to 47 in characteristic 2, and more recently to 48 in \cite{alphaevolve} over the complex numbers. We propose an algorithm requiring 48 multiplications that uses only rational coefficients, thereby removing the requirement for complex-number arithmetic, and making this algorithm valid over any ring except those of characteristic 2. We also produce a straight-line program of this algorithm reducing the number of additions and scalar multiplications, reaching a running time of $\frac{347}{32}n^{2+\log_4{3}}+o(n^{2+\log_4{3}})$ operations, as well as an alternative basis variant of it, leading to an algorithm running in $7n^{2+\log_4{3}} +o(n^{2+\log_4{3}})$ operations over any ring containing an inverse of 2. Similarly, the number of scalar multiplications required to multiply a 3x4 matrix by a 4x7 matrix was reduced from 66 in \cite{Smirnov:2021aa} to 63 in \cite{alphaevolve} by an algorithm over complex numbers. Using the same techniques, we propose an equivalent algorithm in 63 multiplications using only rational coefficients. In both cases the rational algorithm is obtained by identifying an isotropy that projects the previously known complex-valued decomposition onto the field of rational numbers.

2025-06-16T08:42:15Z Jean-Guillaume Dumas CASC Clément Pernet CASC Alexandre Sedoglavic CRIStAL