Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.28928

An algorithmic construction of Nullstellensatz certificates for graph automorphism groups

Ivan Drecun
View original source ↗Read source document ↗Export metadata ↓

Abstract

Solvers for graph isomorphism and related problems are widely used in both theoretical and applied domains, but their complexity often requires users to trust their correctness without verification. We present a certifying algorithm for computing a generating set of the automorphism group of a given graph, meaning that it produces an independently verifiable certificate that the output list of automorphisms generates the entirety of the automorphism group. The problem of constructing a certificate is reduced to certifying that a system of multivariate polynomial equations is infeasible. An individualization-refinement algorithm produces a derivation within an algebraic proof system, representing a Nullstellensatz certificate of infeasibility. We provide an implementation of both the certifying algorithm and a certificate verifier, and demonstrate their viability on graphs with hundreds of vertices.

Explore related subjects

cs.SCcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Ivan Drecun. 2026-10-20. An algorithmic construction of Nullstellensatz certificates for graph automorphism groups. https://arxiv.org/abs/2610.28928

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Indefinite Summation Problem for the Laurent Ring

This article solves the Indefinite Summation Problem (ISP) for the difference ring $(A, α)$, where $A$ is the Laurent ring of shift operators on the lattice $\Z^n$, and $α$ is any ring automorphism of $A$ of finite order. The space of summable elements in $(A, α)$ is infinite dimensional, and it is possible to write down an explicit basis for it. The solution translates to a finite procedure involving a matrix multiplication, where the size of the matrix can be estimated. It follows that the arithmetic complexity of the solution can also be determined. These results extend to a solution of the ISP for the ring of functions on $\Z^n$, on which $α$ acts by duality. The article also points out that the solution to the ISP amounts to calculating the group cohomologies $H^i([α], A), i = 0, 1$, where $[α]$ is the cyclic group generated by $α$.

cs.SC↗
arXiv2026

Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking

GPU kernels are critical to the performance of today's AI services, yet the same operators are rewritten repeatedly: for each GPU generation, numeric format, serving regime, and kernel language. Every rewrite must preserve the function computed by the implementation it replaces. Today, this obligation depends almost entirely on differential testing: run the new kernel and a trusted reference on randomly sampled tensors, then compare their outputs within a tolerance. This approach has blind spots that additional test cases cannot eliminate. For example, a logical bug may produce an error smaller than the tolerance required to accommodate a correct optimized kernel. We propose symbolic equivalence checking, which executes a kernel and its reference on symbolic inputs, turning each output cell into an exact algebraic expression, and then checks whether the paired expressions agree for all inputs. Because these expressions are exact, symbolic equivalence checking distinguishes floating-point error from logical bugs, while a single check covers the entire input space. We implement Racer, a PTX-level symbolic equivalence checking engine, with three techniques that make this approach practical for production kernels: (1) Shape Reduction to control checking cost, (2) a lockstep CTA scheduler to handle concurrency, and (3) idiom templates with exact numeric refutation for otherwise inconclusive results. Across 2,408 production kernels from 41 collection targets, Racer found 82 real bugs in 23 libraries, including 76 previously unknown bugs and 41 confirmed so far.

cs.SC↗
arXiv2026

Sparse Polynomial GCD Cannot Be Computed in Fixed-output Polynomial Time

This paper shows that, assuming $\mathsf{P}\ne\mathsf{NP}$, sparse univariate polynomial GCD cannot be computed in fixed-output polynomial time over any fixed computable field. Precisely, there is no deterministic algorithm that can compute the GCD of sparse univariate polynomials over any fixed computable field with total bit complexity polynomial in the input size, with the output size as a fixed parameter. In particular, there is no deterministic algorithm for sparse polynomial GCD that runs in polynomial time with respect to both the input and the output sizes. This settles the open problem posed as Challenge 5 in the sparsity challenges. Furthermore, we show that the Roots of Unity Detection problem over finite fields is NP-hard under random reductions; that is, determining whether the GCD of a sparse univariate polynomial and $x^n - 1$ has nonzero degree is NP-hard.

cs.SC↗