Closed-Loop Safety Verification of Learned Tree-Ensemble Policies in Planning

• Applicant: Professor Dr. Jörg Hoffmann
• Subject Area: Methods in Artificial Intelligence and Machine Learning
• Term: since 2026
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 568838440

Safe AI, in particular verifying the safety of learned decision components, is a pressing issue in AI today. In this project, we focus on action policies in AI planning: learned functions pi from states to actions, used to control an agent whose objective is to reach a goal state. We propose to address closed-loop safety verification, proving that pi never enters an unsafe state; along with a tight link to learning pi in a way supporting verifiability. We propose to address this for policies pi represented as tree ensembles. This is motivated by our recent joint prior work (ECAI'24), where we developed a policy predicate abstraction (PPA) framework for closed-loop safety verification of tree ensemble policies in the AI planning context. We found that tree ensembles can often achieve similar performance as neural networks while being orders of magnitude easier to verify. Tree-ensembles may thus offer a better trade-off between performance vs. verifiability, within the realm of policies where formal verification is feasible. This hypothesis may have far-reaching consequences for the choice of ML model when verifiability is a major concern. The goal of our proposal is to confirm the hypothesis. This requires addressing several, significant inter-related technical gaps arising because tree ensembles in general require complex input features, going beyond the environment state representation in terms of state variables, to perform well. First, we need methods to automatically construct suitable complex features during the training process, geared at policy performance while at the same time taking into account verification complexity. Second, we need to extend PPA to handle complex features. This involves reasoning about constraints on such features, a capability current tree-ensemble reasoners do not have. Furthermore, complex features entail a new form of spuriousness (imprecision) in PPA, that requires extended abstraction refinement methods. We will address these challenges for environments modeled as automata, as in our prior work; as well as in PDDL, the de-facto standard in AI planning, which comes with the key added challenge of cross-instance learning and verification. The project merges PI Davis' expertise in tree-ensemble learning and reasoning with PI Hoffmann's expertise in AI planning and closed-loop policy safety verification. This merge of expertise is necessary, it would be impossible for one of the partners alone to successfully carry out the proposed research.

• DFG Programme: Research Grants
• International Connection: Belgium
• Cooperation Partner: Professor Jesse Davis, Ph.D.