January 2023 - talks - lists.cs.princeton.edu

Charlie Murphy will present his FPO "Relational Verification of Distributed Systems via Weak Simulations” on Friday, January 27, 2023 at 11am in CS 402.
by Nicki Mahler 06 Jan '23

06 Jan '23

Charlie Murphy will present his FPO "Relational Verification of Distributed Systems via Weak Simulations” on Friday, January 27, 2023 at 11am in CS 402. The members of his committee are as follows: Advisor: Zachary Kincaid Readers: Aarti Gupta and Lennart Beringer Examiners: Wyatt Lloyd and David Walker A copy of his thesis will be available before the FPO upon request. Please email gradinfo(a)cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend his talk. Abstract: Distributed systems are notoriously hard to get right, even when based on existing protocols. This thesis explores the use of executable specifications for (semi-) automatic verification of distributed systems. Rather than proving a distributed system is correct with respect to a given temporal property, this thesis proposes instead verifying a distributed system implements a given distributed protocol via per-node simulation. To prove a distributed system implements a protocol this thesis defines (1) contextual simulation logic, (2) simulation synthesis, and (3) fine-grained strategy improvement. Contextual simulation logic is a relational Hoare logic that consists of a judgement called contextual simulation and a set of inference rules to prove a contextual simulation valid. A contextual simulation relates an implementation program to a specification program via divergence preserving weak simulation. The set of rules are defined using the structure of both programs and used to align the implementation and specification programs. Simulation synthesis is a semi-algorithm that may prove or refute the validity of a (per-node) contextual simulation. Simulation synthesis is based on the game semantics of contextual simulation. Simulation synthesis will (1) construct a complete well-labeled simulation unwinding (a finite representation of a winning strategy proving the validity of a contextual simulation), (2) a counter-strategy to simulation of finite duration (a winning strategy refuting the validity of a contextual simulation), or (3) diverge. To solve a simulation game---an infinite state game of infinite duration---simulation synthesis incrementally expands and solves a finite-horizon of the game. Finite-horizon games are solved by reduction to satisfiability of quantified linear integer arithmetic (LIA) formulas. Further, this thesis develops fine-grained strategy improvement a decision procedure for proving (or refuting) satisfiability of quantified LIA formulas based on the game-semantics of LIA formulas. This procedure produces a certificate (a winning strategy proving or refuting) satisfiability of a LIA Formula. This certificate is used to construct the (winning) strategy for the finite-horizon game.

1 0

Teague Tomesh will present his FPO entitled "Co-designing Quantum Computer Architectures and Algorithms to Bridge the Quantum Resource Gap" on Monday, January 23, 2023 at 11am in CS 105.
by Nicki Mahler 05 Jan '23

05 Jan '23

Teague Tomesh will present his FPO entitled "Co-designing Quantum Computer Architectures and Algorithms to Bridge the Quantum Resource Gap" on Monday, January 23, 2023 at 11am in CS 105. The members of Teague's committee are as follows: Examiners: Margaret Martonosi, Stephen Lyon, and Amit Levy Readers: Kyle Jamieson and Fred Chong (University of Chicago) A copy of his thesis will be available before the FPO upon request. Please email gradinfo(a)cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend his talk. Abstract follows below: Quantum computing is a new computational paradigm based on the laws of quantum physics that have been developed over the last century. Quantum computers (QCs) manipulate quantum states and exploit non-classical phenomena, such as superposition and entanglement, to perform computations. Given this computational model, many quantum algorithms have been developed which are theoretically capable of outperforming any classical computer for certain applications such as factoring large integers, optimization, and simulating highly entangled quantum systems. However, the quantum programs implementing these high impact applications are extremely resource demanding. Their time and space requirements outstrip the capabilities of current QC systems by many orders of magnitude. I refer to this mismatch between the resources demanded by applications and what is available on current hardware as the Quantum Resource Gap (QRG). This dissertation presents a strategy for overcoming the QRG by advocating for the design of domain-specific quantum accelerators. I discuss how this strategy may be pursued using quantum benchmarks and program profiling to identify matches between applications and architectures that are well suited to one another. Once a particular application-architecture match is found, the algorithm’s execution can be optimized with cross-layer, co-design techniques that incorporate relevant information from across the entire hardware-software stack. To demonstrate the advantages of this approach, I discuss three examples covering molecular simulation, data set clustering, and constrained combinatorial optimization applications.

1 0

Paul Krueger will present his FPO "Metacognition: toward a computational framework for improving our minds" on Wednesday, January 18, 2023 at 2:00 PM in CS 402.
by gradinfo＠cs.princeton.edu 05 Jan '23

05 Jan '23

Paul Krueger will present his FPO "Metacognition: toward a computational framework for improving our minds" on Wednesday, January 18, 2023 at 2:00 PM in CS 402. Location: CS 402 The members of Paul's committee are as follows: Examiners: Tom Griffiths (Adviser), Jonathan Cohen, Ryan Adams Readers: Karthik Narasimhan, Nathaniel Daw A copy of his thesis will be available upon request. Please email gradinfo(a)cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend his talk. Abstract follows below: In this dissertation I will show how reinforcement learning (RL) can be applied to the inner workings of cognition. The usual application of RL is to understand human behavior or build intelligent machines interacting in the external world. The same RL formalism can be inverted onto cognitive processes themselves, resulting in a normative account of how to explore and select mental computations, referred to as metacognitive RL. This framework can 1) be used to generate observable behavioral predictions, 2) provide a resource-rational benchmark for both assessing and improving cognition, and 3) motivate cognitive process models based on interacting RL systems. The formalism of metacognitive RL rests on meta-level Markov Decision Processes (meta-MDPs), which provide a general-purpose computational framework that can also make task-specific predictions. The first study applies the resource-rational framework to risky choice resulting in the identification of heuristics and accurate predictions about how people adapt their use of heuristics. The second study uses the same metacognitive RL framework to predict which structures of the environment will enhance metacognitive learning in humans during a planning task. In the third study, rather than manipulate the decision environment-which is often infeasible to do in the real-world-the metacognitive RL framework is used to produce feedback in the form of pseudorewards, resulting in faster metacognitive learning in a related planning task. Next, a new cooperative RL architecture is proposed. This approach also uses pseudorewards to promote learning, but rather than generate the pseudorewards from a computational model, it is proposed that they may be produced internally by a distinct RL system. The successful application of the metacognitive RL framework to understand and improve cognitive function depends critically on developing machine learning methods to solve these problems. In the final chapter, I briefly explore the application of a recently proposed machine learning method for solving meta-MDPs.

1 0