Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2605.10841

Constant time testability of first-order logic with modulo counting on finitary graphs

Isolde Adler·Jenny Stimpson
View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper studies algorithmic meta theorems for property testing with \emph{constant running time} in the bounded degree model. In (Adler, Harwath 2018) it was shown that on graph classes $\mathcal C^{w}_d$ consisting of all graphs with both degree at most $d$ and treewidth at most $w$, every problem expressible in monadic second-order logic with counting (CMSO) is testable with \emph{polylogarithmic} running time (where $d,w\in \mathbb N$ are fixed). It was left open whether this can be improved to \emph{constant} running time. In this paper we give a positive answer for testing CMSO on classes $\mathcal C^{c}_d$, where $d$ bounds the degree and $c$ bounds the component size. Our main result shows constant time testability of first-order logic with modulo counting (FOMOD) on $\mathcal C^{c}_d$. For our proof we tailor Hanf normal form of FOMOD to our setting, and we exhibit a number-theoretic `patchability' condition that allows to infer global information on the input graph from a local sample of constant size. We believe that our `patchability' might be of independent interest. The step from FOMOD to CMSO then follows from a result by (Eickmeyer, Elberfeld, Harwath, 2017) on the expressive power of order invariant monadic second-order logic on classes of bounded treedepth.

Explore related subjects

cs.LOmath.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Isolde Adler, Jenny Stimpson. 2026-05-11. Constant time testability of first-order logic with modulo counting on finitary graphs. https://arxiv.org/abs/2605.10841

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

KEEP EXPLORING

Related papers

arXiv2026

Verifying Numerical Methods with Isabelle/HOL

Modern machine learning pipelines and ODE solvers are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. We evaluate a framework designed for verifying imperative programs and the Isabelle proof assistant as tools for proving the total correctness of four numerical algorithms: the bisection method, the fixed-point method, the perceptron, and the gradient descent algorithm. Our verifications required subtle extensions and generalisations to Isabelle's version of Taylor's theorem and higher-order derivatives. Finally, we reflect on the framework's automation, friendly syntax, and on further requirements to turn it into a verification tool for numerical methods.

cs.LO↗
arXiv2026

Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications

Finite model finders cannot witness an Austin law: an identity whose finite models are all trivial but which has a nontrivial infinite model. We introduce rank-decreasing sparse trace-tree magmas, finitely presented total operations on a countably infinite constructor-tree carrier. The default product pairs its arguments; finitely many positive Horn clauses define exceptions. Our main procedure derives clauses from symbolic evaluation traces. For every model found, it proves functionality of the exceptional relation by descent on constructor size, proves the identity by exhaustive symbolic case analysis, and emits a self-contained Lean 4 certificate. A least simultaneous fixed point gives an implementation-independent semantics, so bounded search may miss models but cannot invalidate certified results. On ETP's 96 order-five Austin candidates, we discover and Lean-verify infinite countermodels for 28 identities with no prior public classification in our audit. They form 14 duality classes and establish 28 new Austin classifications. Four ALPS-known cases bring the total to 32 certified candidates. On Canonical-4187, the deduplicated union of Order5-130 and the 4,141-row ALPS pool, a fresh trace run produces 636 certificates, all accepted by Judge v3. At equal resource limits, Vampire 5.0.1, E 3.5.1, and complete Twee 2.6.1 jointly prove implications in 94 canonical classes. Only Twee returns trusted counter-satisfiable outcomes, for 18 classes; independent finite-side certificates force 16 to be infinite. None of these ATPs emits an explicit model or Lean certificate, and none decides the 28 new classifications. To the best of our audit, this is the first automated system to synthesize this trace-tree model family, generate well-founded inversion proofs, and emit self-contained Lean 4 certificates.

cs.LO↗
arXiv2026

Don't Blame the Model, Verify the Data: An Evaluation of SMT-based Dataset Verification (Extended Version)

The EU AI Act mandates that datasets for high-risk machine learning (ML) systems meet strict quality criteria such as soundness and bias mitigation. While Satisfiability Modulo Theory (SMT) solving offers a formal approach to verifying these properties, its scalability in realistic ML settings remains unexplored. To bridge this gap, this work presents the first large-scale empirical study of SMT-based dataset verification on two real-world ML datasets. We systematically evaluate how solver performance is shaped by three key dimensions: the type of data-quality property, the specification style, and the dataset encoding strategy. Our findings demonstrate that SMT-based verification is feasible for practical scenarios, but each dimension shapes it: the property type sets the tractability limit, the specification style drives scalability (exceeding $2{,}000{\times}$ for aggregate properties), and the encoding strategy has a systematic effect, with extracted feature columns performing best.

cs.LO↗