Our research addresses a core tension in AI: machine learning (ML) methods generalize well but remain opaque, while symbolic planning offers explainability and provable optimality guarantees but struggles with scalability and adaptation to changing environments.

We work on neuro-symbolic methods to combine the strengths of planning and ML for the full development cycle of planning-based systems:

  • From model construction, where ML predicts parts of the formal planning model from data,
  • through solving, where symbolic and learned techniques combine into high-performing solvers with formal guarantees such as optimality,
  • to trustworthy deployment, where systems earn the trust of the humans who rely on them through formal safety verification and testing, as well as plan explanation.

The NSP Group is an Emmy Noether Independent Research Group funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation), project number 572954863.

News

  • Our paper An Admissible Neuro-Symbolic Landmark Cut Heuristic – Preliminary Results by Magnus Cunow, Nicola Müller, Timo Gros, Gregor Behnke, and Daniel Höller got accepted at the ICAPS Workshop on Bridging the Gap Between AI Planning and (Reinforcement) Learning (PRL).
  • Our paper Safety Verification of Additive Tree Ensemble Policies via Symbolic Search by Marcel Schubert and Daniel Höller got accepted at the ICAPS Workshop on Reliability In Planning and Learning (RIPL).
  • Daniel Höller got a Gold Tier Reviewer Distinction at IJCAI 2026.
  • The Neuro-Symbolic Planning (NSP) Group has been established as an Emmy Noether Independent Research Group at Saarland Informatics Campus!

People

Software

  • The LION system is a lifted HTN planning system that uses learned heuristic values to guide he search.
  • The PANDA system is a framework with various functionalities in the context of hierarchical planning: grounding and preprocessing, various solvers, and problem compilations e.g. of plan and goal recognition problems to planning problems or of plan verification problems to planning problems. You can find the software here, and an article summarizing the main functionality here.
  • The TOAD system is a translation-based HTN solver that translates HTN planning problems to classical planning problems and uses approximation instead of bounding to overcome the differences in expressivity. The approach is inspired my work on expressivity, it is described in this paper. You can find the software here.
  • The LiSAT system is a translation-based solver for lifted classical planning that translates lifted classical planning problems to SAT problems in propositional logic. The approach is described here, you can find the software here.