About me
I am a postdoctoral researcher in the Automated Reasoning Group, led by Anthony W. Lin, at RPTU Kaiserslautern-Landau, Germany.
I completed my PhD at the University of Kassel in 2025. My dissertation is The Complexity of Formal Verification of Neural Network Based Models.
Research
My research connects formal methods and machine learning. I study what neural networks can express, which properties can be verified algorithmically, and the computational complexity of these tasks. My work covers feedforward neural networks, graph neural networks, and transformers.
Award
2026 — GI Dissertation Award. I received the dissertation award jointly awarded by the Gesellschaft für Informatik (GI), the Austrian Computer Society (OCG), and the Swiss Informatics Society (SI) for my doctoral research on the formal verification of neural network models. Read the GI announcement.
Service
2026 — LOGICNN workshop organiser and proceedings editor. Together with François Schwarzentruber and Nicolas Troquard, I co-organised the Workshop on Logical Methods for Neural Network Analysis (LOGICNN 2026) at FLoC in Lisbon, Portugal, on July 25, 2026. We also co-edited the proceedings, published as CEUR Workshop Proceedings, volume 4276.
News
- October 2026: I contributed “Formale Verifikation für KI-Systeme” to GI-Radar 411, “Beweisbar sicher?”, discussing the possibilities and limits of formal verification for AI systems. Published on October 16; the article is in German.
- September 2026: The LOGICNN 2026 proceedings, which I co-edited with François Schwarzentruber and Nicolas Troquard, were published by CEUR-WS on September 29.
- September 2026: Our preprint Length Generalization for Transformers via Compression is available on arXiv.
- August 2026: Our paper The Complexity of Verifying Feedforward Neural Networks in Quantised Settings appeared at IJCAI-ECAI 2026.
- July 2026: Our papers Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable and The Polynomial Counting Capabilities of Message Passing Neural Networks appeared at KR 2026.
- April 2026: Our paper The Counting Power of Transformers appeared at ICLR 2026.
- January 2026: The journal version of Verifying and interpreting neural networks using finite automata appeared in Information and Computation.
- September 2025: Our paper The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics was accepted to NeurIPS 2025. I also gave a talk on this work at HIGHLIGHTS 2025 in Saarbrücken.
- August 2025: I gave a lecture at the Formosan Summer School on Logic, Language, and Computation (FLOLAC) at NTU in Taipei. Our paper Verifying Quantized Graph Neural Networks is PSPACE-complete appeared at IJCAI 2025 in Montreal.
- 2025: Our paper Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning appeared at ICLR 2025 in Singapore.
- February 2025: I joined the Automated Reasoning Group at RPTU in Kaiserslautern.
Earlier news (2023–2024)
- August 2024: I gave an invited talk titled “The Complexity of Formal Reasoning of Neural Network-Based Models” at the CerVerA seminar in Kaiserslautern.
- May 2024: Our work “Verifying and interpreting neural networks using finite automata” (M. Sälzer, E. Alsmann, F. Bruse, M. Lange) was accepted to DLT 2024 in Göttingen.
- April 2024: Our work A Logic for Reasoning About Aggregate-Combine Graph Neural Networks (P. Nunn, M. Sälzer, F. Schwarzentruber, N. Troquard) was accepted to IJCAI 2024 in Jeju.
- November 2023: I presented our work on GNN verification at the LoG Local Meetup in Munich, and gave an invited talk on the complexity of reachability for feedforward networks, GNNs, and transformers at the 68nqrt seminar in Rennes.
- July 2023: I gave a talk on the complexity of GNN verification at HIGHLIGHTS 2023 in Kassel.
- April 2023: Together with one of our master’s students, I presented our work on DNN-to-NFA translation at LiVe 2023 in Paris.
- March 2023: I gave talks on the complexity of GNN verification at the FM 2023 Doctoral Symposium in Lübeck and at AlMoTh 2023 in Bochum.