-
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Authors:
Alex Sanchez-Stern,
Abhishek Varghese,
Zhanna Kaufman,
Dylan Zhang,
Talia Ringer,
Yuriy Brun
Abstract:
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively…
▽ More
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 34% shorter proofs 29% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 30.3% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms.
△ Less
Submitted 12 September, 2024; v1 submitted 17 August, 2024;
originally announced August 2024.
-
Thinking Forward: Memory-Efficient Federated Finetuning of Language Models
Authors:
Kunjal Panchal,
Nisarg Parikh,
Sunav Choudhary,
Lijun Zhang,
Yuriy Brun,
Hui Guan
Abstract:
Finetuning large language models (LLMs) in federated learning (FL) settings has become increasingly important as it allows resource-constrained devices to finetune a model using private data. However, finetuning LLMs using backpropagation requires excessive memory (especially from intermediate activations) for resource-constrained devices. While Forward-mode Auto-Differentiation (AD) can significa…
▽ More
Finetuning large language models (LLMs) in federated learning (FL) settings has become increasingly important as it allows resource-constrained devices to finetune a model using private data. However, finetuning LLMs using backpropagation requires excessive memory (especially from intermediate activations) for resource-constrained devices. While Forward-mode Auto-Differentiation (AD) can significantly reduce memory footprint from activations, we observe that directly applying it to LLM finetuning results in slow convergence and poor accuracy. In this paper, we introduce Spry, an FL algorithm that splits trainable weights of an LLM among participating clients, such that each client computes gradients using forward-mode AD that are closer estimations of the true gradients. Spry achieves a low memory footprint, high accuracy, and fast convergence. We formally prove that the global gradients in Spry are unbiased estimators of true global gradients for homogeneous data distributions across clients, while heterogeneity increases bias of the estimates. We also derive Spry's convergence rate, showing that the gradients decrease inversely proportional to the number of FL rounds, indicating the convergence up to the limits of heterogeneity. Empirically, Spry reduces the memory footprint during training by 1.4-7.1x in contrast to backpropagation, while reaching comparable accuracy, across a wide range of language tasks, models, and FL settings. Spry reduces the convergence time by 1.2-20.3x and achieves 5.2-13.5% higher accuracy against zero-order methods. When finetuning Llama2-7B with LoRA, compared to the peak memory consumption of 33.9GB of backpropagation, Spry only consumes 6.2GB of peak memory. For OPT13B, the reduction is from 76.5GB to 10.8GB. Spry makes feasible previously impossible FL deployments on commodity edge devices. Our source code is available at https://github.com/Astuary/Spry.
△ Less
Submitted 22 October, 2024; v1 submitted 24 May, 2024;
originally announced May 2024.
-
Robust Image Watermarking using Stable Diffusion
Authors:
Lijun Zhang,
Xiao Liu,
Antoni Viros Martin,
Cindy Xiong Bearfield,
Yuriy Brun,
Hui Guan
Abstract:
Watermarking images is critical for tracking image provenance and claiming ownership. With the advent of generative models, such as stable diffusion, able to create fake but realistic images, watermarking has become particularly important, e.g., to make generated images reliably identifiable. Unfortunately, the very same stable diffusion technology can remove watermarks injected using existing met…
▽ More
Watermarking images is critical for tracking image provenance and claiming ownership. With the advent of generative models, such as stable diffusion, able to create fake but realistic images, watermarking has become particularly important, e.g., to make generated images reliably identifiable. Unfortunately, the very same stable diffusion technology can remove watermarks injected using existing methods. To address this problem, we present a ZoDiac, which uses a pre-trained stable diffusion model to inject a watermark into the trainable latent space, resulting in watermarks that can be reliably detected in the latent vector, even when attacked. We evaluate ZoDiac on three benchmarks, MS-COCO, DiffusionDB, and WikiArt, and find that ZoDiac is robust against state-of-the-art watermark attacks, with a watermark detection rate over 98% and a false positive rate below 6.4%, outperforming state-of-the-art watermarking methods. Our research demonstrates that stable diffusion is a promising approach to robust watermarking, able to withstand even stable-diffusion-based attacks.
△ Less
Submitted 8 January, 2024;
originally announced January 2024.
-
My Model is Unfair, Do People Even Care? Visual Design Affects Trust and Perceived Bias in Machine Learning
Authors:
Aimen Gaba,
Zhanna Kaufman,
Jason Chueng,
Marie Shvakel,
Kyle Wm. Hall,
Yuriy Brun,
Cindy Xiong Bearfield
Abstract:
Machine learning technology has become ubiquitous, but, unfortunately, often exhibits bias. As a consequence, disparate stakeholders need to interact with and make informed decisions about using machine learning models in everyday systems. Visualization technology can support stakeholders in understanding and evaluating trade-offs between, for example, accuracy and fairness of models. This paper a…
▽ More
Machine learning technology has become ubiquitous, but, unfortunately, often exhibits bias. As a consequence, disparate stakeholders need to interact with and make informed decisions about using machine learning models in everyday systems. Visualization technology can support stakeholders in understanding and evaluating trade-offs between, for example, accuracy and fairness of models. This paper aims to empirically answer "Can visualization design choices affect a stakeholder's perception of model bias, trust in a model, and willingness to adopt a model?" Through a series of controlled, crowd-sourced experiments with more than 1,500 participants, we identify a set of strategies people follow in deciding which models to trust. Our results show that men and women prioritize fairness and performance differently and that visual design choices significantly affect that prioritization. For example, women trust fairer models more often than men do, participants value fairness more when it is explained using text than as a bar chart, and being explicitly told a model is biased has a bigger impact than showing past biased performance. We test the generalizability of our results by comparing the effect of multiple textual and visual design choices and offer potential explanations of the cognitive mechanisms behind the difference in fairness perception and trust. Our research guides design considerations to support future work developing visualization systems for machine learning.
△ Less
Submitted 7 August, 2023;
originally announced August 2023.
-
Baldur: Whole-Proof Generation and Repair with Large Language Models
Authors:
Emily First,
Markus N. Rabe,
Talia Ringer,
Yuriy Brun
Abstract:
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time, and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verific…
▽ More
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time, and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verification: We use large language models, trained on natural language text and code and fine-tuned on proofs, to generate whole proofs for theorems at once, rather than one step at a time. We combine this proof generation model with a fine-tuned repair model to repair generated proofs, further increasing proving power. As its main contributions, this paper demonstrates for the first time that: (1) Whole-proof generation using transformers is possible and is as effective as search-based techniques without requiring costly search. (2) Giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair and further improves automated proof generation. (3) We establish a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs. In addition to empirically showing the effectiveness of whole-proof generation, repair, and added context, we show that Baldur improves on the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7% of the theorems. Together, Baldur and Thor can prove 65.7% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification.
△ Less
Submitted 15 March, 2023; v1 submitted 8 March, 2023;
originally announced March 2023.
-
Avgust: Automating Usage-Based Test Generation from Videos of App Executions
Authors:
Yixue Zhao,
Saghar Talebipour,
Kesina Baral,
Hyojae Park,
Leon Yee,
Safwat Ali Khan,
Yuriy Brun,
Nenad Medvidovic,
Kevin Moran
Abstract:
Writing and maintaining UI tests for mobile apps is a time-consuming and tedious task. While decades of research have produced automated approaches for UI test generation, these approaches typically focus on testing for crashes or maximizing code coverage. By contrast, recent research has shown that developers prefer usage-based tests, which center around specific uses of app features, to help sup…
▽ More
Writing and maintaining UI tests for mobile apps is a time-consuming and tedious task. While decades of research have produced automated approaches for UI test generation, these approaches typically focus on testing for crashes or maximizing code coverage. By contrast, recent research has shown that developers prefer usage-based tests, which center around specific uses of app features, to help support activities such as regression testing. Very few existing techniques support the generation of such tests, as doing so requires automating the difficult task of understanding the semantics of UI screens and user inputs. In this paper, we introduce Avgust, which automates key steps of generating usage-based tests. Avgust uses neural models for image understanding to process video recordings of app uses to synthesize an app-agnostic state-machine encoding of those uses. Then, Avgust uses this encoding to synthesize test cases for a new target app. We evaluate Avgust on 374 videos of common uses of 18 popular apps and show that 69% of the tests Avgust generates successfully execute the desired usage, and that Avgust's classifiers outperform the state of the art.
△ Less
Submitted 1 November, 2022; v1 submitted 6 September, 2022;
originally announced September 2022.
-
Enforcing Delayed-Impact Fairness Guarantees
Authors:
Aline Weber,
Blossom Metevier,
Yuriy Brun,
Philip S. Thomas,
Bruno Castro da Silva
Abstract:
Recent research has shown that seemingly fair machine learning models, when used to inform decisions that have an impact on peoples' lives or well-being (e.g., applications involving education, employment, and lending), can inadvertently increase social inequality in the long term. This is because prior fairness-aware algorithms only consider static fairness constraints, such as equal opportunity…
▽ More
Recent research has shown that seemingly fair machine learning models, when used to inform decisions that have an impact on peoples' lives or well-being (e.g., applications involving education, employment, and lending), can inadvertently increase social inequality in the long term. This is because prior fairness-aware algorithms only consider static fairness constraints, such as equal opportunity or demographic parity. However, enforcing constraints of this type may result in models that have negative long-term impact on disadvantaged individuals and communities. We introduce ELF (Enforcing Long-term Fairness), the first classification algorithm that provides high-confidence fairness guarantees in terms of long-term, or delayed, impact. We prove that the probability that ELF returns an unfair solution is less than a user-specified tolerance and that (under mild assumptions), given sufficient training data, ELF is able to find and return a fair solution if one exists. We show experimentally that our algorithm can successfully mitigate long-term unfairness.
△ Less
Submitted 24 August, 2022;
originally announced August 2022.
-
Passport: Improving Automated Formal Verification Using Identifiers
Authors:
Alex Sanchez-Stern,
Emily First,
Timothy Zhou,
Zhanna Kaufman,
Yuriy Brun,
Talia Ringer
Abstract:
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification, by learning from proof corpora to suggest proofs, have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain.…
▽ More
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification, by learning from proof corpora to suggest proofs, have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain. This richness comes from the stylistic conventions followed by communities of proof developers, together with the logical systems beneath proof assistants. However, this richness remains underexploited, with most work thus far focusing on architecture rather than making the most of the proof data.
In this paper, we develop Passport, a fully-automated proof-synthesis tool that systematically explores how to most effectively exploit one aspect of that proof data: identifiers. Passport enriches a predictive Coq model with three new encoding mechanisms for identifiers: category vocabulary indexing, subword sequence modeling, and path elaboration. We compare Passport to three existing base tools which Passport can enhance: ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29% more theorems than the best-performing of these base tools. Combining the three Passport-enhanced tools automatically proves 38% more theorems than the three base tools together, without Passport's enhancements. Finally, together, these base tools and Passport-enhanced tools prove 45% more theorems than the combined base tools without Passport's enhancements. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software.
△ Less
Submitted 2 August, 2022; v1 submitted 21 April, 2022;
originally announced April 2022.
-
Gradient corrections to the local density approximation in the one-dimensional Bose gas
Authors:
François Riggio,
Yannis Brun,
Dragi Karevski,
Alexandre Faribault,
Jérôme Dubail
Abstract:
The local density approximation (LDA) is the central technical tool in the modeling of quantum gases in trapping potentials. It consists in treating the gas as an assembly of independent mesoscopic fluid cells at equilibrium with a local chemical potential, and it is justified when the correlation length is larger than the size of the cells. The LDA is often regarded as a crude approximation, part…
▽ More
The local density approximation (LDA) is the central technical tool in the modeling of quantum gases in trapping potentials. It consists in treating the gas as an assembly of independent mesoscopic fluid cells at equilibrium with a local chemical potential, and it is justified when the correlation length is larger than the size of the cells. The LDA is often regarded as a crude approximation, particularly in the ground state of the one-dimensional (1D) Bose gas, { where the correlation length is "therefore said to be" infinite (in the sense that correlation functions decay as a power law).} Here we take another look at the LDA. The local density $ρ(x)$ is viewed as a functional of the trapping potential $V(x)$, to which one applies a gradient expansion. The zeroth order in that expansion is the LDA. The first-order correction in the gradient expansion vanishes due to reflection symmetry. At second order, there are two corrections proportional to $d^2V/dx^2$ and $(dV/dx)^2$, and we propose a method to determine the corresponding coefficients by a perturbative calculation in the Lieb-Liniger model. This leads to an expression for the coefficients in terms of matrix elements of the density operator, which can in principle be evaluated numerically for an arbitrary coupling constant; here we show how to efficiently evaluate the coefficient associated to the curvature of the potential $d^2V/dx^2$, which dominates the deviation to LDA near local minima or maxima of the trapping potential. Both coefficients are evaluated analytically in the limits of infinite repulsion (hard-core bosons) and small repulsion (quasi-condensate).} The corrected LDA density profiles are compared to DMRG calculations, with significant improvement compared to zeroth-order LDA.
△ Less
Submitted 15 November, 2022; v1 submitted 12 April, 2022;
originally announced April 2022.
-
Blindspots in Python and Java APIs Result in Vulnerable Code
Authors:
Yuriy Brun,
Tian Lin,
Jessie Elise Somerville,
Elisha Myers,
Natalie C. Ebner
Abstract:
Blindspots in APIs can cause software engineers to introduce vulnerabilities, but such blindspots are, unfortunately, common. We study the effect APIs with blindspots have on developers in two languages by replicating an 109-developer, 24-Java-API controlled experiment. Our replication applies to Python and involves 129 new developers and 22 new APIs. We find that using APIs with blindspots statis…
▽ More
Blindspots in APIs can cause software engineers to introduce vulnerabilities, but such blindspots are, unfortunately, common. We study the effect APIs with blindspots have on developers in two languages by replicating an 109-developer, 24-Java-API controlled experiment. Our replication applies to Python and involves 129 new developers and 22 new APIs. We find that using APIs with blindspots statistically significantly reduces the developers' ability to correctly reason about the APIs in both languages, but that the effect is more pronounced for Python. Interestingly, for Java, the effect increased with complexity of the code relying on the API, whereas for Python, the opposite was true. Whether the developers considered API uses to be more difficult, less clear, and less familiar did not have an effect on their ability to correctly reason about them. Developers with better long-term memory recall were more likely to correctly reason about APIs with blindspots, but short-term memory, processing speed, episodic memory, and memory span had no effect. Surprisingly, professional experience and expertice did not improve the developers' ability to reason about APIs with blindspots across both languages, with long-term professionals with many years of experience making mistakes as often as relative novices. Finally, personality traits did not significantly affect the Python developers' ability to reason about APIs with blindspots, but less extraverted and more open developers were better at reasoning about Java APIs with blindspots. Overall, our findings suggest that blindspots in APIs are a serious problem across languages, and that experience and education alone do not overcome that problem, suggesting that tools are needed to help developers recognize blindspots in APIs as they write code that uses those APIs.
△ Less
Submitted 10 March, 2021;
originally announced March 2021.
-
Fairkit, Fairkit, on the Wall, Who's the Fairest of Them All? Supporting Data Scientists in Training Fair Models
Authors:
Brittany Johnson,
Jesse Bartola,
Rico Angell,
Katherine Keith,
Sam Witty,
Stephen J. Giguere,
Yuriy Brun
Abstract:
Modern software relies heavily on data and machine learning, and affects decisions that shape our world. Unfortunately, recent studies have shown that because of biases in data, software systems frequently inject bias into their decisions, from producing better closed caption transcriptions of men's voices than of women's voices to overcharging people of color for financial loans. To address bias…
▽ More
Modern software relies heavily on data and machine learning, and affects decisions that shape our world. Unfortunately, recent studies have shown that because of biases in data, software systems frequently inject bias into their decisions, from producing better closed caption transcriptions of men's voices than of women's voices to overcharging people of color for financial loans. To address bias in machine learning, data scientists need tools that help them understand the trade-offs between model quality and fairness in their specific data domains. Toward that end, we present fairkit-learn, a toolkit for helping data scientists reason about and understand fairness. Fairkit-learn works with state-of-the-art machine learning tools and uses the same interfaces to ease adoption. It can evaluate thousands of models produced by multiple machine learning algorithms, hyperparameters, and data permutations, and compute and visualize a small Pareto-optimal set of models that describe the optimal trade-offs between fairness and quality. We evaluate fairkit-learn via a user study with 54 students, showing that students using fairkit-learn produce models that provide a better balance between fairness and quality than students using scikit-learn and IBM AI Fairness 360 toolkits. With fairkit-learn, users can select models that are up to 67% more fair and 10% more accurate than the models they are likely to train with scikit-learn.
△ Less
Submitted 17 December, 2020;
originally announced December 2020.
-
Better Automatic Program Repair by Using Bug Reports and Tests Together
Authors:
Manish Motwani,
Yuriy Brun
Abstract:
Automated program repair is already deployed in industry, but concerns remain about repair quality. Recent research has shown that one of the main reasons repair tools produce incorrect (but seemingly correct) patches is imperfect fault localization (FL). This paper demonstrates that combining information from natural-language bug reports and test executions when localizing faults can have a signi…
▽ More
Automated program repair is already deployed in industry, but concerns remain about repair quality. Recent research has shown that one of the main reasons repair tools produce incorrect (but seemingly correct) patches is imperfect fault localization (FL). This paper demonstrates that combining information from natural-language bug reports and test executions when localizing faults can have a significant positive impact on repair quality. For example, existing repair tools with such FL are able to correctly repair 7 defects in the Defects4J benchmark that no prior tools have repaired correctly. We develop, Blues, the first information-retrieval-based, statement-level FL technique that requires no training data. We further develop RAFL, the first unsupervised method for combining multiple FL techniques, which outperforms a supervised method. Using RAFL, we create SBIR by combining Blues with a spectrum-based (SBFL) technique. Evaluated on 815 real-world defects, SBIR consistently ranks buggy statements higher than its underlying techniques. We then modify three state-of-the-art repair tools, Arja, SequenceR, and SimFix, to use SBIR, SBFL, and Blues as their internal FL. We evaluate the quality of the produced patches on 689 real-world defects. Arja and SequenceR significantly benefit from SBIR: Arja using SBIR correctly repairs 28 defects, but only 21 using SBFL, and only 15 using Blues; SequenceR using SBIR correctly repairs 12 defects, but only 10 using SBFL, and only 4 using Blues. SimFix, (which has internal mechanisms to overcome poor FL), correctly repairs 30 defects using SBIR and SBFL, but only 13 using Blues. Our work is the first investigation of simultaneously using multiple software artifacts for automated program repair, and our promising findings suggest future research in this directions is likely to be fruitful.
△ Less
Submitted 6 February, 2023; v1 submitted 16 November, 2020;
originally announced November 2020.
-
Wasm/k: Delimited Continuations for WebAssembly
Authors:
Donald Pinckney,
Arjun Guha,
Yuriy Brun
Abstract:
WebAssembly is designed to be an alternative to JavaScript that is a safe, portable, and efficient compilation target for a variety of languages. The performance of high-level languages depends not only on the underlying performance of WebAssembly, but also on the quality of the generated WebAssembly code. In this paper, we identify several features of high-level languages that current approaches…
▽ More
WebAssembly is designed to be an alternative to JavaScript that is a safe, portable, and efficient compilation target for a variety of languages. The performance of high-level languages depends not only on the underlying performance of WebAssembly, but also on the quality of the generated WebAssembly code. In this paper, we identify several features of high-level languages that current approaches can only compile to WebAssembly by generating complex and inefficient code. We argue that these problems could be addressed if WebAssembly natively supported first-class continuations. We then present Wasm/k, which extends WebAssembly with delimited continuations. Wasm/k introduces no new value types, and thus does not require significant changes to the WebAssembly type system (validation). Wasm/k is safe, even in the presence of foreign function calls (e.g., to and from JavaScript). Finally, Wasm/k is amenable to efficient implementation: we implement Wasm/k as a local change to Wasmtime, an existing WebAssembly JIT. We evaluate Wasm/k by implementing C/k, which adds delimited continuations to C/C++. C/k uses Emscripten and its implementation serves as a case study on how to use Wasm/k in a compiler that targets WebAssembly. We present several case studies using C/k, and show that on implementing green threads, it can outperform the state-of-the-art approach Asyncify with an 18% improvement in performance and a 30% improvement in code size.
△ Less
Submitted 4 October, 2020;
originally announced October 2020.
-
Formal Foundations of Serverless Computing
Authors:
Abhinav Jangda,
Donald Pinckney,
Yuriy Brun,
Arjun Guha
Abstract:
Serverless computing (also known as functions as a service) is a new cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless functions, and the cloud platform transparently manages the operating system, resource allocation, load-balancing, and fault tolerance. When demand for the service spike…
▽ More
Serverless computing (also known as functions as a service) is a new cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless functions, and the cloud platform transparently manages the operating system, resource allocation, load-balancing, and fault tolerance. When demand for the service spikes, the platform automatically allocates additional hardware to the service and manages load-balancing; when demand falls, the platform silently deallocates idle resources; and when the platform detects a failure, it transparently retries affected requests. In 2014, Amazon Web Services introduced the first serverless platform, AWS Lambda, and similar abstractions are now available on all major cloud computing platforms.
Unfortunately, the serverless computing abstraction exposes several low-level operational details that make it hard for programmers to write and reason about their code. This paper sheds light on this problem by presenting $λ_Λ$, an operational semantics of the essence of serverless computing. Despite being a small (half a page) core calculus, $λ_Λ$ models all the low-level details that serverless functions can observe. To show that $λ_Λ$ is useful, we present three applications. First, to ease reasoning about code, we present a simplified naive semantics of serverless execution and precisely characterize when the naive semantics and $λ_Λ$ coincide. Second, we augment $λ_Λ$ with a key-value store to allow reasoning about stateful serverless functions. Third, since a handful of serverless platforms support serverless function composition, we show how to extend $λ_Λ$ with a composition language. We have implemented this composition language and show that it outperforms prior work.
△ Less
Submitted 4 October, 2020; v1 submitted 15 February, 2019;
originally announced February 2019.
-
Conformal field theory on top of a breathing one-dimensional gas of hard core bosons
Authors:
Paola Ruggiero,
Yannis Brun,
Jérome Dubail
Abstract:
The recent results of [J. Dubail, J.-M. Stéphan, J. Viti, P. Calabrese, Scipost Phys. 2, 002 (2017)], which aim at providing access to large scale correlation functions of inhomogeneous critical one-dimensional quantum systems -- e.g. a gas of hard core bosons in a trapping potential -- are extended to a dynamical situation: a breathing gas in a time-dependent harmonic trap. Hard core bosons in a…
▽ More
The recent results of [J. Dubail, J.-M. Stéphan, J. Viti, P. Calabrese, Scipost Phys. 2, 002 (2017)], which aim at providing access to large scale correlation functions of inhomogeneous critical one-dimensional quantum systems -- e.g. a gas of hard core bosons in a trapping potential -- are extended to a dynamical situation: a breathing gas in a time-dependent harmonic trap. Hard core bosons in a time-dependent harmonic potential are well known to be exactly solvable, and can thus be used as a benchmark for the approach. An extensive discussion of the approach and of its relation with classical and quantum hydrodynamics in one dimension is given, and new formulas for correlation functions, not easily obtainable by other methods, are derived. In particular, a remarkable formula for the large scale asymptotics of the bosonic $n$-particle function $\left< Ψ^\dagger (x_1,t_1) \dots Ψ^\dagger (x_n,t_n) Ψ(x_1',t_1') \dots Ψ(x_n',t_n') \right>$ is obtained. Numerical checks of the approach are carried out for the fermionic two-point function -- easier to access numerically in the microscopic model than the bosonic one -- with perfect agreement.
△ Less
Submitted 26 April, 2019; v1 submitted 23 January, 2019;
originally announced January 2019.
-
Causal Testing: Finding Defects' Root Causes
Authors:
Brittany Johnson,
Yuriy Brun,
Alexandra Meliou
Abstract:
Understanding the root cause of a defect is critical to isolating and repairing buggy behavior. We present Causal Testing, a new method of root-cause analysis that relies on the theory of counterfactual causality to identify a set of executions that likely hold key causal information necessary to understand and repair buggy behavior. Using the Defects4J benchmark, we find that Causal Testing could…
▽ More
Understanding the root cause of a defect is critical to isolating and repairing buggy behavior. We present Causal Testing, a new method of root-cause analysis that relies on the theory of counterfactual causality to identify a set of executions that likely hold key causal information necessary to understand and repair buggy behavior. Using the Defects4J benchmark, we find that Causal Testing could be applied to 71% of real-world defects, and for 77% of those, it can help developers identify the root cause of the defect. A controlled experiment with 37 developers shows that Causal Testing improves participants' ability to identify the cause of the defect from 80% of the time with standard testing tools to 86% of the time with Causal Testing. The participants report that Causal Testing provides useful information they cannot get using tools such as JUnit. Holmes, our prototype, open-source Eclipse plugin implementation of Causal Testing, is available at http://holmes.cs.umass.edu/.
△ Less
Submitted 18 February, 2020; v1 submitted 18 September, 2018;
originally announced September 2018.
-
The Inhomogeneous Gaussian Free Field, with application to ground state correlations of trapped 1d Bose gases
Authors:
Yannis Brun,
Jérôme Dubail
Abstract:
Motivated by the calculation of correlation functions in inhomogeneous one-dimensional (1d) quantum systems, the 2d Inhomogeneous Gaussian Free Field (IGFF) is studied and solved. The IGFF is defined in a domain $Ω\subset \mathbb{R}^2$ equipped with a conformal class of metrics $[{\rm g}]$ and with a real positive coupling constant $K: Ω\rightarrow \mathbb{R}_{>0}$ by the action…
▽ More
Motivated by the calculation of correlation functions in inhomogeneous one-dimensional (1d) quantum systems, the 2d Inhomogeneous Gaussian Free Field (IGFF) is studied and solved. The IGFF is defined in a domain $Ω\subset \mathbb{R}^2$ equipped with a conformal class of metrics $[{\rm g}]$ and with a real positive coupling constant $K: Ω\rightarrow \mathbb{R}_{>0}$ by the action $\mathcal{S}[h] = \frac{1}{8π} \int_Ω\frac{\sqrt{\rm g} d^2 {\rm x}}{K({\rm x})} \, {\rm g}^{i j} (\partial_i h)(\partial_j h)$. All correlations functions of the IGFF are expressible in terms of the Green's functions of generalized Poisson operators that are familiar from 2d electrostatics in media with spatially varying dielectric constants.
This formalism is then applied to the study of ground state correlations of the Lieb-Liniger gas trapped in an external potential $V(x)$. Relations with previous works on inhomogeneous Luttinger liquids are discussed. The main innovation here is in the identification of local observables $\hat{O} (x)$ in the microscopic model with their field theory counterparts $\partial_x h, e^{i h(x)}, e^{-i h(x)}$, etc., which involve non-universal coefficients that themselves depend on position --- a fact that, to the best of our knowledge, was overlooked in previous works on correlation functions of inhomogeneous Luttinger liquids ---, and that can be calculated thanks to Bethe Ansatz form factors formulae available for the homogeneous Lieb-Liniger model. Combining those position-dependent coefficients with the correlation functions of the IGFF, ground state correlation functions of the trapped gas are obtained. Numerical checks from DMRG are provided for density-density correlations and for the one-particle density matrix, showing excellent agreement.
△ Less
Submitted 16 May, 2018; v1 submitted 14 December, 2017;
originally announced December 2017.
-
Tortoise: Interactive System Configuration Repair
Authors:
Aaron Weiss,
Arjun Guha,
Yuriy Brun
Abstract:
System configuration languages provide powerful abstractions that simplify managing large-scale, networked systems. Thousands of organizations now use configuration languages, such as Puppet. However, specifications written in configuration languages can have bugs and the shell remains the simplest way to debug a misconfigured system. Unfortunately, it is unsafe to use the shell to fix problems wh…
▽ More
System configuration languages provide powerful abstractions that simplify managing large-scale, networked systems. Thousands of organizations now use configuration languages, such as Puppet. However, specifications written in configuration languages can have bugs and the shell remains the simplest way to debug a misconfigured system. Unfortunately, it is unsafe to use the shell to fix problems when a system configuration language is in use: a fix applied from the shell may cause the system to drift from the state specified by the configuration language. Thus, despite their advantages, configuration languages force system administrators to give up the simplicity and familiarity of the shell.
This paper presents a synthesis-based technique that allows administrators to use configuration languages and the shell in harmony. Administrators can fix errors using the shell and the technique automatically repairs the higher-level specification written in the configuration language. The approach (1) produces repairs that are consistent with the fix made using the shell; (2) produces repairs that are maintainable by minimizing edits made to the original specification; (3) ranks and presents multiple repairs when relevant; and (4) supports all shells the administrator may wish to use. We implement our technique for Puppet, a widely used system configuration language, and evaluate it on a suite of benchmarks under 42 repair scenarios. The top-ranked repair is selected by humans 76% of the time and the human-equivalent repair is ranked 1.31 on average.
△ Less
Submitted 15 September, 2017;
originally announced September 2017.
-
Fairness Testing: Testing Software for Discrimination
Authors:
Sainyam Galhotra,
Yuriy Brun,
Alexandra Meliou
Abstract:
This paper defines software fairness and discrimination and develops a testing-based method for measuring if and how much software discriminates, focusing on causality in discriminatory behavior. Evidence of software discrimination has been found in modern software systems that recommend criminal sentences, grant access to financial products, and determine who is allowed to participate in promotio…
▽ More
This paper defines software fairness and discrimination and develops a testing-based method for measuring if and how much software discriminates, focusing on causality in discriminatory behavior. Evidence of software discrimination has been found in modern software systems that recommend criminal sentences, grant access to financial products, and determine who is allowed to participate in promotions. Our approach, Themis, generates efficient test suites to measure discrimination. Given a schema describing valid system inputs, Themis generates discrimination tests automatically and does not require an oracle. We evaluate Themis on 20 software systems, 12 of which come from prior work with explicit focus on avoiding discrimination. We find that (1) Themis is effective at discovering software discrimination, (2) state-of-the-art techniques for removing discrimination from algorithms fail in many situations, at times discriminating against as much as 98% of an input subdomain, (3) Themis optimizations are effective at producing efficient test suites for measuring discrimination, and (4) Themis is more efficient on systems that exhibit more discrimination. We thus demonstrate that fairness testing is a critical aspect of the software development cycle in domains with possible discrimination and provide initial tools for measuring software discrimination.
△ Less
Submitted 10 September, 2017;
originally announced September 2017.
-
Effectiveness of Anonymization in Double-Blind Review
Authors:
Claire Le Goues,
Yuriy Brun,
Sven Apel,
Emery Berger,
Sarfraz Khurshid,
Yannis Smaragdakis
Abstract:
Double-blind review relies on the authors' ability and willingness to effectively anonymize their submissions. We explore anonymization effectiveness at ASE 2016, OOPSLA 2016, and PLDI 2016 by asking reviewers if they can guess author identities. We find that 74%-90% of reviews contain no correct guess and that reviewers who self-identify as experts on a paper's topic are more likely to attempt to…
▽ More
Double-blind review relies on the authors' ability and willingness to effectively anonymize their submissions. We explore anonymization effectiveness at ASE 2016, OOPSLA 2016, and PLDI 2016 by asking reviewers if they can guess author identities. We find that 74%-90% of reviews contain no correct guess and that reviewers who self-identify as experts on a paper's topic are more likely to attempt to guess, but no more likely to guess correctly. We present our findings, summarize the PC chairs' comments about administering double-blind review, discuss the advantages and disadvantages of revealing author identities part of the way through the process, and conclude by advocating for the continued use of double-blind review.
△ Less
Submitted 5 September, 2017;
originally announced September 2017.
-
One-particle density matrix of trapped one-dimensional impenetrable bosons from conformal invariance
Authors:
Yannis Brun,
Jérôme Dubail
Abstract:
The one-particle density matrix of the one-dimensional Tonks-Girardeau gas with inhomogeneous density profile is calculated, thanks to a recent observation that relates this system to a two-dimensional conformal field theory in curved space. The result is asymptotically exact in the limit of large particle density and small density variation, and holds for arbitrary trapping potentials. In the par…
▽ More
The one-particle density matrix of the one-dimensional Tonks-Girardeau gas with inhomogeneous density profile is calculated, thanks to a recent observation that relates this system to a two-dimensional conformal field theory in curved space. The result is asymptotically exact in the limit of large particle density and small density variation, and holds for arbitrary trapping potentials. In the particular case of a harmonic trap, we recover a formula obtained by Forrester et al. [Phys. Rev. A 67, 043607 (2003)] from a different method.
△ Less
Submitted 5 April, 2017; v1 submitted 9 January, 2017;
originally announced January 2017.