Research map / Graph learning / Graph algorithms and clustering
End-to-End Verification for Subgraph Solving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Presents a formally verified (CakeML/HOL4) toolchain with a pseudo-Boolean proof checker and graph encoders that verifies end-to-end the results of subgraph solving (max clique, subgraph isomorphism, MCCIS).
Problem
Proof-logged subgraph solvers still require trusting the proof checker and the translation of graph problems into 0-1 ILP encodings; end-to-end verification of subgraph solving results is missing.
Approach
Build a formally verified pseudo-Boolean proof checker (CAKEPB) with verified graph encoders (CAKEPBGRAPH) compiled via CakeML to machine code, plus a proof elaborator that converts augmented VeriPB proofs into kernel proofs, so the final conclusion is stated in terms of the original graph problem.
Key results
- Verified 50 of 54 max clique instances from DIMACS; kernel proof checking averaged 3.8 times faster than VeriPB checking of augmented proofs.
- Verified 417 satisfiable and 784 unsatisfiable subgraph isomorphism instances out of 1,226.
- Verified all 690 MCCIS instances with up to 20 vertices per graph; kernel proofs verified about 9% slower than VeriPB on augmented proofs.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use CAKEPBGRAPH to formally verify maximum-clique solver proofs | Glasgow Subgraph Solver · DIMACS maximum clique (54 instances) | instances formally verified: 50 of 54 | Helped |
| Check elaborated kernel proofs with CAKEPB instead of checking augmented proofs with VERIPB | Maximum clique proof checking · DIMACS maximum clique | checking time: 3.8 times lower | Helped |
| Elaborate augmented proofs into kernel proofs | Maximum clique proof checking · DIMACS maximum clique | proof size: 2.26 times as large | Hurt |
| Use CAKEPBGRAPH to formally verify subgraph-isomorphism solver proofs | Glasgow Subgraph Solver · Subgraph isomorphism | instances formally verified: 417 satisfiable and 784 unsatisfiable instances | Helped |
| Check kernel proofs with CAKEPB instead of checking augmented proofs with VERIPB | Subgraph-isomorphism proof checking · Subgraph isomorphism | checking time: 2.4 times slower | Hurt |
| Elaborate augmented proofs into kernel proofs | Subgraph-isomorphism proof checking · Subgraph isomorphism | proof size: 10.5 times larger | Hurt |
| Use CAKEPBGRAPH to formally verify maximum common connected induced-subgraph solver proofs | Glasgow Subgraph Solver · Maximum common connected induced subgraph (up to 20 vertices per graph) | instances formally verified: all 690 instances | Helped |
| Check kernel proofs with CAKEPB instead of checking augmented proofs with VERIPB | Maximum common connected induced-subgraph proof checking · Maximum common connected induced subgraph | checking time: 9% longer | Hurt |
| Elaborate augmented proofs into kernel proofs | Maximum common connected induced-subgraph proof checking · Maximum common connected induced subgraph | proof size: 14.7 times larger | Hurt |
Surprising findings
- Kernel proofs were on average 2.26 to 14.7 times larger than augmented proofs, depending on problem family.
- Checking kernel proofs was slower than checking augmented proofs for subgraph isomorphism (2.4 times slower on average).
Limitations
- Some instances failed due to memory limits of the verified checker or excessive kernel proof size.
- Text proof parsing is a substantial portion of elaboration and checking time.
- Proofs are not trimmed, so all solver steps are verified.
Experimental setup
Datasets: Second DIMACS Implementation Challenge clique instances subgraph isomorphism benchmark set (Kotthoff et al. 2016) random MCCIS graph database (Conte et al. 2007; De Santo et al. 2003)
Benchmarks: DIMACS clique instances subgraph isomorphism benchmark (1,226 instances) random MCCIS instances (690 instances)
Metrics: verification time proof size number of instances verified
Baselines: VeriPB
Builds on: VeriPB CakeML HOL4 Glasgow Subgraph Solver cutting planes
Closest papers by meaning
- Between Subgraph Isomorphism and Maximum Common Subgraph (AAAI 2017 · similarity 0.85)
- SAT-Based Algorithms for Regular Graph Pattern Matching (AAAI 2024 · similarity 0.85)
- On the Power of the Weisfeiler-Leman Test for Graph Motif Parameters (ICLR 2024 · similarity 0.84)
- Paths, Proofs, and Perfection: Developing a Human-Interpretable Proof System for Constrained Shortest Paths (AAAI 2024 · similarity 0.84)
- Incremental Topological Ordering and Cycle Detection with Predictions (ICML 2024 · similarity 0.83)
- Functional Matching of Logic Subgraphs: Beyond Structural Isomorphism (NeurIPS 2025 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.