Neural networks power critical applications, from autonomous vehicles to medical diagnostics, but their opacity pose significant safety and trust challenges. Formal logical frameworks offer a rigorous path to understand, validate, and trust these models. This workshop aims to bridge the gap between logic and neural network analysis.
We invite contributions that demonstrate how logical frameworks can address core challenges in neural‑network analysis. Topics of interest include the expressivity of logical formalisms for neural networks, the formal verification of safety‑critical properties, the development of interpretation mechanisms grounded in logic, and the assessment of the computational complexity of model behavior.
Submissions can be in three categories:
Submissions should follow the CEURART format. The templare is available here: http://ceur-ws.org/Vol-XXX/CEURART.zip. The proceedings shall be submitted to CEUR-WS.org for online publication. Authors of regular and short papers may opt out of having their work included in the proceedings. Abstracts of already published papers will not be included in the proceedings. We plan to evaluate the possibility of a journal special issue, depending on the outcome of the workshop.
Martin Grohe, RWTH Aachen University, Germany webpage
Graph neural networks (GNNs) are deep learning models for graph data that play a key role in machine learning on graphs. A GNN describes a distributed algorithm carrying out local computations at the vertices of the input graph. Typically, the parameters governing this algorithm are acquired through a data-driven learning process.
After reviewing GNNs and their basic theory, in this talk, I will focus on the expressiveness of recurrent GNNs. We show that recurrent GNNs can emulate all graph algorithms that respect the natural message-passing invariance induced by the colour refinement (or Weisfeiler-Leman) algorithm. Furthermore, we show that by incorporating random initialisation, recurrent GNNs can emulate all graph algorithms. This emulation introduces only a polynomial overhead in both time and space. In particular, any polynomial-time graph algorithm can be simulated by a recurrent GNN with random initialisation running in polynomial time.
(This is joint work with Eran Rosenbluth.)
Omri Isac, Hebrew University of Jerusalem, Israël webpage
As neural networks (NNs) become a critical part of our everyday lives, their unpredictability and opaqueness make their logical analysis both a challenging and a crucial problem. In this tutorial, we will explore Marabou, a tool for formally verifying deep neural networks (DNNs). Formal verification aims to determine whether a DNN satisfies a given logical property, providing rigorous guarantees about its behavior. The first part of the tutorial presents the theoretical foundations of DNN verification and an overview of Marabou’s core algorithms. The second part focuses on the practical aspects of verification: defining verification queries, specifying properties of interest, and using Marabou to verify them through its various heuristics and solving modes. Finally, time permitting, we will explore the proof-producing version of Marabou, discuss the importance of proof generation for trustworthy verification, and demonstrate how Marabou’s proofs can be independently checked. Participants are encouraged to install Marabou before the tutorial (https://github.com/NeuralNetworkVerification/Marabou) and follow along.
Feel free to contact
francois.schwarzentruber🐌ens-lyon.fr.