Lecture Notes on Verifying Graph Neural Networks
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909842185125888 |
|---|---|
| author | Schwarzentruber, François |
| author_facet | Schwarzentruber, François |
| contents | In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_11617 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Lecture Notes on Verifying Graph Neural Networks Schwarzentruber, François Logic in Computer Science Machine Learning In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic. |
| title | Lecture Notes on Verifying Graph Neural Networks |
| topic | Logic in Computer Science Machine Learning |
| url | https://arxiv.org/abs/2510.11617 |