arXiv subjects

Jörg Hoffmann

Publications and source records attributed to Jörg Hoffmann.

At least 19 recordsLinked to original sources

arXiv2026

Provably Complete Generalized Planning with LLMs

Generalized planning aims to compute a plan that solves all instances of a planning domain. Recent work has used LLMs to automatically generate and debug such generalized plans in the form of Python programs and achieved perfect test data coverage for several domains. However, whether these generalized plans are actually complete, i.e. solve all instances of the domain, could only be determined by manual evaluation. Here, we present an approach for automatically generating generalized plans in Lean together with proofs of their completeness relative to a specification of the domain constraints provided as input. We introduce a semantic-preserving PDDL-to-Lean conversion, and use an LLM to generate both the generalized plan and the formal proof that it solves every instance satisfying the domain constraints. The correctness of the completeness proof is determined by Lean's kernel. We evaluate our approach on 13 commonly used benchmark domains, using GPT-5.6-Sol as the LLM. For 12 of the domains we obtain generalized plans together with valid completeness proofs. This is a major advancement of the state of the art in automatic generalized-plan completeness proofs.

cs.AI↗

arXiv2026

Generating Instance Generators in PDDL Planning

PDDL, the de-facto standard language in the AI Planning community, is designed to specify planning domains: sets of instances that share the same predicates and action schemas. Yet it does not provide any means to specify the actual instance set, i.e., legality constraints on initial states and goal conditions, as well as possibly domain subset constraints specifying an instance subset we are interested in. One consequence of this is that instance generation has always been ad-hoc, with manually written domain- and subset-specific instance generators. Recent work has started to address this, through reasoning and learning methods that however suffer from scalability limitations. Here we introduce an alternative approach, leveraging LLMs to generate instance-generation programs, with built-in soundness guarantees through prescribed checks. We show that these automatically generated instance generators return large numbers of sound and diverse instances efficiently.

cs.AI↗

arXiv2026

Improved Generalized Planning with LLMs through Strategy Refinement and Reflection

LLMs have recently been used to generate Python programs representing generalized plans in PDDL planning, i.e., plans that generalize across the tasks of a given PDDL domain. Previous work proposed a framework consisting of three steps: the LLM first generates a summary and then a strategy for the domain, both in natural language, and then implements that strategy as a Python program, that gets debugged on example planning tasks. In that work, only one strategy is generated and passed directly to the program generation. If the strategy is incorrect, its implementation will therefore result in an incorrect generalized plan. Here, we introduce an approach that generates the strategy in the form of pseudocode and enables automatic debugging of the pseudocode, hence allowing us to identify and fix errors prior to the generation of the generalized plan itself. Additionally, we extend the Python debugging phase with a reflection step prompting the LLM to pinpoint the reason for the observed plan failure. Finally, we take inspiration from LLM code generation to produce several program variants and pick the best one. Running experiments on 17 benchmark domains with two reasoning and two non-reasoning LLMs, we show that these extensions substantially improve the quality of the generalized plans. Our best performing configuration achieves an average coverage of 82% across the domains.

cs.AI↗

arXiv2026

Per-Domain Generalizing Policies: On Learning Efficient and Robust Q-Value Functions (Extended Version with Technical Appendix)

Learning per-domain generalizing policies is a key challenge in learning for planning. Standard approaches learn state-value functions represented as graph neural networks using supervised learning on optimal plans generated by a teacher planner. In this work, we advocate for learning Q-value functions instead. Such policies are drastically cheaper to evaluate for a given state, as they need to process only the current state rather than every successor. Surprisingly, vanilla supervised learning of Q-values performs poorly as it does not learn to distinguish between the actions taken and those not taken by the teacher. We address this by using regularization terms that enforce this distinction, resulting in Q-value policies that consistently outperform state-value policies across a range of 10 domains and are competitive with the planner LAMA-first.

cs.AI↗

arXiv2026

Intelligent support for Human Oversight: Integrating Reinforcement Learning with Gaze Simulation to Personalize Highlighting

Interfaces for human oversight must effectively support users' situation awareness under time-critical conditions. We explore reinforcement learning (RL)-based UI adaptation to personalize alerting strategies that balance the benefits of highlighting critical events against the cognitive costs of interruptions. To enable learning without real-world deployment, we integrate models of users' gaze behavior to simulate attentional dynamics during monitoring. Using a delivery-drone oversight scenario, we present initial results suggesting that RL-based highlighting can outperform static, rule-based approaches and discuss challenges of intelligent oversight support.

cs.HC↗

arXiv2025

Planning Ahead with RSA: Efficient Signalling in Dynamic Environments by Projecting User Awareness across Future Timesteps

Adaptive agent design offers a way to improve human-AI collaboration on time-sensitive tasks in rapidly changing environments. In such cases, to ensure the human maintains an accurate understanding of critical task elements, an assistive agent must not only identify the highest priority information but also estimate how and when this information can be communicated most effectively, given that human attention represents a zero-sum cognitive resource where focus on one message diminishes awareness of other or upcoming information. We introduce a theoretical framework for adaptive signalling which meets these challenges by using principles of rational communication, formalised as Bayesian reference resolution using the Rational Speech Act (RSA) modelling framework, to plan a sequence of messages which optimise timely alignment between user belief and a dynamic environment. The agent adapts message specificity and timing to the particulars of a user and scenario based on projections of how prior-guided interpretation of messages will influence attention to the interface and subsequent belief update, across several timesteps out to a fixed horizon. In a comparison to baseline methods, we show that this effectiveness depends crucially on combining multi-step planning with a realistic model of user awareness. As the first application of RSA for communication in a dynamic environment, and for human-AI interaction in general, we establish theoretical foundations for pragmatic communication in human-agent teams, highlighting how insights from cognitive science can be capitalised to inform the design of assistive agents.

cs.AI↗

arXiv2025

Automating the Generation of Prompts for LLM-based Action Choice in PDDL Planning

Large language models (LLMs) have revolutionized a large variety of NLP tasks. An active debate is to what extent they can do reasoning and planning. Prior work has assessed the latter in the specific context of PDDL planning, based on manually converting three PDDL domains into natural language (NL) prompts. Here we automate this conversion step, showing how to leverage an LLM to automatically generate NL prompts from PDDL input. Our automatically generated NL prompts result in similar LLM-planning performance as the previous manually generated ones. Beyond this, the automation enables us to run much larger experiments, providing for the first time a broad evaluation of LLM planning performance in PDDL. Our NL prompts yield better performance than PDDL prompts and simple template-based NL prompts. Compared to symbolic planners, LLM planning lags far behind; but in some domains, our best LLM configuration scales up further than A$^\star$ using LM-cut.

cs.AI↗

arXiv2025

Per-Domain Generalizing Policies: On Validation Instances and Scaling Behavior

Recent work has shown that successful per-domain generalizing action policies can be learned. Scaling behavior, from small training instances to large test instances, is the key objective; and the use of validation instances larger than training instances is one key to achieve it. Prior work has used fixed validation sets. Here, we introduce a method generating the validation set dynamically, on the fly, increasing instance size so long as informative and feasible.We also introduce refined methodology for evaluating scaling behavior, generating test instances systematically to guarantee a given confidence in coverage performance for each instance size. In experiments, dynamic validation improves scaling behavior of GNN policies in all 9 domains used.

cs.LG↗

arXiv2025

A thin film source in a solid-state diffusion experiment: CoO on SrTiO3

To realize a chemical diffusion experiment for simple quantitative analysis of one-dimensional diffusion profiles requires the fabrication of a planar and chemically sharp interface between two phases, one serving as the diffusion source and the other as the material to be studied. We demonstrate a thin film source on top of single crystals or epitaxial films for the example of cobalt (II) oxide (CoO) grown on top of SrTiO3 (STO) by ion beam sputtering. After deposition at room temperature, a nanocrystalline film with flat and chemically sharp interface is present. Diffusion annealing leads to a partial formation of the Co3O4 phase and recrystallization accompanied by a strong increase of the surface and the interface roughness. We report the conditions, where compact and stable CoO layers with flat interface can be maintained, serving as a constant source for Co diffusion. Exemplarily, the formation of a Co-diffusion profile is demonstrated after annealing of 240 h at 1163 K and comparatively studied by using three different methods: Energy dispersive x-ray spectroscopy (EDX) in a transmission electron microscope (TEM), atom probe tomography (APT) and time of flight secondary ion mass spectroscopy (TOF SIMS). Local and rather macroscopic concentration profiling do well agree within error.

cond-mat.mtrl-sci↗

arXiv2022

Specifying and Testing $k$-Safety Properties for Machine-Learning Models

Machine-learning models are becoming increasingly prevalent in our lives, for instance assisting in image-classification or decision-making tasks. Consequently, the reliability of these models is of critical importance and has resulted in the development of numerous approaches for validating and verifying their robustness and fairness. However, beyond such specific properties, it is challenging to specify, let alone check, general functional-correctness expectations from models. In this paper, we take inspiration from specifications used in formal methods, expressing functional-correctness properties by reasoning about $k$ different executions, so-called $k$-safety properties. Considering a credit-screening model of a bank, the expected property that "if a person is denied a loan and their income decreases, they should still be denied the loan" is a 2-safety property. Here, we show the wide applicability of $k$-safety properties for machine-learning models and present the first specification language for expressing them. We also operationalize the language in a framework for automatically validating such properties using metamorphic testing. Our experiments show that our framework is effective in identifying property violations, and that detected bugs could be used to train better models.

cs.LG↗

arXiv2022

Expressivity of Planning with Horn Description Logic Ontologies (Technical Report)

State constraints in AI Planning globally restrict the legal environment states. Standard planning languages make closed-domain and closed-world assumptions. Here we address open-world state constraints formalized by planning over a description logic (DL) ontology. Previously, this combination of DL and planning has been investigated for the light-weight DL DL-Lite. Here we propose a novel compilation scheme into standard PDDL with derived predicates, which applies to more expressive DLs and is based on the rewritability of DL queries into Datalog with stratified negation. We also provide a new rewritability result for the DL Horn-ALCHOIQ, which allows us to apply our compilation scheme to quite expressive ontologies. In contrast, we show that in the slight extension Horn-SROIQ no such compilation is possible unless the weak exponential hierarchy collapses. Finally, we show that our approach can outperform previous work on existing benchmarks for planning with DL ontologies, and is feasible on new benchmarks taking advantage of more expressive ontologies. That is an extended version of a paper accepted at AAAI 22.

cs.AI↗

arXiv2022

An Explainable AI System for the Diagnosis of High Dimensional Biomedical Data

Typical state of the art flow cytometry data samples consists of measures of more than 100.000 cells in 10 or more features. AI systems are able to diagnose such data with almost the same accuracy as human experts. However, there is one central challenge in such systems: their decisions have far-reaching consequences for the health and life of people, and therefore, the decisions of AI systems need to be understandable and justifiable by humans. In this work, we present a novel explainable AI method, called ALPODS, which is able to classify (diagnose) cases based on clusters, i.e., subpopulations, in the high-dimensional data. ALPODS is able to explain its decisions in a form that is understandable for human experts. For the identified subpopulations, fuzzy reasoning rules expressed in the typical language of domain experts are generated. A visualization method based on these rules allows human experts to understand the reasoning used by the AI system. A comparison to a selection of state of the art explainable AI systems shows that ALPODS operates efficiently on known benchmark data and also on everyday routine case data.

cs.LG↗

arXiv2020

Iterative Planning with Plan-Space Explanations: A Tool and User Study

In a variety of application settings, the user preference for a planning task - the precise optimization objective - is difficult to elicit. One possible remedy is planning as an iterative process, allowing the user to iteratively refine and modify example plans. A key step to support such a process are explanations, answering user questions about the current plan. In particular, a relevant kind of question is "Why does the plan you suggest not satisfy $p$?", where p is a plan property desirable to the user. Note that such a question pertains to plan space, i.e., the set of possible alternative plans. Adopting the recent approach to answer such questions in terms of plan-property dependencies, here we implement a tool and user interface for human-guided iterative planning including plan-space explanations. The tool runs in standard Web browsers, and provides simple user interfaces for both developers and users. We conduct a first user study, whose outcome indicates the usefulness of plan-property dependency explanations in iterative planning.

cs.AI↗

arXiv2020

Phase transitions in a perovskite thin film studied by environmental in-situ heating nano-beam electron diffraction

The rich phase diagram of bulk Pr$_{1-x}$Ca$_{x}$MnO$_3$ resulting in a high tunability of physical properties gave rise to various studies related to fundamental research as well as prospective applications of the material. Importantly, as a consequence of strong correlation effects, electronic and lattice degrees of freedom are vigorously coupled. Hence, it is debatable whether such bulk phase diagrams can be transferred to inherently strained epitaxial thin films. In this paper, the structural orthorhombic to pseudo-cubic transition for $x=0.1$ is studied in ion-beam sputtered thin films and point out differences to the respective bulk system by employing in-situ heating nano-beam electron diffraction to follow the temperature dependence of lattice constants. In addition, it is demonstrated that controlling the environment during heating, i.e. preventing oxygen loss, is crucial in order to avoid irreversible structural changes, which is expected to be a general problem of compounds containing volatile elements under non-equilibrium conditions.

cond-mat.mtrl-sci↗

arXiv2020

Generating Instructions at Different Levels of Abstraction

When generating technical instructions, it is often convenient to describe complex objects in the world at different levels of abstraction. A novice user might need an object explained piece by piece, while for an expert, talking about the complex object (e.g. a wall or railing) directly may be more succinct and efficient. We show how to generate building instructions at different levels of abstraction in Minecraft. We introduce the use of hierarchical planning to this end, a method from AI planning which can capture the structure of complex objects neatly. A crowdsourcing evaluation shows that the choice of abstraction level matters to users, and that an abstraction strategy which balances low-level and high-level object descriptions compares favorably to ones which don't.

cs.CL↗

arXiv2020

Tailoring c-axis orientation in epitaxial Ruddlesden-Popper Pr$_{0.5}$Ca$_{1.5}$MnO$_{4}$ films

Interest for layered Ruddlesden-Popper strongly correlated manganites of Pr$_{0.5}$Ca$_{1.5}$MnO$_4$ as well as to their thin film polymorphs is motivated by the high temperature of charge orbital ordering above room temperature. We report on the tailoring of the c-axis orientation in epitaxial RP-PCMO films grown on SrTiO$_3$ (STO) substrates with different orientations as well as the use of CaMnO$_3$ (CMO) buffer layers. Films on STO(110) reveal in-plane alignment of the c-axis lying along to the [100] direction. On STO(100), two possible directions of the in-plane c-axis lead to a mosaic like, quasi two-dimensional nanostructure, consisting of RP, rock-salt and perovskite building blocks. With the use of a CMO buffer layer, RP-PCMO epitaxial films with c-axis out-of-plane were realized. Different physical vapor deposition techniques, i.e. ion beam sputtering (IBS), pulsed laser deposition (PLD) as well as metalorganic aerosol deposition (MAD) are applied in order to distinguish between the effect of growth conditions and intrinsic epitaxial properties. For all deposition techniques, despite their very different growth conditions, the surface morphology, crystal structure and orientation of the thin films reveal a high level of similarity as verified by X-ray diffraction, scanning and high resolution transmission electron microscopy. We found that for different epitaxial relations the stress in the films can be relaxed by means of a modified interface chemistry. The charge ordering in the films estimated by resistivity measurements occurs at a temperature close to that expected in bulk material.

cond-mat.mtrl-sci↗

arXiv2020

Tracking the Race Between Deep Reinforcement Learning and Imitation Learning -- Extended Version

Learning-based approaches for solving large sequential decision making problems have become popular in recent years. The resulting agents perform differently and their characteristics depend on those of the underlying learning approach. Here, we consider a benchmark planning problem from the reinforcement learning domain, the Racetrack, to investigate the properties of agents derived from different deep (reinforcement) learning approaches. We compare the performance of deep supervised learning, in particular imitation learning, to reinforcement learning for the Racetrack model. We find that imitation learning yields agents that follow more risky paths. In contrast, the decisions of deep reinforcement learning are more foresighted, i.e., avoid states in which fatal decisions are more likely. Our evaluations show that for this sequential decision making problem, deep reinforcement learning performs best in many aspects even though for imitation learning optimal decisions are considered.

cs.LG↗

arXiv2019

Towards Automated Network Mitigation Analysis (extended)

Penetration testing is a well-established practical concept for the identification of potentially exploitable security weaknesses and an important component of a security audit. Providing a holistic security assessment for networks consisting of several hundreds hosts is hardly feasible though without some sort of mechanization. Mitigation, prioritizing counter-measures subject to a given budget, currently lacks a solid theoretical understanding and is hence more art than science. In this work, we propose the first approach for conducting comprehensive what-if analyses in order to reason about mitigation in a conceptually well-founded manner. To evaluate and compare mitigation strategies, we use simulated penetration testing, i.e., automated attack-finding, based on a network model to which a subset of a given set of mitigation actions, e.g., changes to the network topology, system updates, configuration changes etc. is applied. Using Stackelberg planning, we determine optimal combinations that minimize the maximal attacker success (similar to a Stackelberg game), and thus provide a well-founded basis for a holistic mitigation strategy. We show that these Stackelberg planning models can largely be derived from network scan, public vulnerability databases and manual inspection with various degrees of automation and detail, and we simulate mitigation analysis on networks of different size and vulnerability.

cs.CR↗