GPU-Accelerated Search and Certification of Bounded Indistinguishability in Finite Kripke Semantics

This paper turns finite Kripke semantics into a brute-force search problem that can be accelerated and independently certified. The authors encode sets of worlds as integer bitmasks, so modal operators collapse to fast word-level operations, then fuse that logic into a CUDA kernel for exhaustive scans of small frames.

The headline number is substantial: across K, T, S4, and S5, they evaluated 5,624 formulas on all frames up to five worlds, reaching 1.63×10^14 formula evaluations in 45 minutes on a single H100. They also emitted 20,990 countermodel certificates, and every one of them verified. For engine and tools folks, the notable pattern is not just GPU throughput, but the pairing of high-volume search with a separate checker that makes the results auditable.

They also report a bounded result that is easy to miss: in this corpus, every K-refutable formula had a countermodel on at most two worlds, far below the usual filtration bound of 2^{|Sub(φ)|}. That suggests a lot of practical refutation work may be much smaller than worst-case theory implies, at least for the explored space.

Beyond refutation, the paper treats pairwise equivalence as a minimal-countermodel problem and synthesizes “semantic mirages” that agree on all models up to a finite size and only diverge later. The authors also build a density-aggregated semantic atlas and compare retrieval layouts such as PCA, UMAP, spectral, and random under a million-pair verifier budget. The broader takeaway is a reproducible pipeline for GPU enumeration, certificate checking, and visual exploration of semantic...