SearcharxivSearch

arXiv subjects

Simon Burton

Publications and source records attributed to Simon Burton.

At least 19 recordsLinked to original sources

Meromorphic Quantum Computing

We consider the kinematic axioms of quantum mechanics projectively. Instead of normalized (pure) states up to global phase, states become one-dimensional subspaces of vector spaces. This process of projectivization is functorial and lax monoidal. For qubits it identifies the Bloch sphere with the Riemann sphere. We interpret a fragment of the ZXW-calculus projectively and thereby provide an alternate derivation of the arithmetic GHZ/W-calculus of Coecke et al. We find meromorphic functions that characterize the coherent behaviour of circuits for logical state preparation of quantum codes and magic state distillation.

quant-ph

Milestone Determination for Autonomous Railway Operation

In the field of railway automation, one of the key challenges has been the development of effective computer vision systems due to the limited availability of high-quality, sequential data. Traditional datasets are restricted in scope, lacking the spatio temporal context necessary for real-time decision-making, while alternative solutions introduce issues related to realism and applicability. By focusing on route-specific, contextually relevant cues, we can generate rich, sequential datasets that align more closely with real-world operational logic. The concept of milestone determination allows for the development of targeted, rule-based models that simplify the learning process by eliminating the need for generalized recognition of dynamic components, focusing instead on the critical decision points along a route. We argue that this approach provides a practical framework for training vision agents in controlled, predictable environments, facilitating safer and more efficient machine learning systems for railway automation.

cs.CV

A Classification of Transversal Clifford Gates for Qubit Stabilizer Codes

This work classifies stabilizer codes by the set of diagonal Clifford gates that can be implemented transversally on them. We show that, for any stabilizer code, its group of diagonal transversal Clifford gates on $\ell$ code blocks must be one of six distinct families of matrix groups. We further develop the theory of classifying stabilizer codes by via matrix algebras of endomorphisms first introduced by Rains, and give a complete classification of the diagonal Clifford symmetries of $\ell$ code blocks. A number of corollaries are given in the final section.

quant-ph

Assuring the Safety of Reinforcement Learning Components: AMLAS-RL

The rapid advancement of machine learning (ML) has led to its increasing integration into cyber-physical systems (CPS) across diverse domains. While CPS offer powerful capabilities, incorporating ML components introduces significant safety and assurance challenges. Among ML techniques, reinforcement learning (RL) is particularly suited for CPS due to its capacity to handle complex, dynamic environments where explicit models of interaction between system and environment are unavailable or difficult to construct. However, in safety-critical applications, this learning process must not only be effective but demonstrably safe. Safe-RL methods aim to address this by incorporating safety constraints during learning, yet they fall short in providing systematic assurance across the RL lifecycle. The AMLAS methodology offers structured guidance for assuring the safety of supervised learning components, but it does not directly apply to the unique challenges posed by RL. In this paper, we adapt AMLAS to provide a framework for generating assurance arguments for an RL-enabled system through an iterative process; AMLAS-RL. We demonstrate AMLAS-RL using a running example of a wheeled vehicle tasked with reaching a target goal without collision.

cs.LG

Breaking even with magic: demonstration of a high-fidelity logical non-Clifford gate

Encoding quantum information to protect it from errors is essential for performing large-scale quantum computations. Performing a universal set of quantum gates on encoded states demands a potentially large resource overhead and minimizing this overhead is key for the practical development of large-scale fault-tolerant quantum computers. We propose and experimentally implement a magic-state preparation protocol to fault-tolerantly prepare a pair of logical magic states in a [[6,2,2]] quantum error-detecting code using only eight physical qubits. Implementing this protocol on H1-1, a 20 qubit trapped-ion quantum processor, we prepare magic states with experimental infidelity $7^{+3}_{-1}\times 10^{-5}$ with a $14.8^{+1}_{-1}\%$ discard rate and use these to perform a fault-tolerant non-Clifford gate, the controlled-Hadamard (CH), with logical infidelity $\leq 2.3^{+9}_{-9}\times 10^{-4}$. Notably, this significantly outperforms the unencoded physical CH infidelity of $10^{-3}$. Through circuit-level stabilizer simulations, we show that this protocol can be self-concatenated to produce extremely high-fidelity magic states with low space-time overhead in a [[36,4,4]] quantum error correcting code, with logical error rates of $6\times 10^{-10}$ ($5\times 10^{-14}$) at two-qubit error rate of $10^{-3}$ ($10^{-4}$) respectively.

quant-ph

Insights from Railway Professionals: Rethinking Railway assumptions regarding safety and autonomy

This study investigates how railway professionals perceive safety as a concept within rail, with the intention to help inform future technological developments within the industry. Through a series of interviews with drivers, route planners,and administrative personnel, the research explores the currentstate of safety practices, the potential for automation and the understanding of the railway as a system of systems. Key findings highlight a cautious attitude towards automation, a preference for assistive technologies, and a complex understanding of safety that integrates human, systematic and technological factors. The study also addresses the limitations of transferring automotive automation technologies to railways and the need for a railway-specific causation model to better evaluate and enhance safety in an evolving technological landscape. This study aims to bridge thegap between contemporary research and practical applications, contributing to the development of more effective safety metrics.

cs.HC

Emergence in Multi-Agent Systems: A Safety Perspective

Emergent effects can arise in multi-agent systems (MAS) where execution is decentralized and reliant on local information. These effects may range from minor deviations in behavior to catastrophic system failures. To formally define these effects, we identify misalignments between the global inherent specification (the true specification) and its local approximation (such as the configuration of different reward components or observations). Using established safety terminology, we develop a framework to understand these emergent effects. To showcase the resulting implications, we use two broadly configurable exemplary gridworld scenarios, where insufficient specification leads to unintended behavior deviations when derived independently. Recognizing that a global adaptation might not always be feasible, we propose adjusting the underlying parameterizations to mitigate these issues, thereby improving the system's alignment and reducing the risk of emergent failures.

cs.MA

Genons, Double Covers and Fault-tolerant Clifford Gates

A great deal of work has been done developing quantum codes with varying overhead and connectivity constraints. However, given the such an abundance of codes, there is a surprising shortage of fault-tolerant logical gates supported therein. We define a construction, such that given an input $[[n,k,d]]$ code, yields a $[[2n,2k,\ge d]]$ symplectic double code with naturally occurring fault-tolerant logical Clifford gates. As applied to 2-dimensional $D(\mathbb{Z}_2)$-topological codes with genons (twists) and domain walls, we find the symplectic double is genon free, and of possibly higher genus. Braiding of genons on the original code becomes Dehn twists on the symplectic double. Such topological operations are particularly suited for architectures with all-to-all connectivity, and we demonstrate this experimentally on Quantinuum's H1-1 trapped-ion quantum computer.

quant-ph

Safety Analysis of Autonomous Railway Systems: An Introduction to the SACRED Methodology

As the railway industry increasingly seeks to introduce autonomy and machine learning (ML), several questions arise. How can safety be assured for such systems and technologies? What is the applicability of current safety standards within this new technological landscape? What are the key metrics to classify a system as safe? Currently, safety analysis for the railway reflects the failure modes of existing technology; in contrast, the primary concern of analysis of automation is typically average performance. Such purely statistical approaches to measuring ML performance are limited, as they may overlook classes of situations that may occur rarely but in which the function performs consistently poorly. To combat these difficulties we introduce SACRED, a safety methodology for producing an initial safety case and determining important safety metrics for autonomous systems. The development of SACRED is motivated by the proposed GoA-4 light-rail system in Berlin.

cs.SE

Safeguarding Learning-based Control for Smart Energy Systems with Sampling Specifications

We study challenges using reinforcement learning in controlling energy systems, where apart from performance requirements, one has additional safety requirements such as avoiding blackouts. We detail how these safety requirements in real-time temporal logic can be strengthened via discretization into linear temporal logic (LTL), such that the satisfaction of the LTL formulae implies the satisfaction of the original safety requirements. The discretization enables advanced engineering methods such as synthesizing shields for safe reinforcement learning as well as formal verification, where for statistical model checking, the probabilistic guarantee acquired by LTL model checking forms a lower bound for the satisfaction of the original real-time safety requirements.

cs.SE

Categorified Path Calculus

Path calculus, or graphical linear algebra, is a string diagram calculus for the category of matrices over a base ring. It is the usual string diagram calculus for a symmetric monoidal category, where the monoidal product is the direct sum of matrices. We categorify this story to develop a surface diagram calculus for the bicategory of matrices over a base bimonoidal category. This yields a surface diagram calculus for any bimonoidal category by restricting to diagrams for 1x1 matrices. We show how additional structure on the base category, such as biproducts, duals and the dagger, adds structure to the resulting calculus. Applied to categorical quantum mechanics this yields a new graphical proof of the teleportation protocol.

quant-ph

CSS code surgery as a universal construction

We define code maps between Calderbank-Shor-Steane (CSS) codes using maps between chain complexes, and describe code surgery between such codes using a specific colimit in the category of chain complexes. As well as describing a surgery operation, this gives a general recipe for new codes. As an application we describe how to `merge' and `split' along a shared $\overline{X}$ or $\overline{Z}$ operator between arbitrary CSS codes in a fault-tolerant manner, so long as certain technical conditions concerning gauge fixing and code distance are satisfied. We prove that such merges and splits on LDPC codes yield codes which are themselves LDPC.

quant-ph

Facilitating Change Implementation for Continuous ML-Safety Assurance

We propose a method for deploying a safety-critical machine-learning component into continuously evolving environments where an increased degree of automation in the engineering process is desired. We associate semantic tags with the safety case argumentation and turn each piece of evidence into a quantitative metric or a logic formula. With proper tool support, the impact can be characterized by a query over the safety argumentation tree to highlight evidence turning invalid. The concept is exemplified using a vision-based emergency braking system of an autonomous guided vehicle for factory automation.

cs.SE

Fold-Transversal Clifford Gates for Quantum Codes

We generalize the concept of folding from surface codes to CSS codes by considering certain dualities within them. In particular, this gives a general method to implement logical operations in suitable LDPC quantum codes using transversal gates and qubit permutations only. To demonstrate our approach, we specifically consider a [[30, 8, 3]] hyperbolic quantum code called Bring's code. Further, we show that by restricting the logical subspace of Bring's code to four qubits, we can obtain the full Clifford group on that subspace.

quant-ph

Unaligned but Safe -- Formally Compensating Performance Limitations for Imprecise 2D Object Detection

In this paper, we consider the imperfection within machine learning-based 2D object detection and its impact on safety. We address a special sub-type of performance limitations: the prediction bounding box cannot be perfectly aligned with the ground truth, but the computed Intersection-over-Union metric is always larger than a given threshold. Under such type of performance limitation, we formally prove the minimum required bounding box enlargement factor to cover the ground truth. We then demonstrate that the factor can be mathematically adjusted to a smaller value, provided that the motion planner takes a fixed-length buffer in making its decisions. Finally, observing the difference between an empirically measured enlargement factor and our formally derived worst-case enlargement factor offers an interesting connection between the quantitative evidence (demonstrated by statistics) and the qualitative evidence (demonstrated by worst-case analysis).

cs.LG

Safe AI -- How is this Possible?

Ttraditional safety engineering is coming to a turning point moving from deterministic, non-evolving systems operating in well-defined contexts to increasingly autonomous and learning-enabled AI systems which are acting in largely unpredictable operating contexts. We outline some of underlying challenges of safe AI and suggest a rigorous engineering framework for minimizing uncertainty, thereby increasing confidence, up to tolerable levels, in the safe behavior of AI systems.

cs.AI

A causal model of safety assurance for machine learning

This paper proposes a framework based on a causal model of safety upon which effective safety assurance cases for ML-based applications can be built. In doing so, we build upon established principles of safety engineering as well as previous work on structuring assurance arguments for ML. The paper defines four categories of safety case evidence and a structured analysis approach within which these evidences can be effectively combined. Where appropriate, abstract formalisations of these contributions are used to illustrate the causalities they evaluate, their contributions to the safety argument and desirable properties of the evidences. Based on the proposed framework, progress in this area is re-evaluated and a set of future research directions proposed in order for tangible progress in this field to be made.

cs.SE

Logically Sound Arguments for the Effectiveness of ML Safety Measures

We investigate the issues of achieving sufficient rigor in the arguments for the safety of machine learning functions. By considering the known weaknesses of DNN-based 2D bounding box detection algorithms, we sharpen the metric of imprecise pedestrian localization by associating it with the safety goal. The sharpening leads to introducing a conservative post-processor after the standard non-max-suppression as a counter-measure. We then propose a semi-formal assurance case for arguing the effectiveness of the post-processor, which is further translated into formal proof obligations for demonstrating the soundness of the arguments. Applying theorem proving not only discovers the need to introduce missing claims and mathematical concepts but also reveals the limitation of Dempster-Shafer's rules used in semi-formal argumentation.

cs.LO