End-to-End Verification for Subgraph Solving
Authors: Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our experimental evaluation shows that end-to-end formal verification is now feasible for a wide range of hard graph problems. Experiments To validate our approach, we performed experiments on a cluster of machines with dual AMD EPYC 7643 processors, 2TBytes RAM, and a RAID array of solid state drives, running Ubuntu 22.04. We ran up to 40 jobs in parallel, and limited each individual process to 64GBytes RAM. |
| Researcher Affiliation | Academia | Stephan Gocht1,2, Ciaran Mc Creesh3, Magnus O. Myreen4, Jakob Nordstr om2,1, Andy Oertel1,2, Yong Kiam Tan5 1Lund University, Lund, Sweden 2University of Copenhagen, Copenhagen, Denmark 3University of Glasgow, Glasgow, Scotland 4Chalmers University of Technology, Gothenburg, Sweden 5Institute for Infocomm Research (I2R), A*STAR, Singapore |
| Pseudocode | Yes | Where applicable, formal code snippets are pretty-printed for illustration, e.g., as shown in Figure 2. |
| Open Source Code | Yes | All code is available in the supplementary material (Gocht et al. 2023). |
| Open Datasets | Yes | For maximum clique, we took the 54 instances from the Second DIMACS Implementation Challenge (Johnson and Trick 1996) that Gocht et al. were able to check. For subgraph isomorphism, we used the same subset of 1,226 small-to-medium-sized instances from the benchmark set in (Kotthoff, Mc Creesh, and Solnon 2016) as was studied by Gocht, Mc Creesh, and Nordstr om (2020). |
| Dataset Splits | No | The paper uses standard benchmark sets but does not specify the explicit training, validation, and test dataset splits or methodologies used for data partitioning. |
| Hardware Specification | Yes | Experiments To validate our approach, we performed experiments on a cluster of machines with dual AMD EPYC 7643 processors, 2TBytes RAM, and a RAID array of solid state drives, running Ubuntu 22.04. |
| Software Dependencies | No | The paper mentions the 'CAKEML ecosystem' and 'HOL4 proof assistant' and the operating system 'Ubuntu 22.04', but does not provide specific version numbers for these or other software dependencies. |
| Experiment Setup | Yes | We ran up to 40 jobs in parallel, and limited each individual process to 64GBytes RAM. |