Describing systems in terms of choices and their resulting costs and rewards offers the promise of freeing algorithm designers and programmers from specifying how those choices should be made; in implementations, the choices can be realized by optimization techniques and, increasingly, by machine-learning methods. We study this approach from a programming-language perspective. We define two small languages that support decision-making abstractions: one with choices and rewards, and the other additionally with probabilities. We give both operational and denotational semantics.In the case of the second language we consider three denotational semantics, with varying degrees of correlation between possible program values and expected rewards. The operational semantics combine the usual semantics of standard constructs with optimiza-tion over spaces of possible execution strategies. The denotational semantics, which are compositional, rely on the selection monad, to handle choice, augmented with an auxiliary monad to handle other effects, such as rewards or probability.We establish adequacy theorems that the two semantics coincide in all cases. We also prove full abstraction at base types, with varying notions of observation in the probabilistic case corresponding to the various degrees of correlation. We present axioms for choice combined with rewards and probability, establishing completeness at base types for the case of rewards without probability.

Federated learning with differential privacy, 001 i.e. private federated learning (PFL), makes it 002 possible to train models on private data dis-003 tributed across users’ devices without harming 004 privacy. However, it is only known how to do 005 this for models, such as neural networks, that 006 have a fixed number of parameters, and thus a 007 fixed-dimensional gradient vector. Such mod-008 els include neural-net language models, but 009 not n-gram language models or, indeed, tok-010 enizers, the topic of this work. Training a to-011 kenizer normally requires access to the train-012 ing data. An alternative is to train the to-013 kenizer on publicly available data, but this, 014 we show, degrades accuracy for a next-word 015 prediction task by 10–20 % across different 016 datasets and models. We propose to take a tok-017 enizer built on public data, use it to train a lan-018 guage model with PFL, and sample from the 019 language model to find a new tokenizer. Re-020 training with the new tokenizer brings perfor-021 mance to within 2 % of the oracle tokenizer, 022 without expending additional privacy budget. 023 Finally, we build a new federated pipeline to 024 update the tokenizer during model training by 025 modifying affected model embeddings. 026

We present a new model for rollback recovery in distributed dataflow systems. We explain existing rollback schemes by assigning a logical time to each event such as a message delivery. If some processors fail during an execution, the system rolls back by selecting a set of logical times for each processor. The effect of events at times within the set is retained or restored from saved state, while the effect of other events is undone and re-executed. We show that, by adopting different logical time domains at different processors, an application can adopt appropriate checkpointing schemes for different parts of its computation. We illustrate with an example of an application that combines batch processing with low-latency streaming updates. We show rules, and an algorithm, to determine a globally consistent state for rollback in a system that uses multiple logical time domains. We also introduce selective rollback at a processor, which can selectively preserve the effect of events at some logical times and not others, independent of the original order of execution of those events. Selective rollback permits new checkpointing policies that are particularly well suited to iterative streaming algorithms. We report on an implementation of our new framework in the context of the Naiad system.

Automatic differentiation plays a prominent role in scientific computing and in modern machine learning, often in the context of powerful programming systems. The relation of the various embodiments of automatic differentiation to the mathematical notion of derivative is not always entirely clear---discrepancies can arise, sometimes inadvertently. In order to study automatic differentiation in such programming contexts, we define a small but expressive programming language that includes a construct for reverse-mode differentiation. We give operational and denotational semantics for this language. The operational semantics employs popular implementation techniques, while the denotational semantics employs notions of differentiation familiar from real analysis. We establish that these semantics coincide.

Differentiable programming allows programmers to calculate program gradients and unlocks experimentation with new optimizers and neural network architectures. This is why modern deep learning frameworks [1, 23, 20, 7] introduce derivative APIs (e.g. tf.gradients in TensorFlow). Programmers ask for the gradient of an objective function with respect to its parameters; which is then used to optimize these parameters, e.g. through stochastic gradient descent. Recent projects, as Swift for TensorFlow (S4TF) (www.tensorflow.org/swift) and Julia Zygote [15], in the spirit of the seminal “Lambda the Ultimate Backpropagator” (LTUB) [21], advocate AD as a first-class construct in a general-purpose programming language, and aim to take advantage of traditional compiler optimizations for efficient code generation. The idea is to produce statically, for every differentiable function of type a → b, another function returning the result of the original function and a linear back-propagator map, of type a → (b, Tan b −◦ Tan a). We call these compiler-generated functions the representation functions (rep-functions for short) of differentiable functions, and will use a b as a type abbreviation for a → (b, Tan b −◦ Tan a). To achieve this, the AD pass merely composes rep-functions out of primitive rep-functions like those for (+) and (−), by systematically lifting these primitives through the constructs of the programming language. An important challenge in this setting is the differentiation of functions that accept or return other functions, perhaps capturing (differentiable or nondifferentiable) variables. Partial applications must not “forget” to back-propagate to captured variables, and more generally we need AD that provably preserves equational reasoning – needed to justify inlining, common sub-expression elimination etc. As we will see (Section 2), higher-order functions are ubiquitous in modern statically-typed languages, even inside the implementation of end-to-end first-order programs. They have to be tackled heads-on to avoid additional complications in a compiler, such as extra inlining and loop unrolling or early defunctionalization, and to allow for separate compilation, to name a few. This is the challenge we address. We focus on (i) statically-typed, (ii) compile-time, (ii) reverse-mode AD, a scenario exemplified by Swift AD. (http://bit. ly/swift-autodiff) Our contributions are:

In einem Verfahren zum Steuern einer gemeinsamen Nutzung eines Objekts unter Entitaten in einem verteilten System wird ein Prozessor ein Objekt identifizieren und eine Zugriffssteuerungsliste (ACL) fur das Objekt so erzeugen, dass die ACL eine Liste von Klauseln umfasst. Jede Klausel wird ein Segnungsmuster umfassen, das mit einer oder mehreren Segnungen ubereinstimmt, und eine oder mehrere Klauseln konnen zudem einen Verweis auf eine oder mehrere Gruppen umfassen. Jede Gruppe reprasentiert eine Menge von Zeichenfolgen, die Segnungsmuster oder Fragmente von Segnungsmustern reprasentieren. Der Prozessor kann jede Klausel der ACL entweder als Erlaubnisklausel oder Verweigerungsklausel erzeugen, um anzugeben, ob es einer Entitat oder Entitaten, die eine Segnung aufweisen, die mit dem Segnungsmuster ubereinstimmt, erlaubt ist, auf das Objekt zuzugreifen. Der Prozessor wird die ACL in einem Datenspeicher speichern, und zwar zur Verwendung beim Antworten auf eine Anforderung, auf das Objekt zuzugreifen.

We study the interaction of the programming construct "new," which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. We define the applied pi calculus, a simple, general extension of the pi calculus in which values can be formed from names via the application of built-in functions, subject to equations, and be sent as messages. (In contrast, the pure pi calculus lacks built-in functions; its only messages are atomic names.) We develop semantics and proof techniques for this extended language and apply them in reasoning about security protocols. This article essentially subsumes the conference paper that introduced the applied pi calculus in 2001. It fills gaps, incorporates improvements, and further explains and studies the applied pi calculus. Since 2001, the applied pi calculus has been the basis for much further work, described in many research publications and sometimes embodied in useful software, such as the tool ProVerif, which relies on the applied pi calculus to support the specification and automatic analysis of security protocols. Although this article does not aim to be a complete review of the subject, it benefits from that further work and provides better foundations for some of it. In particular, the applied pi calculus has evolved through its implementation in ProVerif, and the present definition reflects that evolution.

We use neural guidance to direct search of the DPLL algorithm. We compare SAT-solving performance of various heuristics and two neural architectures: LSTM and a message-passing architecture. By a large margin the best one is the message passing architecture, which has more desirable theoretical properties and which is capable of solving complicated instances of SAT problems even when used with a naive implementation of the DPLL algorithm.

Many recent machine learning models rely on fine-grained dynamic control flow for training and inference. In particular, models based on recurrent neural networks and on reinforcement learning depend on recurrence relations, data-dependent conditional execution, and other features that call for dynamic control flow. These applications benefit from the ability to make rapid control-flow decisions across a set of computing devices in a distributed system. For performance, scalability, and expressiveness, a machine learning system must support dynamic control flow in distributed and heterogeneous environments. This paper presents a programming model for distributed machine learning that supports dynamic control flow. We describe the design of the programming model, and its implementation in TensorFlow, a distributed machine learning system. Our approach extends the use of dataflow graphs to represent machine learning models, offering several distinctive features. First, the branches of conditionals and bodies of loops can be partitioned across many machines to run on a set of heterogeneous devices, including CPUs, GPUs, and custom ASICs. Second, programs written in our model support automatic differentiation and distributed gradient computations, which are necessary for training machine learning models that use control flow. Third, our choice of non-strict semantics enables multiple loop iterations to execute in parallel across machines, and to overlap compute and I/O operations. We have done our work in the context of TensorFlow, and it has been used extensively in research and production. We evaluate it using several real-world applications, and demonstrate its performance and scalability.

Born in the late 70s, Abstract Interpretation has proven an effective method to construct static analyzers. It has led to successful program analysis tools routinely used in avionic, automotive, and space industries to help ensuring the correctness of mission-critical software. This tutorial presents Abstract Interpretation and its use to create static analyzers that infer numeric invariants on programs. We first present the theoretical bases of Abstract Interpretation: how to assign a well-defined formal semantics to programs, construct computable approximations to derive effective analyzers, and ensure soundness, i.e., any property derived by the analyzer is true of all actual executions — although some properties may be missed due to approximations, a necessary compromise to keep the analysis automatic, sound, and terminating when inferring uncomputable properties. We describe the classic numeric abstractions readily available to an analysis designer: intervals, polyhedra, congruences, octagons, etc., as well as domain combiners: the reduced product and various disjunctive completions. This tutorial focuses not only on the semantic aspect, but also on the algorithmic one, providing a description of the data-structures and algorithms necessary to effectively implement all our abstractions. We will encounter many trade-offs between cost on the one hand, and precision and expressiveness on the other hand. Invariant inference is formalized on an idealized, toy-language, manipulating perfect numbers, but the principles and algorithms we present are effectively used in analyzers for real industrial programs, although this is out of the scope of this tutorial. This tutorial is intended as an entry course in Abstract Interpretation, after which the reader should be ready to read the research literature on current advances in Abstract Interpretation and on the design of static analyzers for real languages. A. Miné. Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. Foundations and Trends © in Programming Languages, vol. 4, no. 3-4, pp. 120–372, 2017. DOI: 10.1561/2500000034. Full text available at: http://dx.doi.org/10.1561/2500000034

Some machine learning applications involve training data that is sensitive, such as the medical histories of patients in a clinical trial. A model may inadvertently and implicitly store some of its training data; careful analysis of the model may therefore reveal sensitive information. To address this problem, we demonstrate a generally applicable approach to providing strong privacy guarantees for training data: Private Aggregation of Teacher Ensembles (PATE). The approach combines, in a black-box fashion, multiple models trained with disjoint datasets, such as records from different subsets of users. Because they rely directly on sensitive data, these models are not published, but instead used as "teachers" for a "student" model. The student learns to predict an output chosen by noisy voting among all of the teachers, and cannot directly access an individual teacher or the underlying data or parameters. The student's privacy properties can be understood both intuitively (since no single teacher and thus no single dataset dictates the student's training) and formally, in terms of differential privacy. These properties hold even if an adversary can not only query the student but also inspect its internal workings. Compared with previous work, the approach imposes only weak assumptions on how teachers are trained: it applies to any model, including non-convex models like DNNs. We achieve state-of-the-art privacy/utility trade-offs on MNIST and SVHN thanks to an improved privacy analysis and semi-supervised learning.

Learning a natural language interface for database tables is a challenging task that involves deep language understanding and multi-step reasoning. The task is often approached by mapping natural language queries to logical forms or programs that provide the desired response when executed on the database. To our knowledge, this paper presents the first weakly supervised, end-to-end neural network model to induce such programs on a real-world dataset. We enhance the objective function of Neural Programmer, a neural network with built-in discrete operations, and apply it on WikiTableQuestions, a natural language question-answering dataset. The model is trained end-to-end with weak supervision of question-answer pairs, and does not require domain-specific grammars, rules, or annotations that are key elements in previous approaches to program induction. The main experimental result in this paper is that a single Neural Programmer model achieves 34.2% accuracy using only 10,000 examples with weak supervision. An ensemble of 15 models, with a trivial combination technique, achieves 37.7% accuracy, which is competitive to the current state-of-the-art accuracy of 37.1% obtained by a traditional natural language semantic parser.

TensorFlow is a powerful, programmable system for machine learning. This paper aims to provide the basics of a conceptual framework for understanding the behavior of TensorFlow models during training and inference: it describes an operational semantics, of the kind common in the literature on programming languages. More broadly, the paper suggests that a programming-language perspective is fruitful in designing and in explaining systems such as TensorFlow.

We present a method to create universal, robust, targeted adversarial image patches in the real world. The patches are universal because they can be used to attack any scene, robust because they work under a wide variety of transformations, and targeted because they can cause a classifier to output any target class. These adversarial patches can be printed, added to any scene, photographed, and presented to image classifiers; even when the patches are small, they cause the classifiers to ignore the other items in the scene and report a chosen target class. To reproduce the results from the paper, our code is available at https://github.com/tensorflow/cleverhans/tree/master/examples/adversarial_patch

The recent, remarkable growth of machine learning has led to intense interest in the privacy of the data on which machine learning relies, and to new techniques for preserving privacy. However, older ideas about privacy may well remain valid and useful. This note reviews two recent works on privacy in the light of the wisdom of some of the early literature, in particular the principles distilled by Saltzer and Schroeder in the 1970s.

TensorFlow is an interface for expressing machine learning algorithms, and an implementation for executing such algorithms. A computation expressed using TensorFlow can be executed with little or no change on a wide variety of heterogeneous systems, ranging from mobile devices such as phones and tablets up to large-scale distributed systems of hundreds of machines and thousands of computational devices such as GPU cards. The system is flexible and can be used to express a wide variety of algorithms, including training and inference algorithms for deep neural network models, and it has been used for conducting research and for deploying machine learning systems into production across more than a dozen areas of computer science and other fields, including speech recognition, computer vision, robotics, information retrieval, natural language processing, geographic information extraction, and computational drug discovery. This paper describes the TensorFlow interface and an implementation of that interface that we have built at Google. The TensorFlow API and a reference implementation were released as an open-source package under the Apache 2.0 license in November, 2015 and are available at www.tensorflow.org.