End-to-End Verification for Subgraph Solving
Research output: Contribution to journal › Conference article › Research › peer-review
Documents
- Fulltext
Final published version, 317 KB, PDF document
Modern subgraph-finding algorithm implementations consist of thousands of lines of highly optimized code, and this complexity raises questions about their trustworthiness. Recently, some state-of-the-art subgraph solvers have been enhanced to output machine-verifiable proofs that their results are correct. While this significantly improves reliability, it is not a fully satisfactory solution, since end-users have to trust both the proof checking algorithms and the translation of the high-level graph problem into a low-level 0-1 integer linear program (ILP) used for the proofs. In this work, we present the first formally verified toolchain capable of full end-to-end verification for subgraph solving, which closes both of these trust gaps. We have built encoder frontends for various graph problems together with a 0-1 ILP (a.k.a. pseudo-Boolean) proof checker, all implemented and formally verified in the CAKEML ecosystem. This toolchain is flexible and extensible, and we use it to build verified proof checkers for both decision and optimization graph problems, namely, subgraph isomorphism, maximum clique, and maximum common (connected) induced subgraph. Our experimental evaluation shows that end-to-end formal verification is now feasible for a wide range of hard graph problems.
Original language | English |
---|---|
Journal | Proceedings of the AAAI Conference on Artificial Intelligence |
Volume | 38 |
Issue number | 8 |
Pages (from-to) | 8038-8047 |
Number of pages | 10 |
ISSN | 2159-5399 |
DOIs | |
Publication status | Published - 2024 |
Event | 38th AAAI Conference on Artificial Intelligence, AAAI 2024 - Vancouver, Canada Duration: 20 Feb 2024 → 27 Feb 2024 |
Conference
Conference | 38th AAAI Conference on Artificial Intelligence, AAAI 2024 |
---|---|
Country | Canada |
City | Vancouver |
Period | 20/02/2024 → 27/02/2024 |
Sponsor | Association for the Advancement of Artificial Intelligence |
Bibliographical note
Publisher Copyright:
Copyright © 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
ID: 390581269