SAtRes    News    Emmy Noether Project "Scalable Automated Reasoning"

Emmy Noether Project "Scalable Automated Reasoning"

March 27, 2026

The German Research Foundation (DFG) has announced to fund Dominik Schreiber’s Emmy Noether research group project entitled Scalable Automated Reasoning in the context of the funding initiative Methods in Artificial Intelligence.

About the project

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. The project is endorsed by a total of thirteen collaboration partners from six countries, including Armin Biere, Marijn Heule, Matti Järvisalo, and Yong Kiam Tan.

Background

The promised funding for an Emmy Noether group presents an exciting opportunity to continue and intensify our young investigator group’s research, also beyond the time frame of our current main funding source (the Helmholtz pilot programme Core Informatics at KIT (KiKIT), 2024-2027).
We expect the project to be kicked off in Fall 2026, which likely also entails moving the group to a different university in Germany (yet to be determined/announced).

The DFG’s Emmy Noether Programme is a prestigious funding initiative designed to support early-career researchers in Germany. As stated on the DFG webpage, “The Emmy Noether Programme gives exceptionally qualified early career researchers the chance to qualify for the post of professor at a university by leading an independent junior research group for a period of six years.” The programme is named in honor of the renowned German mathematician Amalie Emmy Noether (1882-1935).

See also the DFG’s announcement with all funded Emmy Noether groups.