Search papers, labs, and topics across Lattice.
This paper introduces CertiFOX, a novel certifying grounding framework that ensures the equivalence between high-level specifications and low-level inputs in first-order logic model expansion over finite domains. By developing a new normal form called Grounding Normal Form (GNF) and incorporating a proof format for grounding derivations alongside an independent proof checker, the authors address the critical trust gap in declarative solving. Experimental results demonstrate that CertiFOX maintains competitive performance with existing grounders while providing essential certification, paving the way for reliable certified solving pipelines in declarative languages.
Trustworthy AI solutions are now possible with CertiFOX, which certifies that grounding outputs match their high-level specifications.
Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)--a new normal form designed for compact, domain-aware grounding--and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is broadly comparable with other grounders, and proof checking with CheckFOX adds overhead within a small constant factor of grounding time.
