End-to-End Verification for Subgraph Solving
Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt
Standard
End-to-End Verification for Subgraph Solving. / Gocht, Stephan; McCreesh, Ciaran; Myreen, Magnus O.; Nordström, Jakob; Oertel, Andy; Tan, Yong Kiam.
I: Proceedings of the AAAI Conference on Artificial Intelligence, Bind 38, Nr. 8, 2024, s. 8038-8047.Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - End-to-End Verification for Subgraph Solving
AU - Gocht, Stephan
AU - McCreesh, Ciaran
AU - Myreen, Magnus O.
AU - Nordström, Jakob
AU - Oertel, Andy
AU - Tan, Yong Kiam
N1 - Publisher Copyright: Copyright © 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
U2 - 10.1609/aaai.v38i8.28642
DO - 10.1609/aaai.v38i8.28642
M3 - Conference article
AN - SCOPUS:85189616389
VL - 38
SP - 8038
EP - 8047
JO - AAAI Conference on Artificial Intelligence
JF - AAAI Conference on Artificial Intelligence
SN - 2159-5399
IS - 8
T2 - 38th AAAI Conference on Artificial Intelligence, AAAI 2024
Y2 - 20 February 2024 through 27 February 2024
ER -
ID: 390581269