End-to-End Verification for Subgraph Solving
Gocht, Stephan LU ; McCreesh, Ciaran ; Myreen, Magnus O. ; Nordström, Jakob LU ; Oertel, Andy LU
and Tan, Yong Kiam
(2024)
38th AAAI Conference on Artificial Intelligence, AAAI 2024
In Proceedings of the AAAI Conference on Artificial Intelligence
38.
p.8038-8047
- Abstract
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... (More)
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.
(Less)
- author
- Gocht, Stephan
LU
; McCreesh, Ciaran
; Myreen, Magnus O.
; Nordström, Jakob
LU
; Oertel, Andy
LU
and Tan, Yong Kiam
- organization
- publishing date
- 2024-03-25
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- End-to-End Verification for Subgraph Solving
- series title
- Proceedings of the AAAI Conference on Artificial Intelligence
- volume
- 38
- edition
- 8
- pages
- 10 pages
- conference name
- 38th AAAI Conference on Artificial Intelligence, AAAI 2024
- conference location
- Vancouver, Canada
- conference dates
- 2024-02-20 - 2024-02-27
- external identifiers
-
- scopus:85189616389
- ISSN
- 2159-5399
- DOI
- 10.1609/aaai.v38i8.28642
- language
- English
- LU publication?
- yes
- id
- 4c0d5226-758f-4e9c-804d-13d5c525ed39
- date added to LUP
- 2024-04-26 14:40:57
- date last changed
- 2024-04-26 14:41:16
@inproceedings{4c0d5226-758f-4e9c-804d-13d5c525ed39,
abstract = {{<p>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.</p>}},
author = {{Gocht, Stephan and McCreesh, Ciaran and Myreen, Magnus O. and Nordström, Jakob and Oertel, Andy and Tan, Yong Kiam}},
booktitle = {{End-to-End Verification for Subgraph Solving}},
issn = {{2159-5399}},
language = {{eng}},
month = {{03}},
pages = {{8038--8047}},
series = {{Proceedings of the AAAI Conference on Artificial Intelligence}},
title = {{End-to-End Verification for Subgraph Solving}},
url = {{http://dx.doi.org/10.1609/aaai.v38i8.28642}},
doi = {{10.1609/aaai.v38i8.28642}},
volume = {{38}},
year = {{2024}},
}