Sage Binder (Jul 12 2025 at 23:55): Sage Binder (Jul 12 2025 at 23:55):Hi,
I am wondering if there is a verified graph isomorphism algorithm on the AFP.
I came across some papers that seem to involve algorithms for isomorphism checking (https://isabelle.in.tum.de/~nipkow/pubs/itp11.pdf, https://pmc.ncbi.nlm.nih.gov/articles/PMC7324030/), but could not find these developments on the AFP.
I am also aware of https://github.com/mabdula/Isabelle-Graph-Library, but did not see an isomorphism algorithm there.
Manuel Eberl (Jul 13 2025 at 16:51):I don't think so. The positive answer is of course very easy to certify, and that's usually the one people care about. So perhaps the incentive to formalise an algorithm for this has not been too big. I don't know how much work you have to do to get significantly better performance than brute-forcing, but competitive GI solvers are quite complex, I think.
@Mohammad Abdulaziz ought to know much more about this.
Mathias Fleury (Jul 13 2025 at 17:30):As far as I know https://github.com/ciaranm/glasgow-subgraph-solver is the most advanced certifying approach
Mathias Fleury (Jul 13 2025 at 17:31):(but not verified… from Ciaran McCreesh's talks it is not easy )
Mohammad Abdulaziz (Jul 13 2025 at 22:36):I am certain there is a calculus for certifying graph isomorphism by Filip Maric. It is formalised and shown to indeed certify Naughty style isomorphism solvers in Isabelle, iirc. I wanted to integrate it with the graph library you pointed to above
Mohammad Abdulaziz (Jul 13 2025 at 22:36):Here is a link:
https://lmcs.episciences.org/10892
Mohammad Abdulaziz (Jul 13 2025 at 22:38):Let me know if that is a topic you want to further explore
irvin (Jul 14 2025 at 04:24):Mathias Fleury said:
As far as I know https://github.com/ciaranm/glasgow-subgraph-solver is the most advanced certifying approach
I think that @Yong Kiam has a verified checker for that in HOL4
Yong Kiam (Jul 14 2025 at 05:28):irvin said:
Mathias Fleury said:
As far as I know https://github.com/ciaranm/glasgow-subgraph-solver is the most advanced certifying approach
I think that Yong Kiam has a verified checker for that in HOL4
we can certify both positive/negative answers generated by the Glasgow subgraph solver.
besides verified algorithms vs certifying algorithms, I think there's also a substantial difference if this thread is meant to be asking about verifying a real GI solver or something more on the theoretical end.
Yong Kiam (Jul 14 2025 at 05:31):(if it is the former on verifying a real GI solver, I agree with @Mathias Fleury's assessment)
edit: actually if it is the latter, I also guess it's not esay :sweat_smile:
Sage Binder (Jul 14 2025 at 19:14):Thank you for the responses!
I was interested in this problem in the context of graph enumeration up to isomorphism. I've seen, for instance, tree enumeration on the AFP, but in that case I believe isomorphic copies were avoided by construction. A little while ago, I was experimenting with enumerating a particular type of graph up to isomorphism, up to around 20 vertices, so I wrote the enumeration algorithm, including an isomorphism checker, in Isabelle (and verified the isomorphism checker part). The isomorphism checker does some hashing to improve performance, but is by no means advanced (and does not check for subgraph isomorphism). As I did not finish verification of the enumeration, nothing is on the AFP yet, but I was considering submitting the verified isomorphism checker by itself. But, I know that GI is a deep problem so I was wondering what other work is out there.
Based on this thread, my understanding is that the main interest is going to be in certifying GI outputs rather than verifying a GI algorithm directly, since the state-of-the-art GI algorithms are very complex.
I wonder how this certificate-based approach would extend to verified graph enumeration, though. The only instance of verified graph enumeration I've seen is the Nipkow paper previously linked (well, there is also the tree enumeration on the AFP, but again I believe that avoids isomorphic copies by construction).
Anyways, perhaps a basic verified isomorphism checker can be useful to other users for experiments in graph enumeration, so I will try and submit that soon.
@Mohammad Abdulaziz Yes, I am certainly interested in exploring verified graph algorithms! (By the way, will you be at ITP this year? I was hoping to have a chance to connect with you then.)
Mohammad Abdulaziz (Jul 16 2025 at 19:30):Yes, I will be there. See you in September!
Last updated: Aug 20 2025 at 20:23 UTC