Autoformalization has emerged as a term referring to the automation of formalization in the context of the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in deep learning, especially large language models (LLMs). More recently, usage of the term has expanded beyond mathematics to describe tasks that involve translating natural language input into verifiable logical representations. At the same time, a growing body of research explores using LLMs to translate informal language into formal representations for reasoning, planning, and knowledge representation, but without explicitly referring to this process as autoformalization. As a result, despite addressing similar tasks, the largely independent development of these research areas has limited opportunities for shared methodologies, benchmarks, and theoretical frameworks that could accelerate progress. Our goal is to review - explicit or implicit - instances of what can be considered autoformalization and to propose a unified framework, encouraging cross-pollination between different fields to advance the development of next generation AI systems.

This paper explores how incompletely described tie-break policies can invalidate the experimental results reported in papers on optimal bidirectional heuristic search (BiHS). Experiments usually use a single implementation of an algorithm with its specific tie-break policy. When the tie-breaks are insufficiently described, we show that the results can be irreproducible, vary dramatically under different implementations, and lead to misleading assessments of an algorithm’s performance. To ensure reproducible and representative results, papers should either provide a description of the algorithm’s implementation, i.e., the complete tie-break policy, or alternatively, give results as a summary statistic representative of all possible tie-break implementations. We developed a software tool for this purpose.

AI planning technology faces performance issues with large-scale problems with negative preconditions. In this extended abstract, we show how to leverage the power of the Finite Domain Representation (FDR) used by the popular Fast Downward planner for such domains. FDR improves scalability thanks to its use of multi-valued state variables. However, it scales poorly when dealing with negative preconditions. We propose an alternative hybrid approach that evaluates negative preconditions on the fly during search but only when strictly needed. This is compared to the traditional use of domain-specific PDDL bookmark predicates, increasing memory usage, and automated transformations to Positive Normal Form, further escalating memory consumption.

In this paper, we perform a joint design of goal legibility and recognition in a cooperative, multi-agent pathfinding setting with partial observability. More specifically, we consider a set of identical agents (the actors) that move in an environment only partially observable to an observer in the loop. The actors are tasked with reaching a set of locations that need to be serviced in a timely fashion. The observer monitors the actors' behavior from a distance and needs to identify each actor's destination based on the actor's observable movements. Our approach generates legible paths for the actors; namely, it constructs one path from the origin to each destination so that these paths overlap as little as possible while satisfying budget constraints. It also equips the observer with a goal-recognition mapping between unique sequences of observations and destinations, ensuring that the observer can infer an actor's destination by making the minimum number of observations (legibility delay). Our method substantially extends previous work, which is limited to an observer with full observability, showing that optimizing pathfinding for goal legibility and recognition can be performed via a reformulation into a classical minimum cost flow problem in the partially observable case when the algorithms for the fully observable case are appropriately modified. Our empirical evaluation shows that our techniques are as effective in partially observable settings as in fully observable ones.

Lattice structures allow robotic systems to operate in complex and hazardous environments, e.g. construction, mining and nuclear plants, reliably and effectively. However, current navigation systems for these structures are neither realistic, as they assume simplistic motion primitives and obstacle-free workspaces, nor efficient as they rely solely on global discrete search in an attempt to leverage the modularity of lattices. This paper tackles this gap and studies how robots can navigate lattice structures efficiently. We present a realistic application environment where robots have to avoid obstacles and the structure itself to reach target locations. Our solution couples discrete optimal search, using a domain-dependent heuristic, and sampling-based motion planning to find feasible trajectories in the discrete search space and in the continuous joint space at the same time. We provide two search graph formulations and a path planning approach. Simulation experiments, based on structures and robots created for the Innovate UK Connect-R project, examine scalability to large grid spaces while maintaining performances close to optimal.

In this paper, we present a set of strategies to underpin the behavior of an agent that wants to arrive as close as possible to its destination without revealing it to an observer, which monitors its progress in the environment. This problem is an instance of goal obfuscation (GO), which has lately received significant attention in the AI community. With different variants of GO being proposed, the field lacks coherence and characterization from first principles. In addition, existing techniques are not robust to possible attempts of the observer to learn the agent's strategy. To fill this gap, we provide here a foundational study of GO and offer robust techniques to ensure that the agent can protect its privacy as much as possible regardless of the observer's behavior. We cast GO as an optimization problem, offer a complete theoretical analysis of it and introduce efficient algorithms to find exact solutions.

Abstraction heuristics are a leading approach for deriving admissible estimates in cost-optimal planning. However, a drawback with respect to other families of heuristics is that they require a preprocessing phase for choosing the abstraction, computing the abstract distances, and/or suitable cost-partitionings. Typically, this is performed in advance by a fixed amount of time, even though some instances could be solved much faster with little or no preprocessing. We interleave the computation of abstraction heuristics with search, avoiding a long precomputation phase and allowing information from the search to be used for guiding the abstraction selection. To evaluate our ideas, we implement them on a planner that uses a single symbolic PDB. Our results show that delaying the preprocessing is not harmful in general even when an important amount of preprocessing is required to obtain good performance.

Two key aspects of problem solving are representation and search heuristics. Both theoretical and experimental studies have shown that there is no one best problem representation nor one best search heuristic. Therefore, some recent methods, e.g., portfolios, learn a good combination of problem solvers to be used in a given domain or set of domains. There are even dynamic portfolios that select a particular combination of problem solvers specific to a problem. These approaches: (1) need to perform a learning step; (2) do not usually focus on changing the representation of the input domain/problem; and (3) frequently do not adapt the portfolio to the specific problem. This paper describes a meta-reasoning system that searches through the space of combinations of representations and heuristics to find one suitable for optimally solving the specific problem. We show that this approach can be better than selecting a combination to use for all problems within a domain and is competitive with state of the art optimal planners.

A pattern database (PDB) for a planning task is a heuristic function in the form of a lookup table that contains optimal solution costs of a simplified version of the task. In this paper we introduce a method that sequentially creates multiple PDBs which are later combined into a single heuristic function. At a given iteration, our method uses estimates of the A* running time to create a PDB that complements the strengths of the PDBs created in previous iterations. We evaluate our algorithm using explicit and symbolic PDBs. Our results show that the heuristics produced by our approach are able to outperform existing schemes, and that our method is able to create PDBs that complement the strengths of other existing heuristics such as a symbolic perimeter heuristic.

The global growth in urbanisation increases the demand for services including road transport infrastructure, presenting challenges in terms of mobility. Optimising the exploitation of urban road network, while attempting to minimise the effects of traffic emissions, is a great challenge. SimplyfAI was a UK research council grant funded project which was aimed towards solving air quality problems caused by road traffic emissions. Large cities such as Manchester struggle to meet air quality limits as the range of available traffic management devices is limited. In the study, we investigated the application of linked data to enrich environmental and traffic data feeds, and we used this with automated planning tools to enable traffic to be managed at a region level. The management will have the aim of avoiding air pollution problems before they occur. This demo focuses on the planning component, and in particular the engineering and validation aspects, that were pivotal for the success of the project.

This paper describes a system that automatically transforms a PDDL encoding, calls a planner to solve the transformed representation, and translates the solution back into the original representation. The approach involves counting objects that are indistinguishable, rather than treating them as individuals, which eliminates some unnecessary combinatorial explosion.