Document Open Access Logo

Decidability of Graph Neural Networks via Logical Characterizations

Authors Michael Benedikt , Chia-Hsuan Lu , Boris Motik , Tony Tan

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2024.127.pdf
  • Filesize: 0.77 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Logic
  • Graph Neural Networks

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.

Cite As Get BibTex

Michael Benedikt, Chia-Hsuan Lu, Boris Motik, and Tony Tan. Decidability of Graph Neural Networks via Logical Characterizations. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 127:1-127:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ICALP.2024.127

Author Details

Michael Benedikt
  • University of Oxford, UK
Chia-Hsuan Lu
  • University of Oxford, UK
Boris Motik
  • University of Oxford, UK
Tony Tan
  • University of Liverpool, UK

Funding

  • Benedikt, Michael: This research was funded by EPSRC grant EP/T022124/1.

References

  1. Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan L. Reutter, and Juan Pablo Silva. The Logical Expressiveness of Graph Neural Networks. In ICLR, 2020. Google Scholar
  2. Pablo Barceló, Alexander Kozachinskiy, Anthony Wijdada Lin, and Vladamir Podolskii. Logical languages accepted by transformer encoders with hard attention. In ICLR, 2024. Google Scholar
  3. Bartosz Bednarczyk, Maja Orlowska, Anna Pacanowska, and Tony Tan. On classical decidable logics extended with percentage quantifiers and arithmetics. In FSTTCS, 2021. Google Scholar
  4. David Chiang, Peter Cholak, and Anand Pillay. Tighter bounds on the expressivity of transformer encoders. In ICML, 2023. Google Scholar
  5. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In ICALP, 2016. Google Scholar
  6. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific J. Math., 16(2):285-296, 1966. Google Scholar
  7. Valentin Goranko and Martin Otto. Model theory of modal logic. In Blackburn, van Benthem, and Wolter, editors, Handbook of Modal Logic. North-Holland, 2007. Google Scholar
  8. Martin Grohe. The logic of graph neural networks. In LICS, 2021. Google Scholar
  9. Martin Grohe. The descriptive complexity of graph neural networks. In LICS, 2023. Google Scholar
  10. C. Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. LICS, 2019. Google Scholar
  11. Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. In CADE, 2005. Google Scholar
  12. Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6(3):467-480, 1977. Google Scholar
  13. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. Google Scholar
  14. Marco Sälzer and Martin Lange. Fundamental limits in formal verification of message-passing neural networks. In ICLR, 2023. Google Scholar
  15. Manfred Schmidt-Schaubß and Gert Smolka. Attributive concept descriptions with complements. Artif. Intell., 48(1):1-26, 1991. Google Scholar
  16. Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How Powerful are Graph Neural Networks. In ICLR, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact