Research
[DFG] Scalable Automated Reasoning[DFG] Scalable Automated Reasoning
The German Research Foundation (DFG) is funding Dominik Schreiber’s Emmy Noether junior research group project entitled Scalable Automated Reasoning in the context of the funding initiative Methods in Artificial Intelligence.
See also the DFG announcement with all funded Emmy Noether groups.
Project duration: 2026 - 2032
Funding source: DFG Emmy Noether project, 2025 call “Methods of AI”
Principal Investigator: Dominik Schreiber
Collaboration partners: Peter Sanders, Bernhard Beckert, Armin Biere, Birte Glimm, Katalin Fazekas, Nils Froleyks, Keijo Heljanko, Matti Järvisalo, Jeremias Berg, Aina Niemetz, Mathias Preiner, Marijn Heule, Yong Kiam Tan
Automated Reasoning (AR) entails the algorithmic exploration of a formal rule set in order to deduce precise properties. The central algorithmic tools of AR include theorem proving for propositional logic (SAT) and first-order logics as well as combinatorial optimization. While sub-symbolic AI methods (machine learning, generative AI) perform associative reasoning steered by data-driven most-likelihood decisions, symbolic AI methods excel at the efficient and precise search of huge combinatorial spaces, yielding provable guarantees.
Complementing today’s ubiquitous sub-symbolic AI with powerful symbolic AI, i.e., with precise and provably correct reasoning, can be considered a grand challenge of modern computer science. However, while sub-symbolic AI profits tremendously from massively parallel computing, critical AR tools have been falling behind and can only make little use of parallel, let alone distributed and/or GPU-based systems. The funded Emmy Noether project aims to address these shortcomings and advance the scalability of crucial, generic AR tools. We also want to transfer the resulting feature-rich scalable approaches to fundamental tools in the domains of verification, electronic design, explainability, and mathematical theorem proving. We expect that this will not only directly empower numerous important workflows in science and industry but also render the use of parallel and distributed systems more attractive for users of AR in the longer term.
Throughout the project, we will strive to produce efficient, accessible, and well-documented open-source software artifacts that go beyond academic proof-of-concept pieces and can therefore find widespread, long-term adoption by scientific and industrial actors.