More Like this

1. Explaining Deep Adaptive Programs via Reward Decomposition

   Erwig, Martin; Fern, Alan; Murali, Magesh; Koul, Anurag (January 2018, IJCAI/ECAI Workshop on Explainable Artificial Intelligence)

   Adaptation Based Programming (ABP) allows programmers to employ "choice points" at program locations where they are uncertain about how to best code the program logic. Reinforcement learning (RL) is then used to automatically learn to make choice-point decisions to optimize the reward achieved by the program. In this paper, we consider a new approach to explaining the learned decisions of adaptive programs. The key idea is to include simple program annotations that define multiple semantically meaningful reward types, which compose to define the overall reward signal used for learning. Using these reward types we define the notion of reward difference explanations (RDXs), which aim to explain why at a choice point an alternative A was selected over another alternative B An RDX gives the difference in the predicted future reward of each type when selecting A versus B and then continuing to run the adaptive program. Significant differences can provide insight into why A was or was not preferred to B. We describe a SARSA-style learning algorithm for learning to optimize the choices at each choice point, while also learning side information for producing RDXs. We demonstrate this explanation approach through a case study in a synthetic domain, which shows the general promise of the approach and highlights future research questions. 

   more » « less
2. Adaptable Traces for Program Explanations

   https://doi.org/10.1007/978-3-030-89051-3_12  

   Bajaj, Divya; Erwig, Martin; Fedorin, Danila; Gay, Kai (January 2021, Asian Symposium on Programming Languages and Systems)

   Program traces are a sound basis for explaining the dynamic behavior of programs. Alas, program traces can grow big very quickly, even for small programs, which diminishes their value as explanations. In this paper we demonstrate how the systematic simplification of traces can yield succinct program explanations. Specifically, we introduce operations for transforming traces that facilitate the abstraction of details. The operations are the basis of a query language for the definition of trace filters that can adapt and simplify traces in a variety of ways. The generation of traces is governed by a variant of Call-By-Value semantics which specifically supports parsimony in trace representations. We show that our semantics is a conservative extension of Call-By-Value that can produce smaller traces and that the evaluation traces preserve the explanatory content of proof trees at a much smaller footprint. 

   more » « less
3. Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy

   https://doi.org/10.1145/3360598  

   Near, Joseph P.; Darais, David; Abuah, Chike; Stevens, Tim; Gaddamadugu, Pranav; Wang, Lun; Somani, Neel; Zhang, Mu; Sharma, Nikhil; Shan, Alex; et al (October 2019, Proceedings of the ACM on Programming Languages)

   null (Ed.)

   During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy. We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework. We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models. 

   more » « less
4. A Visual Notation for Succinct Program Traces

   https://doi.org/10.1109/VL/HCC51201.2021.9576441  

   Bajaj, Divya; Erwig, Martin; Fedorin, Danila; Gay, Kai (October 2021, IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC))

   Program traces are often used for explaining the dynamic behavior of programs. Unfortunately, program traces can grow quite big very quickly, even for small programs, which compromises their usefulness. In this paper we present a visual notation for program traces that supports their succinct representation, as well as their dynamic transformation through a structured query language. An evaluation on a set of standard examples shows that our representation can reduce the overall size of traces by more than 80\%, which suggests that our notation is an effective improvement over the use of plain traces in the explanation of dynamic program behavior. 

   more » « less
5. Migrating gradual types

   https://doi.org/10.1017/S0956796822000089  

   CAMPORA, JOHN PETER; CHEN, SHENG; ERWIG, MARTIN; WALKINGSHAW, ERIC (January 2022, Journal of Functional Programming)

   Abstract Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically typed to more statically typed or vice versa, gradual typing itself does not provide a way to facilitate this migration. This places the burden on programmers who have to manually add or remove type annotations. Besides the general challenge of adding type annotations to dynamically typed code, there are subtle interactions between these annotations in gradually typed code that exacerbate the situation. For example, to migrate a program to be as static as possible, in general, all possible combinations of adding or removing type annotations from parameters must be tried out and compared. In this paper, we address this problem by developing migrational typing , which efficiently types all possible ways of replacing dynamic types with fully static types for a gradually typed program. The typing result supports automatically migrating a program to be as static as possible or introducing the least number of dynamic types necessary to remove a type error. The approach can be extended to support user-defined criteria about which annotations to modify. We have implemented migrational typing and evaluated it on large programs. The results show that migrational typing scales linearly with the size of the program and takes only 2–4 times longer than plain gradual typing. 

   more » « less