Search

We propose a method to capture the handling abilities of fast jet pilots in a software model via reinforcement learning (RL) from human preference feedback. We use pairwise preferences over simulated flight trajectories to learn an interpretable rule-based model called a reward tree, which enables the automated scoring of trajectories alongside an explanatory rationale. We train an RL agent to execute high-quality handling behaviour by using the reward tree as the objective, and thereby generate data for iterative preference collection and further refinement of both tree and agent. Experiments with synthetic preferences show reward trees to be competitive with uninterpretable neural network reward models on quantitative and qualitative evaluations., Comment: arXiv admin note: substantial text overlap with arXiv:2210.01007

Recent efforts to learn reward functions from human feedback have tended to use deep neural networks, whose lack of transparency hampers our ability to explain agent behaviour or verify alignment. We explore the merits of learning intrinsically interpretable tree models instead. We develop a recently proposed method for learning reward trees from preference labels, and show it to be broadly competitive with neural networks on challenging high-dimensional tasks, with good robustness to limited or corrupted data. Having found that reward tree learning can be done effectively in complex settings, we then consider why it should be used, demonstrating that the interpretable reward structure gives significant scope for traceability, verification and explanation., Comment: 22 pages (9 main body). Preprint, under review

We introduce a data-driven, model-agnostic technique for generating a human-interpretable summary of the salient points of contrast within an evolving dynamical system, such as the learning process of a control agent. It involves the aggregation of transition data along both spatial and temporal dimensions according to an information-theoretic divergence measure. A practical algorithm is outlined for continuous state spaces, and deployed to summarise the learning histories of deep reinforcement learning agents with the aid of graphical and textual communication methods. We expect our method to be complementary to existing techniques in the realm of agent interpretability., Comment: 13 pages (6 body, 1 references, 6 appendix). Accepted for presentation at XAI-IJCAI22 Workshop, July 2022

To investigate the impact of Autonomous Vehicles (AVs) on urban congestion, this study looks at their performance at road intersections. Intersection performance has been studied across a range of traffic densities using a simple MATLAB simulation of two intersecting 1-D flows of homogeneous automated vehicles. This lacks the detail of more advanced simulations, but it enables fast identification of fundamental behaviours. The results show that there are distinct crossing regimes at low, medium and high densities. Furthermore, the transitions between regimes can be predicted analytically and their performance related to the fundamental model of 1-D traffic flow. These findings have the potential to focus efforts on the development of improved decision-making rules for emerging AVs.

As we deploy autonomous agents in safety-critical domains, it becomes important to develop an understanding of their internal mechanisms and representations. We outline an approach to imitation learning for reverse-engineering black box agent policies in MDP environments, yielding simplified, interpretable models in the form of decision trees. As part of this process, we explicitly model and learn agents' latent state representations by selecting from a large space of candidate features constructed from the Markov state. We present initial promising results from an implementation in a multi-agent traffic environment., Comment: 6 pages, 3 figures; under review for the 1st TAILOR Workshop, due to take place 29-30 August 2020 in Santiago de Compostela

The Travelling Salesman and its variations are some of the most well known NP hard optimisation problems. This paper looks to use both centralised and decentralised implementations of Evolutionary Algorithms (EA) to solve a dynamic variant of the Multi-Agent Travelling Salesman Problem (MATSP). The problem is dynamic, requiring an on-line solution, whereby tasks are completed during simulation with new tasks added and completed ones removed. The problem is allocating an active set of tasks to a set of agents whilst simultaneously planning the route for each agent. The allocation and routing are closely coupled parts of the same problem making it difficult to decompose, instead this paper uses multiple populations with well defined interactions to exploit the problem structure. This work attempts to align the real world implementation demands of a decentralised solution, where agents are far apart and have communication limits, to that of the structure of the multi-demic EA solution process, ultimately allowing decentralised parts of the problem to be solved `on board' agents and allow for robust communication and exchange of tasks.

Autonomous robots must operate in complex and changing environments subject to requirements on their behaviour. Verifying absolute satisfaction (true or false) of these requirements is challenging. Instead, we analyse requirements that admit flexible degrees of satisfaction. We analyse vague requirements using fuzzy logic, and probabilistic requirements using model checking. The resulting analysis method provides a partial ordering of system designs, identifying trade-offs between different requirements in terms of the degrees to which they are satisfied. A case study involving a home care robot interacting with a human is used to demonstrate the approach.

The widespread adoption of autonomous systems depends on providing guarantees of safety and functional correctness, at both design time and runtime. Information about the extent to which functional requirements can be met in combination with non-functional requirements (NFRs) -- i.e. requirements that can be partially complied with -- , under dynamic and uncertain environments, provides opportunities to enhance the safety and functional correctness of systems at design time. We present a technique to formally define system attributes that can change or be changed to deal with dynamic and uncertain environments (denominated weakened specifications) as a partially ordered lattice, and to automatically explore the system under different specifications, using probabilistic model checking, to find the likelihood of satisfying a requirement. The resulting probabilities form boundaries of "optimal specifications", analogous to Pareto frontiers in multi-objective optimization, informing the designer about the system's capabilities, such as resilience or robustness, when changing its attributes to deal with dynamic and uncertain environments. We illustrate the proposed technique through a domestic robotic assistant example.

This paper presents the verification of control systems implemented in Simulink. The goal is to ensure that high-level requirements on control performance, like stability, are satisfied by the Simulink diagram. A two stage process is proposed. First, the high-level requirements are decomposed into specific parametrized sub-requirements and implemented as assertions in Simulink. Second, the verification takes place. On one hand, the sub-requirements are verified through assertion checks in simulation. On the other hand, according to their scope, some of the sub-requirements are verified through assertion checks in simulation, and others via automatic theorem proving over an ideal mathematical model of the diagram. We compare performing only assertion checks against the use of theorem proving, to highlight the advantages of the latter. Theorem proving performs verification by computing a mathematical proof symbolically, covering the entire state space of the variables. An automatic translation tool from Simulink to the language of the theorem proving tool Why3 is also presented. The paper demonstrates our approach by verifying the stability of a simple discrete linear system., Comment: Accepted, waiting for publication. European Control Conference, July 2015, Linz, Austria

This paper presents the deductive formal verification of high-level properties of control systems with theorem proving, using the Why3 tool. Properties that can be verified with this approach include stability, feedback gain, and robustness, among others. For the systems, modelled in Simulink, we propose three main steps to achieve the verification: specifying the properties of interest over the signals within the model using Simulink blocks, an automatic translation of the model into Why3, and the automatic verification of the properties with theorem provers in Why3. We present a methodology to specify the properties in the model and a library of relevant assertion blocks (logic expressions), currently in development. The functionality of the blocks in the Simulink models are automatically translated to Why3 as theories and verification goals by our tool implemented in MATLAB. A library of theories in Why3 corresponding to each supported block has been developed to facilitate the process of translation. The goals are automatically verified in Why3 with relevant theorem provers. A simple first-order discrete system is used to exemplify the specification of the Simulink model, the translation process from Simulink to the Why3 formal logic language, and the verification of Lyapunov stability., Comment: Accepted to be presented in UKACC, Loughborough, UK, 2014. Final reference to appear on publication