Format results
Electric Multipole Insulators
Taylor Hughes University of Illinois Urbana-Champaign
Resource theories of communication
Hlér Kristjánsson Université de Montréal
Specification, Verification and Synthesis in Cyberphysical Systems
Ufuk Topcu (University of Texas at Austin)Towards Lorentzian quantum gravity via effective spin foams
Bianca Dittrich Perimeter Institute for Theoretical Physics
Minding the Gap: Lessons from LIGO-Virgo’s Biggest Black Holes
Maya Fishbach University of Toronto
Verification and Control of Partially Observable Probabilistic Systems
Gethin Norman (University of Glasgow)The infinite symmetries of black holes and other celestial stories
Laura Donnay SISSA International School for Advanced Studies
Games on Graphs: from Logic and Automata to Algorithms
Marcin Jurdziński (University of Warwick)Collisions of false-vacuum bubble walls in a quantum spin chain
Ashley Milsted California Institute of Technology
SAT-Solving
Armin Biere (Johannes Kepler University)This tutorial focuses on explaining the most important aspects of the search loop in modern SAT solvers. It is an online BBC talk, i.e., black board and code, switching between a virtual black board to explain details and reviewing and using code in an interleaved manner. The code part features the new SAT Satch developed from scratch for this particular occasion. It is now available at https://github.com/arminbiere/satch. We start with an introduction on encoding problems into conjunctive normal form, the input format of SAT solvers, and then delve into search based complete algorithms for SAT solving, from DPLL to CDCL and all its modern concepts, including the implication graph, decision heuristics (VSIDS and VMTF), restarts, as well as clause data base reduction, and then end with a closer look at clause and watching data structures and how they are updated during boolean constraint propagation.Electric Multipole Insulators
Taylor Hughes University of Illinois Urbana-Champaign
In this talk I will present a general framework to distinguish different classes of charge insulators based on whether or not they insulate or conduct higher multipole moments (dipole, quadrupole, etc.). This formalism applies to generic many-body systems that support multipolar conservation laws. Applications of this work provide a key link between recently discovered higher order topological phases and fracton phases of matter.
SAT-Centered Complexity Theory
Valentine Kabanets (Simon Fraser University)From the early 1970s until now, SAT has been the central problem in Complexity Theory, inspiring many research directions. In the tutorial, I hope to show why SAT is such a favorite with complexity theorists, by talking about classical and modern results that involve SAT or its close relatives. We'll talk about NP-completeness, polynomial-time hierarchy, interactive proofs, PCPs, as well as (circuit) lower bounds, Exponential-Time Hypothesis, and learning.Resource theories of communication
Hlér Kristjánsson Université de Montréal
A series of recent works has shown that placing communication channels in a coherent superposition of alternative configurations can boost their ability to transmit information. Instances of this phenomenon are the advantages arising from the use of communication devices in a superposition of alternative causal orders, and those arising from the transmission of information along a superposition of alternative trajectories. The relation among these advantages has been the subject of recent debate, with some authors claiming that the advantages of the superposition of orders could be reproduced, and even surpassed, by other forms of superpositions. To shed light on this debate, we develop a general framework of resource theories of communication. In this framework, the resources are communication devices, and the allowed operations are (a) the placement of communication devices between the communicating parties, and (b) the connection of communication devices with local devices in the parties' laboratories. The allowed operations are required to satisfy the minimal condition that they do not enable communication independently of the devices representing the initial resources. The resource-theoretic analysis reveals that the aforementioned criticisms on the superposition of causal orders were based on an uneven comparison between different types of quantum superpositions, exhibiting different operational features.
Ref. https://iopscience.iop.org/article/10.1088/1367-2630/ab8ef7
Specification, Verification and Synthesis in Cyberphysical Systems
Ufuk Topcu (University of Texas at Austin)Cyberphysical systems are roughly characterized as systems enabled by coordination between computational and physical components and resources. They appear in a vast range of applications. Most applications of cyberphysical systems are subject to strict requirements for---to name a few---safety, security, and privacy. Formal methods for specification, verification, and synthesis have the potential to provide the languages, tools, and discipline necessary to meet these strict requirements. On the other hand, this potential can be realized only through proper connections between formal methods and several other fields. This tutorial will provide an overview of the complications in the context of cyberphysical systems that may benefit---and have benefited---from formal methods. It will provide examples of problems whose solution heavily relies on formal methods: correct-by-construction synthesis of hierarchical control protocols; synthesis of strategies under limitations on information availability; and verifiability of learning-enabled components.Unreasonable effectiveness of methods from theoretical computer science in quantum many-body physics
Anurag Anshu Harvard University
A central challenge in quantum many-body physics is a characterization of properties of `natural' quantum states, such as the ground states and Gibbs states of a local hamiltonian. The area-law conjecture, which postulates a remarkably simple structure of entanglement in gapped ground states, has resisted a resolution based on information-theoretic methods. We discuss how the right set of insights may come, quite unexpectedly, from polynomial approximations to boolean functions. Towards this, we describe a 2D sub-volume law for frustration-free locally-gapped ground states and highlight a pathway that could lead to an area law. Similar polynomial approximations have consequences for entanglement in Gibbs states and lead to the first provably linear time algorithm to simulate Gibbs states in 1D. Next, we consider the task of learning a Hamiltonian from a Gibbs state, where many-body entanglement obstructs rigorous algorithms. Here, we find that the effects of entanglement can again be controlled using tools from computer science, namely, strong convexity and sufficient statistics.
Towards Lorentzian quantum gravity via effective spin foams
Bianca Dittrich Perimeter Institute for Theoretical Physics
Euclidean quantum gravity approaches have a long history but suffer from a number of severe issues. This gives a strong motivation to develop Lorentzian approaches. Spin foams constitute an important such approach, which incorporate a rigorously derived discrete area spectrum. I will explain how this discrete area spectrum is connected to the appearance of an anomaly, which explains the significance of the Barbero-Immirzi parameter and forces an extension of the quantum configuration space, to also include torsion degrees of freedom. This can be understood as a defining characteristic of the spin foam approach, and provides a pathway to an (experimental) falsification.
All these features are captured in the recently constructive effective spin foam model, which is much more amenable to numerical calculations than previous models. I will present numerical results that a) show that spin foams do impose the correct equations of motion b) highlight the influence of the anomaly and c) underline the difference to Euclidean quantum gravity. I will close with an outlook on the features that can be studied with a truly Lorentzian model, e.g. topology change.
Minding the Gap: Lessons from LIGO-Virgo’s Biggest Black Holes
Maya Fishbach University of Toronto
Models for black hole formation from stellar evolution predict the existence of a pair-instability supernova mass gap in the range ~50 to ~120 solar masses. The binary black holes of LIGO-Virgo's first two observing runs supported this prediction, showing evidence for a dearth of component black hole masses above 45 solar masses. Meanwhile, among the 30+ new observations from the third observing run, there are several black holes that appear to sit above the 45 solar mass limit. I will discuss how these unexpectedly massive black holes fit into our understanding of the binary black hole population. The data are consistent with several scenarios, including a mass distribution that evolves with redshift and the possibility that the most massive binary black hole, GW190521, straddles the mass gap, containing an intermediate-mass black hole heavier than 120 solar masses.
Verification and Control of Partially Observable Probabilistic Systems
Gethin Norman (University of Glasgow)In this talk I will outline automated techniques for the verification and control of partially observable probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. Quantitative properties of interest, relate to the probability of an event’s occurrence or the expected value of some reward measure. I will present techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. The approach is based on an integer discretisation of the model’s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however both lower and upper bounds on numerical results can be generated.The infinite symmetries of black holes and other celestial stories
Laura Donnay SISSA International School for Advanced Studies
In this talk, I will review the recent advances in the understanding of intriguing infinite-dimensional symmetries that emerge at the boundary of asymptotically flat spacetime and in the vicinity of black hole horizons. These symmetries play an important role in the description of many phenomena such as gravitational memory effects and scattering amplitudes, and have paved the way to a holographic description of gravity in asymptotically flat spacetimes in terms of correlators on the celestial sphere.
Games on Graphs: from Logic and Automata to Algorithms
Marcin Jurdziński (University of Warwick)Game theory has been forged in the 1944 book of von Neumann (a mathematician) and Morgenstern (an economist) as a way to reason rigorously about economic behaviour, but its methodologies have since also illuminated many areas of social, political, and natural sciences. More recently, it has also enjoyed fruitful cross-fertilization with Computer Science, yielding the vibrant areas of Algorithmic Game Theory and Algorithmic Mechanism Design. Less broadly known, but relevant to the Theoretical Foundations of Computer Systems program at Simons, are the game theoretic models that originate from set theory, logic, and automata. In this tutorial, we consider a very basic model of games on graphs. We then argue that this simple model is general enough to encompass a range of classic game-theoretic models, and that it can streamline or enable solutions of notable problems, for example: - Gale-Stewart games in set theory and Martin’s Borel determinacy theorem; - Church’s reactive synthesis problem and its solution by Buchi and Landweber; - Rabin’s tree theorem and its proof using positional determinacy; - Pnueli and Rosner’s temporal synthesis problem; - evaluating nested Knaster-Tarski fixpoints; - the complexity of pivoting rules in linear optimization and stochastic planning; - star height problem. The technical focus of this tutorial is on the algorithmic aspects of one relatively simple but influential graph game model called parity games. Building efficient parity game solvers is worthwhile because many model-checking, equivalence-checking, satisfiability, and synthesis problems boil down to solving a parity game. The problem has an intriguing computational complexity status: it is both in NP and in co-NP, and in PLS and PPAD, and hence unlikely to be complete for any of those complexity classes; no compelling evidence of hardness is known; and it is a long-standing open problem if it can be solved in polynomial time. A key parameter that measures the descriptive complexity of a parity game graph is the number of distinct priorities; for example, in games arising from nested Knaster-Tarski fixpoint expressions, it reflects the number of alternations between least and greatest fixpoints. All known algorithms for several decades have been exponential in the number of priorities, until 2017 when Calude, Jain, Khoussainov, Li, and Stephan made a breakthrough by showing that the problem is FPT and that there is a quasi-polynomial algorithm. In 2018, Lehtinen has proposed another parameter called the register number and has shown that parity games can be solved in time exponential in it. This refines the quasi-polynomial complexity obtained by Calude et al. because the register number of a finite game is at most logarithmic in its size. We argue that the register number coincides with another parameter called the Strahler number, which provides structural insights and allows to solve parity games efficiently using small Strahler-universal trees. We mention preliminary experimental evidence to support Lehtinen’s thesis that most parity games in the wild have very tiny register/Strahler numbers. This strengthens a popular belief that finding a polynomial-time algorithm is more vital in theory than in practice and it suggests practical ways of turning modern quasi-polynomial algorithms into competitive solvers.Collisions of false-vacuum bubble walls in a quantum spin chain
Ashley Milsted California Institute of Technology
We study the real-time dynamics of a small bubble of "false vacuum'' in a quantum spin chain near criticality, where the low-energy physics is described by a relativistic (1+1)-dimensional quantum field theory. Such a bubble can be thought of as a confined kink-antikink pair (a meson). We carefully construct bubbles so that particle production does not occur until the walls collide. To achieve this in the presence of strong correlations, we extend a Matrix Product State (MPS) ansatz for quasiparticle wavepackets [Van Damme et al., arXiv:1907.02474 (2019)] to the case of confined, topological quasiparticles. By choosing the wavepacket width and the bubble size appropriately, we avoid strong lattice effects and observe relativistic kink-antikink collisions. We use the MPS quasiparticle ansatz to identify scattering outcomes: In the Ising model, with transverse and longitudinal fields, we do not observe particle production despite nonintegrability (supporting recent numerical observations of nonthermalizing mesonic states). With additional interactions, we see production of confined and unconfined particle pairs. Although we simulated these low-energy, few-particle events with moderate resources, we observe significant growth of entanglement with energy and with the number of collisions, suggesting that increasing either will ultimately exhaust our methods. Quantum devices, in contrast, are not limited by entanglement production, and promise to allow us to go far beyond classical methods. We anticipate that kink-antikink scattering in 1+1 dimensions will be an instructive benchmark problem for relatively near-term quantum devices.