An algorithmic construction of Nullstellensatz certificates for graph automorphism groups

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.