Program Repair for Hyperproperties @SimonsInstituteTOC

Simons Institute | Program Repair for Hyperproperties @SimonsInstituteTOC | Uploaded 2 months ago | Updated 14 hours ago
Borzoo Bonakdarpour (Michigan State University)
https://simons.berkeley.edu/talks/borzoo-bonakdarpour-michigan-state-university-2024-07-01
Synthesis of Models and Systems

Hyperproperties are system properties that relate multiple computation traces. This class of properties includes popular information-flow security policies as well as consistency requirements in concurrent computing. We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. We first consider finite-state programs and rigorously analyze the complexity of repair for various fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures. We then switch to infinite-state programs and propose a repair algorithm based on symbolic execution, constraint generation, and syntax-guided synthesis (SyGuS) of repair expression. As a practical realization, we develop an iterative repair approach. Here, we search for a sequence of repairs that are closer and closer to the original program’s behavior. We implement our method in a prototype and report on encouraging experimental results using off-the-shelf SyGuS solvers.

AI and Emotions: opportunities and challenges (Virtual Talk)

Toward Optimal Semi-streaming Algorithm for (1+ε)-approximate Maximum Matching

Attractor decompositions in games and automata

Debugging genomic profiling experiments and predictive models with interpretation tools

A Theory of Multi-objective Machine Learning

$Large Scale Private Learning on Data Streams, and the BLTs Abhradeep Guha Thakurta (Google DeepMind) https://simons.berkeley.edu/talks/abhradeep-guha-thakurta-google-deepmind-2024-06-18 Extroverted Sublinear Algorithms In recent years, Differentially Private Follow the Regularized Leader (DP-FTRL) style algorithms have become increasingly popular for training large models over data streams, e.g., in training DP models for Gboard next-word prediction (https://research.google/blog/federated-learning-with-formal-differentia… and https://arxiv.org/abs/2305.18465). At the heart of these algorithms is a correlated noise addition mechanism that factorizes a square lower triangular matrix of all ones (A=BC) and adds noise BZ (with Z ~ N(0,σ^2)^{training steps x dimensions}) to the prefix sum of the gradients observed during training. Prior work required generating and storing the noise matrix in advance, which is prohibitively expensive for large-scale model training. In this talk, we introduce a new algorithmic construction called the Buffered Linear Toeplitz operator (BLT) that allows generating the noise required for DP in a streaming fashion while requiring a buffer size of approximately log^2(training steps) x dimensions. Furthermore, compared to the class of all Lower Triangular Toeplitz (LTT) factorizations (i.e., B and C being LTT), BLTs are only off by an additive constant in terms of utility under standard error metrics. The talk will draw ideas from rational function approximations and constant recurrence sequences for the construction of BLTs. The talk will also demonstrate the practicality of this work through simulation experiments. The talk is primarily based on https://arxiv.org/pdf/2404.16706, and is a joint work with Krishnamurthy (Dj) Dvijotham, Brendan McMahan, Krishna Pillutla, and Thomas Steinke.$

Space is a latent sequence: A theory of hippocampus and PFC

Massively Parallel Algorithms for High-Dimensional Euclidean Minimum Spanning Tree