用带计数的模态逻辑验证图神经网络，解决可满足性问题。
Lecture Notes on Verifying Graph Neural Networks
- 提出含计数模态的线性不等式逻辑，用于验证图神经网络
- 设计算法求解该逻辑的可满足性问题，基于表演法扩展
- 适合研究形式化验证与图神经网络可解释性的学者
这些讲义首先回顾图神经网络与Weisfeiler-Lehman测试、一阶逻辑及分级模态逻辑之间的联系。随后提出一种模态逻辑，其中计数模态以线性不等式形式出现，用于解决图神经网络的验证任务。描述了该逻辑的可满足性问题求解算法，其灵感源于经典模态逻辑的表演法，并扩展至无量词布尔代数与Presburger算术的推理框架。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。