Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof

TL;DR

This paper presents optimized algorithms and implementation techniques that enable the verification of a large-scale, computer-generated proof for the optimality of sorting networks with 9 inputs, significantly improving scalability and efficiency.

Contribution

It introduces several non-trivial optimizations to a certified proof checker, allowing it to verify the full proof for 9 inputs, which was previously infeasible.

Findings

Orders of magnitude improvements in runtime and memory for 8-input verification

Successful verification of the full proof for 9 inputs

Enhanced formalization and oracle implementation contributed to scalability

Abstract

In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.