Showing 1–50 of 56 results for author: Rinard, M

Probabilistic Programming with Programmable Variational Inference

Authors: McCoy R. Becker, Alexander K. Lew, Xiaoyan Wang, Matin Ghavami, Mathieu Huot, Martin C. Rinard, Vikash K. Mansinghka

Abstract: Compared to the wide array of advanced Monte Carlo methods supported by modern probabilistic programming languages (PPLs), PPL support for variational inference (VI) is less developed: users are typically limited to a predefined selection of variational objectives and gradient estimators, which are implemented monolithically (and without formal correctness arguments) in PPL backends. In this paper… ▽ More Compared to the wide array of advanced Monte Carlo methods supported by modern probabilistic programming languages (PPLs), PPL support for variational inference (VI) is less developed: users are typically limited to a predefined selection of variational objectives and gradient estimators, which are implemented monolithically (and without formal correctness arguments) in PPL backends. In this paper, we propose a more modular approach to supporting variational inference in PPLs, based on compositional program transformation. In our approach, variational objectives are expressed as programs, that may employ first-class constructs for computing densities of and expected values under user-defined models and variational families. We then transform these programs systematically into unbiased gradient estimators for optimizing the objectives they define. Our design enables modular reasoning about many interacting concerns, including automatic differentiation, density accumulation, tracing, and the application of unbiased gradient estimation strategies. Additionally, relative to existing support for VI in PPLs, our design increases expressiveness along three axes: (1) it supports an open-ended set of user-defined variational objectives, rather than a fixed menu of options; (2) it supports a combinatorial space of gradient estimation strategies, many not automated by today's PPLs; and (3) it supports a broader class of models and variational families, because it supports constructs for approximate marginalization and normalization (previously introduced only for Monte Carlo inference). We implement our approach in an extension to the Gen probabilistic programming system (genjax.vi, implemented in JAX), and evaluate on several deep generative modeling tasks, showing minimal performance overhead vs. hand-coded implementations and performance competitive with well-established open-source PPLs. △ Less

Submitted 22 June, 2024; originally announced June 2024.

Journal ref: PLDI 2024

GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables

Authors: Mathieu Huot, Matin Ghavami, Alexander K. Lew, Ulrich Schaechtle, Cameron E. Freer, Zane Shelby, Martin C. Rinard, Feras A. Saad, Vikash K. Mansinghka

Abstract: This article presents GenSQL, a probabilistic programming system for querying probabilistic generative models of database tables. By augmenting SQL with only a few key primitives for querying probabilistic models, GenSQL enables complex Bayesian inference workflows to be concisely implemented. GenSQL's query planner rests on a unified programmatic interface for interacting with probabilistic model… ▽ More This article presents GenSQL, a probabilistic programming system for querying probabilistic generative models of database tables. By augmenting SQL with only a few key primitives for querying probabilistic models, GenSQL enables complex Bayesian inference workflows to be concisely implemented. GenSQL's query planner rests on a unified programmatic interface for interacting with probabilistic models of tabular data, which makes it possible to use models written in a variety of probabilistic programming languages that are tailored to specific workflows. Probabilistic models may be automatically learned via probabilistic program synthesis, hand-designed, or a combination of both. GenSQL is formalized using a novel type system and denotational semantics, which together enable us to establish proofs that precisely characterize its soundness guarantees. We evaluate our system on two case real-world studies -- an anomaly detection in clinical trials and conditional synthetic data generation for a virtual wet lab -- and show that GenSQL more accurately captures the complexity of the data as compared to common baselines. We also show that the declarative syntax in GenSQL is more concise and less error-prone as compared to several alternatives. Finally, GenSQL delivers a 1.7-6.8x speedup compared to its closest competitor on a representative benchmark set and runs in comparable time to hand-written code, in part due to its reusable optimizations and code specialization. △ Less

Submitted 21 June, 2024; originally announced June 2024.

Comments: 54 pages, 30 figures, 1 table, published at PLDI 2024

Limited-perception games

Authors: Kai Jia, Martin Rinard

Abstract: We study rational agents with different perception capabilities in strategic games. We focus on a class of one-shot limited-perception games. These games extend simultaneous-move normal-form games by presenting each player with an individualized perception of all players' payoff functions. The accuracy of a player's perception is determined by the player's capability level. Capability levels are c… ▽ More We study rational agents with different perception capabilities in strategic games. We focus on a class of one-shot limited-perception games. These games extend simultaneous-move normal-form games by presenting each player with an individualized perception of all players' payoff functions. The accuracy of a player's perception is determined by the player's capability level. Capability levels are countable and totally ordered, with a higher level corresponding to a more accurate perception. We study the rational behavior of players in these games and formalize relevant equilibria conditions. In contrast to equilibria in conventional bimatrix games, which can be represented by a pair of mixed strategies, in our limited perception games a higher-order response function captures how the lower-capability player uses their (less accurate) perception of the payoff function to reason about the (more accurate) possible perceptions of the higher-capability opponent. This response function characterizes, for each possible perception of the higher-capability player (from the perspective of the lower-capability player), the best response of the higher capability player for that perception. Since the domain of the response function can be exponentially large or even infinite, finding one equilibrium may be computationally intractable or even undecidable. Nevertheless, we show that for any $ε$, there exists an $ε$-equilibrium with a compact, tractable representation whose size is independent of the size of the response function's domain. We further identify classes of zero-sum limited-perception games in which finding an equilibrium becomes a (typically tractable) nonsmooth convex optimization problem. △ Less

Submitted 26 May, 2024; originally announced May 2024.

Randomness Requirements and Asymmetries in Nash Equilibria

Authors: Edan Orzech, Martin Rinard

Abstract: In general, Nash equilibria in normal-form games may require players to play (probabilistically) mixed strategies. We define a measure of the complexity of finite probability distributions and study the complexity required to play Nash equilibria in finite two player $n\times n$ games with rational payoffs. Our central results show that there exist games in which there is an exponential vs. linear… ▽ More In general, Nash equilibria in normal-form games may require players to play (probabilistically) mixed strategies. We define a measure of the complexity of finite probability distributions and study the complexity required to play Nash equilibria in finite two player $n\times n$ games with rational payoffs. Our central results show that there exist games in which there is an exponential vs. linear gap in the complexity of the mixed distributions that the two players play in the (unique) Nash equilibrium of these games. This gap induces asymmetries in the amounts of space required by the players to represent and sample from the corresponding distributions using known state-of-the-art sampling algorithms. We also establish exponential upper and lower bounds on the complexity of Nash equilibria in normal-form games. These results highlight (i) the nontriviality of the assumption that players can play any mixed strategy and (ii) the disparity in resources that players may require to play Nash equilibria in normal-form games. △ Less

Submitted 11 May, 2024; v1 submitted 28 December, 2023; originally announced December 2023.

TRAFS: A Nonsmooth Convex Optimization Algorithm with $\mathcal{O}\left(\frac{1}ε\right)$ Iteration Complexity

Authors: Kai Jia, Martin Rinard

Abstract: We present the Trust Region Adversarial Functional Subdifferential (TRAFS) algorithm for constrained optimization of nonsmooth convex Lipschitz functions. Unlike previous methods that assume a subgradient oracle model, we work with the functional subdifferential defined as a set of subgradients that simultaneously captures sufficient local information for effective minimization while being easy to… ▽ More We present the Trust Region Adversarial Functional Subdifferential (TRAFS) algorithm for constrained optimization of nonsmooth convex Lipschitz functions. Unlike previous methods that assume a subgradient oracle model, we work with the functional subdifferential defined as a set of subgradients that simultaneously captures sufficient local information for effective minimization while being easy to compute for a wide range of functions. In each iteration, TRAFS finds the best step vector in an $\ell_2$-bounded trust region by considering the worst bound given by the functional subdifferential. TRAFS finds an approximate solution with an absolute error up to $ε$ in $\mathcal{O}\left( ε^{-1}\right)$ or $\mathcal{O}\left(ε^{-0.5} \right)$ iterations depending on whether the objective function is strongly convex, compared to the previously best-known bounds of $\mathcal{O}\left(ε^{-2}\right)$ and $\mathcal{O}\left(ε^{-1}\right)$ in these settings. TRAFS makes faster progress if the functional subdifferential satisfies a locally quadratic property; as a corollary, TRAFS achieves linear convergence (i.e., $\mathcal{O}\left(\log ε^{-1}\right)$) for strongly convex smooth functions. In the numerical experiments, TRAFS is on average 39.1x faster and solves twice as many problems compared to the second-best method. △ Less

Submitted 29 January, 2024; v1 submitted 10 November, 2023; originally announced November 2023.

Correlated vs. Uncorrelated Randomness in Adversarial Congestion Team Games

Authors: Edan Orzech, Martin Rinard

Abstract: We consider team zero-sum network congestion games with $n$ agents playing against $k$ interceptors over a graph $G$. The agents aim to minimize their collective cost of sending traffic over paths in $G$, which is an aggregation of edge costs, while the interceptors aim to maximize the collective cost by increasing some of these edge costs. To evade the interceptors, the agents will usually use ra… ▽ More We consider team zero-sum network congestion games with $n$ agents playing against $k$ interceptors over a graph $G$. The agents aim to minimize their collective cost of sending traffic over paths in $G$, which is an aggregation of edge costs, while the interceptors aim to maximize the collective cost by increasing some of these edge costs. To evade the interceptors, the agents will usually use randomized strategies. We consider two cases, the correlated case when agents have access to a shared source of randomness, and the uncorrelated case, when each agent has access to only its own source of randomness. We study the additional cost that uncorrelated agents have to bear, specifically by comparing the costs incurred by agents in cost-minimal Nash equilibria when agents can and cannot share randomness. We consider two natural cost functions on the agents, which measure the invested energy and time, respectively. We prove that for both of these cost functions, the ratio of uncorrelated cost to correlated cost at equilibrium is $O(\min(m_c(G),n))$, where $m_c(G)$ is the mincut size of $G$. This bound is much smaller than the most general case, where a tight, exponential bound of $Θ((m_c(G))^{n-1})$ on the ratio is known. We also introduce a set of simple agent strategies which are approximately optimal agent strategies. We then establish conditions for when these strategies are optimal agent strategies for each cost function, showing an inherent difference between the two cost functions we study. △ Less

Submitted 11 May, 2024; v1 submitted 15 August, 2023; originally announced August 2023.

Depth-bounded Epistemic Logic

Authors: Farid Arthaud, Martin Rinard

Abstract: Epistemic logics model how agents reason about their beliefs and the beliefs of other agents. Existing logics typically assume the ability of agents to reason perfectly about propositions of unbounded modal depth. We present DBEL, an extension of S5 that models agents that can reason about epistemic formulas only up to a specific modal depth. To support explicit reasoning about agent depths, DBEL… ▽ More Epistemic logics model how agents reason about their beliefs and the beliefs of other agents. Existing logics typically assume the ability of agents to reason perfectly about propositions of unbounded modal depth. We present DBEL, an extension of S5 that models agents that can reason about epistemic formulas only up to a specific modal depth. To support explicit reasoning about agent depths, DBEL includes depth atoms Ead (agent a has depth exactly d) and Pad (agent a has depth at least d). We provide a sound and complete axiomatization of DBEL. We extend DBEL to support public announcements for bounded depth agents and show how the resulting DPAL logic generalizes standard axioms from public announcement logic. We present two alternate extensions and identify two undesirable properties, amnesia and knowledge leakage, that these extensions have but DPAL does not. We provide axiomatizations of these logics as well as complexity results for satisfiability and model checking. Finally, we use these logics to illustrate how agents with bounded modal depth reason in the classical muddy children problem, including upper and lower bounds on the depth knowledge necessary for agents to successfully solve the problem. △ Less

Submitted 11 July, 2023; originally announced July 2023.

Comments: In Proceedings TARK 2023, arXiv:2307.04005

Report number: EPTCS 379-7 ACM Class: F.4.1; I.2.11

Journal ref: EPTCS 379, 2023, pp. 46-65

Sound Explanation for Trustworthy Machine Learning

Authors: Kai Jia, Pasapol Saowakon, Limor Appelbaum, Martin Rinard

Abstract: We take a formal approach to the explainability problem of machine learning systems. We argue against the practice of interpreting black-box models via attributing scores to input components due to inherently conflicting goals of attribution-based interpretation. We prove that no attribution algorithm satisfies specificity, additivity, completeness, and baseline invariance. We then formalize the c… ▽ More We take a formal approach to the explainability problem of machine learning systems. We argue against the practice of interpreting black-box models via attributing scores to input components due to inherently conflicting goals of attribution-based interpretation. We prove that no attribution algorithm satisfies specificity, additivity, completeness, and baseline invariance. We then formalize the concept, sound explanation, that has been informally adopted in prior work. A sound explanation entails providing sufficient information to causally explain the predictions made by a system. Finally, we present the application of feature selection as a sound explanation for cancer prediction models to cultivate trust among clinicians. △ Less

Submitted 8 June, 2023; originally announced June 2023.

Evidence of Meaning in Language Models Trained on Programs

Authors: Charles **, Martin Rinard

Abstract: We present evidence that language models can learn meaning despite being trained only to perform next token prediction on text, specifically a corpus of programs. Each program is preceded by a specification in the form of (textual) input-output examples. Working with programs enables us to precisely define concepts relevant to meaning in language (e.g., correctness and semantics), making program s… ▽ More We present evidence that language models can learn meaning despite being trained only to perform next token prediction on text, specifically a corpus of programs. Each program is preceded by a specification in the form of (textual) input-output examples. Working with programs enables us to precisely define concepts relevant to meaning in language (e.g., correctness and semantics), making program synthesis well-suited as an intermediate testbed for characterizing the presence (or absence) of meaning in language models. We first train a Transformer model on the corpus of programs, then probe the trained model's hidden states as it completes a program given a specification. Despite providing no inductive bias toward learning the semantics of the language, we find that a linear probe is able to extract abstractions of both current and future program states from the model states. Moreover, there is a strong, statistically significant correlation between the accuracy of the probe and the model's ability to generate a program that implements the specification. To evaluate whether the semantics are represented in the model states rather than learned by the probe, we design a novel experimental procedure that intervenes on the semantics of the language while preserving the lexicon and syntax. We also demonstrate that the model learns to generate correct programs that are, on average, shorter than those in the training set, which is evidence that language model outputs may differ from the training distribution in semantically meaningful ways. In summary, this paper does not propose any new techniques for training language models, but develops an experimental framework for and provides insights into the acquisition and representation of (formal) meaning in language models. △ Less

Submitted 24 May, 2023; v1 submitted 18 May, 2023; originally announced May 2023.

Depth-bounded epistemic logic

Authors: Farid Arthaud, Martin Rinard

Abstract: Epistemic logics model how agents reason about their beliefs and the beliefs of other agents. Existing logics typically assume the ability of agents to reason perfectly about propositions of unbounded modal depth. We present DBEL, an extension of S5 that models agents that can reason about epistemic formulas only up to a specific modal depth. To support explicit reasoning about agent depths, DBEL… ▽ More Epistemic logics model how agents reason about their beliefs and the beliefs of other agents. Existing logics typically assume the ability of agents to reason perfectly about propositions of unbounded modal depth. We present DBEL, an extension of S5 that models agents that can reason about epistemic formulas only up to a specific modal depth. To support explicit reasoning about agent depths, DBEL includes depth atoms $E_a^d$ (agent $a$ has depth exactly $d$) and $P_a^d$ (agent $a$ has depth at least $d$). We provide a sound and complete axiomatization of DBEL. We extend DBEL to support public announcements for bounded depth agents and show how the resulting DPAL logic generalizes standard axioms from public announcement logic. We present two alternate extensions and identify two undesirable properties, amnesia and knowledge leakage, that these extensions have but DPAL does not. We provide axiomatizations of these logics as well as complexity results for satisfiability and model checking. Finally, we use these logics to illustrate how agents with bounded modal depth reason in the classical muddy children problem, including upper and lower bounds on the depth knowledge necessary for agents to successfully solve the problem. △ Less

Submitted 15 May, 2023; originally announced May 2023.

Comments: 25 pages, 1 figure. To be published in TARK 2023 proceedings

Decentralized Inference via Capability Type Structures in Cooperative Multi-Agent Systems

Authors: Charles **, Zhang-Wei Hong, Farid Arthaud, Idan Orzech, Martin Rinard

Abstract: This work studies the problem of ad hoc teamwork in teams composed of agents with differing computational capabilities. We consider cooperative multi-player games in which each agent's policy is constrained by a private capability parameter, and agents with higher capabilities are able to simulate the behavior of agents with lower capabilities (but not vice-versa). To address this challenge, we pr… ▽ More This work studies the problem of ad hoc teamwork in teams composed of agents with differing computational capabilities. We consider cooperative multi-player games in which each agent's policy is constrained by a private capability parameter, and agents with higher capabilities are able to simulate the behavior of agents with lower capabilities (but not vice-versa). To address this challenge, we propose an algorithm that maintains a belief over the other agents' capabilities and incorporates this belief into the planning process. Our primary innovation is a novel framework based on capability type structures, which ensures that the belief updates remain consistent and informative without constructing the infinite hierarchy of beliefs. We also extend our techniques to settings where the agents' observations are subject to noise. We provide examples of games in which deviations in capability between oblivious agents can lead to arbitrarily poor outcomes, and experimentally validate that our capability-aware algorithm avoids the anti-cooperative behavior of the naive approach in these toy settings as well as a more complex cooperative checkers environment. △ Less

Submitted 27 April, 2023; originally announced April 2023.

Effective Neural Network $L_0$ Regularization With BinMask

Authors: Kai Jia, Martin Rinard

Abstract: $L_0$ regularization of neural networks is a fundamental problem. In addition to regularizing models for better generalizability, $L_0… ▽ More $L_0$ regularization of neural networks is a fundamental problem. In addition to regularizing models for better generalizability, $L_0$ regularization also applies to selecting input features and training sparse neural networks. There is a large body of research on related topics, some with quite complicated methods. In this paper, we show that a straightforward formulation, BinMask, which multiplies weights with deterministic binary masks and uses the identity straight-through estimator for backpropagation, is an effective $L_0$ regularizer. We evaluate BinMask on three tasks: feature selection, network sparsification, and model regularization. Despite its simplicity, BinMask achieves competitive performance on all the benchmarks without task-specific tuning compared to methods designed for each task. Our results suggest that decoupling weights from mask optimization, which has been widely adopted by previous work, is a key component for effective $L_0$ regularization. △ Less

Submitted 21 April, 2023; originally announced April 2023.

Emergence of Locally Suboptimal Behavior in Finitely Repeated Games

Authors: Yichen Yang, Martin Rinard

Abstract: We study the emergence of locally suboptimal behavior in finitely repeated games. Locally suboptimal behavior refers to players play suboptimally in some rounds of the repeated game (i.e., not maximizing their payoffs in those rounds) while maximizing their total payoffs in the whole repeated game. The central research question we aim to answer is when locally suboptimal behavior can arise from ra… ▽ More We study the emergence of locally suboptimal behavior in finitely repeated games. Locally suboptimal behavior refers to players play suboptimally in some rounds of the repeated game (i.e., not maximizing their payoffs in those rounds) while maximizing their total payoffs in the whole repeated game. The central research question we aim to answer is when locally suboptimal behavior can arise from rational play in finitely repeated games. In this research, we focus on the emergence of locally suboptimal behavior in subgame-perfect equilibria (SPE) of finitely repeated games with complete information. We prove the first sufficient and necessary condition on the stage game G that ensure that, for all T and all subgame-perfect equilibria of the repeated game G(T), the strategy profile at every round of G(T) forms a Nash equilibrium of the stage game G. We prove the sufficient and necessary conditions for three cases: 1) only pure strategies are allowed, 2) the general case where mixed strategies are allowed, and 3) one player can only use pure strategies and the other player can use mixed strategies. Based on these results, we obtain complete characterizations on when allowing players to play mixed strategies will change whether local suboptimality can ever occur in some repeated game. Furthermore, we present an algorithm for the computational problem of, given an arbitrary stage game, deciding if locally suboptimal behavior can arise in the corresponding finitely repeated games. This addresses the practical side of the research question. △ Less

Submitted 29 March, 2023; originally announced March 2023.

Mixed Capability Games

Authors: Kai Jia, Martin Rinard, Yichen Yang

Abstract: We present a new class of strategic games, mixed capability games, as a foundation for studying how different player capabilities impact the dynamics and outcomes of strategic games. We analyze the impact of different player capabilities via a capability transfer function that characterizes the payoff of each player at equilibrium given capabilities for all players in the game. In this paper, we m… ▽ More We present a new class of strategic games, mixed capability games, as a foundation for studying how different player capabilities impact the dynamics and outcomes of strategic games. We analyze the impact of different player capabilities via a capability transfer function that characterizes the payoff of each player at equilibrium given capabilities for all players in the game. In this paper, we model a player's capability as the size of the strategy space available to that player. We analyze a mixed capability variant of the Gold and Mines Game recently proposed by Yang et al. and derive its capability transfer function in closed form. △ Less

Submitted 15 August, 2022; v1 submitted 8 August, 2022; originally announced August 2022.

On the Impact of Player Capability on Congestion Games

Authors: Yichen Yang, Kai Jia, Martin Rinard

Abstract: We study the impact of player capability on social welfare in congestion games. We introduce a new game, the Distance-bounded Network Congestion game (DNC), as the basis of our study. DNC is a symmetric network congestion game with a bound on the number of edges each player can use. We show that DNC is PLS-complete in contrast to standard symmetric network congestion games which are in P. To model… ▽ More We study the impact of player capability on social welfare in congestion games. We introduce a new game, the Distance-bounded Network Congestion game (DNC), as the basis of our study. DNC is a symmetric network congestion game with a bound on the number of edges each player can use. We show that DNC is PLS-complete in contrast to standard symmetric network congestion games which are in P. To model different player capabilities, we propose using programs in a Domain-Specific Language (DSL) to compactly represent player strategies. We define a player's capability as the maximum size of the programs they can use. We introduce two variants of DNC with accompanying DSLs representing the strategy spaces. We propose four capability preference properties to characterize the impact of player capability on social welfare at equilibrium. We then establish necessary and sufficient conditions for the four properties in the context of our DNC variants. Finally, we study a specific game where we derive exact expressions of the social welfare in terms of the capability bound. This provides examples where the social welfare at equilibrium increases, stays the same, or decreases as players become more capable. △ Less

Submitted 23 August, 2022; v1 submitted 19 May, 2022; originally announced May 2022.

Searching for Replacement Classes

Authors: Malavika Samak, Jose Pablo Cambronero, Martin C. Rinard

Abstract: Software developers must often replace existing components in their systems to adapt to evolving environments or tooling. While traditional code search systems are effective at retrieving components with related functionality, it is much more challenging to retrieve components that can be used to directly replace existing functionality, as replacements must account for more fundamental program pro… ▽ More Software developers must often replace existing components in their systems to adapt to evolving environments or tooling. While traditional code search systems are effective at retrieving components with related functionality, it is much more challenging to retrieve components that can be used to directly replace existing functionality, as replacements must account for more fundamental program properties such as type compatibility. To address this problem, we introduce ClassFinder, a system which given a query class Q, and a search corpus S, returns a ranked subset of classes that can replace Q and its functionality. ClassFinder produces afield and method map** between the classes that can provide useful hints to a developer and can be used to effectively refine the ranking of candidate replacement classes. Our technique leverages the complementary strengths of a distributed embeddings-based search and type-based analysis, using the former to prune down candidates for an optimization-based approach based on the latter. ClassFinder retrieves replacement classes, along with a type-aware field/method map** between classes. We evaluate ClassFinder on a search space of ~600thousand open sourceJava classes. Querying ClassFinder with 24 known Java classes provided meaningful replacement classes and map**s, in many cases producing complete map**s with functionally identical replacement classes. △ Less

Submitted 11 October, 2021; originally announced October 2021.

Comments: 11 pages, 3 figures

Verifying Low-dimensional Input Neural Networks via Input Quantization

Authors: Kai Jia, Martin Rinard

Abstract: Deep neural networks are an attractive tool for compressing the control policy lookup tables in systems such as the Airborne Collision Avoidance System (ACAS). It is vital to ensure the safety of such neural controllers via verification techniques. The problem of analyzing ACAS Xu networks has motivated many successful neural network verifiers. These verifiers typically analyze the internal comput… ▽ More Deep neural networks are an attractive tool for compressing the control policy lookup tables in systems such as the Airborne Collision Avoidance System (ACAS). It is vital to ensure the safety of such neural controllers via verification techniques. The problem of analyzing ACAS Xu networks has motivated many successful neural network verifiers. These verifiers typically analyze the internal computation of neural networks to decide whether a property regarding the input/output holds. The intrinsic complexity of neural network computation renders such verifiers slow to run and vulnerable to floating-point error. This paper revisits the original problem of verifying ACAS Xu networks. The networks take low-dimensional sensory inputs with training data provided by a precomputed lookup table. We propose to prepend an input quantization layer to the network. Quantization allows efficient verification via input state enumeration, whose complexity is bounded by the size of the quantization space. Quantization is equivalent to nearest-neighbor interpolation at run time, which has been shown to provide acceptable accuracy for ACAS in simulation. Moreover, our technique can deliver exact verification results immune to floating-point error if we directly enumerate the network outputs on the target inference implementation or on an accurate simulation of the target implementation. △ Less

Submitted 17 August, 2021; originally announced August 2021.

Comments: SAS 2021

Incompatibility Clustering as a Defense Against Backdoor Poisoning Attacks

Authors: Charles **, Melinda Sun, Martin Rinard

Abstract: We propose a novel clustering mechanism based on an incompatibility property between subsets of data that emerges during model training. This mechanism partitions the dataset into subsets that generalize only to themselves, i.e., training on one subset does not improve performance on the other subsets. Leveraging the interaction between the dataset and the training process, our clustering mechanis… ▽ More We propose a novel clustering mechanism based on an incompatibility property between subsets of data that emerges during model training. This mechanism partitions the dataset into subsets that generalize only to themselves, i.e., training on one subset does not improve performance on the other subsets. Leveraging the interaction between the dataset and the training process, our clustering mechanism partitions datasets into clusters that are defined by--and therefore meaningful to--the objective of the training process. We apply our clustering mechanism to defend against data poisoning attacks, in which the attacker injects malicious poisoned data into the training dataset to affect the trained model's output. Our evaluation focuses on backdoor attacks against deep neural networks trained to perform image classification using the GTSRB and CIFAR-10 datasets. Our results show that (1) these attacks produce poisoned datasets in which the poisoned and clean data are incompatible and (2) our technique successfully identifies (and removes) the poisoned data. In an end-to-end evaluation, our defense reduces the attack success rate to below 1% on 134 out of 165 scenarios, with only a 2% drop in clean accuracy on CIFAR-10 and a negligible drop in clean accuracy on GTSRB. △ Less

Submitted 27 April, 2023; v1 submitted 8 May, 2021; originally announced May 2021.

Comments: ICLR 2023. Code is available at https://github.com/charles**/compatibility_clustering/

Inductive Program Synthesis over Noisy Datasets using Abstraction Refinement Based Optimization

Authors: Shivam Handa, Martin Rinard

Abstract: We present a new synthesis algorithm to solve program synthesis over noisy datasets, i.e., data that may contain incorrect/corrupted input-output examples. Our algorithm uses an abstraction refinement based optimization process to synthesize programs which optimize the tradeoff between the loss over the noisy dataset and the complexity of the synthesized program. The algorithm uses abstractions to… ▽ More We present a new synthesis algorithm to solve program synthesis over noisy datasets, i.e., data that may contain incorrect/corrupted input-output examples. Our algorithm uses an abstraction refinement based optimization process to synthesize programs which optimize the tradeoff between the loss over the noisy dataset and the complexity of the synthesized program. The algorithm uses abstractions to divide the search space of programs into subspaces by computing an abstract value that represents outputs for all programs in a subspace. The abstract value allows our algorithm to compute, for each subspace, a sound approximate lower bound of the loss over all programs in the subspace. It iteratively refines these abstractions to further subdivide the space into smaller subspaces, prune subspaces that do not contain an optimal program, and eventually synthesize an optimal program. We implemented this algorithm in a tool called Rose. We compare Rose to a current state-of-the-art noisy program synthesis system using the SyGuS 2018 benchmark suite. Our evaluation demonstrates that Rose significantly outperforms this previous system: on two noisy benchmark program synthesis problems sets drawn from the SyGus 2018 benchmark suite, Rose delivers speedups of up to 1587 and 81.7, with median speedups of 20.5 and 81.7. Rose also terminates on 20 (out of 54) and 4 (out of 11) more benchmark problems than the previous system. Both Rose and the previous system synthesize programs that are optimal over the provided noisy data sets. For the majority of the problems in the benchmark sets ($272$ out of $286$), the synthesized programs also produce correct outputs for all inputs in the original (unseen) noise-free data set. These results highlight the benefits that Rose can deliver for effective noisy program synthesis. △ Less

Submitted 27 April, 2021; originally announced April 2021.

Inferring Drop-in Binary Parsers from Program Executions

Authors: Thurston H. Y. Dang, Jose P. Cambronero, Martin C. Rinard

Abstract: We present BIEBER (Byte-IdEntical Binary parsER), the first system to model and regenerate a full working parser from instrumented program executions. To achieve this, BIEBER exploits the regularity (e.g., header fields and array-like data structures) that is commonly found in file formats. Key generalization steps derive strided loops that parse input file data and rewrite concrete loop bounds wi… ▽ More We present BIEBER (Byte-IdEntical Binary parsER), the first system to model and regenerate a full working parser from instrumented program executions. To achieve this, BIEBER exploits the regularity (e.g., header fields and array-like data structures) that is commonly found in file formats. Key generalization steps derive strided loops that parse input file data and rewrite concrete loop bounds with expressions over input file header bytes. These steps enable BIEBER to generalize parses of specific input files to obtain parsers that operate over input files of arbitrary size. BIEBER also incrementally and efficiently infers a decision tree that reads file header bytes to route input files of different types to inferred parsers of the appropriate type. The inferred parsers and decision tree are expressed in an IR; separate backends (C and Perl in our prototype) can translate the IR into the same language as the original program (for a safer drop-in replacement), or automatically port to a different language. An empirical evaluation shows that BIEBER can successfully regenerate parsers for six file formats (waveform audio [1654 files], MT76x0 .BIN firmware containers [5 files], OS/2 1.x bitmap images [9 files], Windows 3.x bitmaps [9971 files], Windows 95/NT4 bitmaps [133 files], and Windows 98/2000 bitmaps [859 files]), correctly parsing 100% (>= 99.98% when using standard held-out cross-validation) of the corresponding corpora. The regenerated parsers contain automatically inserted safety checks that eliminate common classes of errors such as memory errors. We find that BIEBER can help reverse-engineer file formats, because it automatically identifies predicates for the decision tree that relate to key semantics of the file format. We also discuss how BIEBER helped us detect and fix two new bugs in stb_image as well as independently rediscover and fix a known bug. △ Less

Submitted 19 April, 2021; originally announced April 2021.

Program Synthesis Over Noisy Data with Guarantees

Authors: Shivam Handa, Martin Rinard

Abstract: We explore and formalize the task of synthesizing programs over noisy data, i.e., data that may contain corrupted input-output examples. By formalizing the concept of a Noise Source, an Input Source, and a prior distribution over programs, we formalize the probabilistic process which constructs a noisy dataset. This formalism allows us to define the correctness of a synthesis algorithm, in terms o… ▽ More We explore and formalize the task of synthesizing programs over noisy data, i.e., data that may contain corrupted input-output examples. By formalizing the concept of a Noise Source, an Input Source, and a prior distribution over programs, we formalize the probabilistic process which constructs a noisy dataset. This formalism allows us to define the correctness of a synthesis algorithm, in terms of its ability to synthesize the hidden underlying program. The probability of a synthesis algorithm being correct depends upon the match between the Noise Source and the Loss Function used in the synthesis algorithm's optimization process. We formalize the concept of an optimal Loss Function given prior information about the Noise Source. We provide a technique to design optimal Loss Functions given perfect and imperfect information about the Noise Sources. We also formalize the concept and conditions required for convergence, i.e., conditions under which the probability that the synthesis algorithm produces a correct program increases as the size of the noisy data set increases. This paper presents the first formalization of the concept of optimal Loss Functions, the first closed form definition of optimal Loss Functions, and the first conditions that ensure that a noisy synthesis algorithm will have convergence guarantees. △ Less

Submitted 27 April, 2021; v1 submitted 8 March, 2021; originally announced March 2021.

Program Synthesis Guided Reinforcement Learning for Partially Observed Environments

Authors: Yichen David Yang, Jeevana Priya Inala, Osbert Bastani, Yewen Pu, Armando Solar-Lezama, Martin Rinard

Abstract: A key challenge for reinforcement learning is solving long-horizon planning problems. Recent work has leveraged programs to guide reinforcement learning in these settings. However, these approaches impose a high manual burden on the user since they must provide a guiding program for every new task. Partially observed environments further complicate the programming task because the program must imp… ▽ More A key challenge for reinforcement learning is solving long-horizon planning problems. Recent work has leveraged programs to guide reinforcement learning in these settings. However, these approaches impose a high manual burden on the user since they must provide a guiding program for every new task. Partially observed environments further complicate the programming task because the program must implement a strategy that correctly, and ideally optimally, handles every possible configuration of the hidden regions of the environment. We propose a new approach, model predictive program synthesis (MPPS), that uses program synthesis to automatically generate the guiding programs. It trains a generative model to predict the unobserved portions of the world, and then synthesizes a program based on samples from this model in a way that is robust to its uncertainty. In our experiments, we show that our approach significantly outperforms non-program-guided approaches on a set of challenging benchmarks, including a 2D Minecraft-inspired environment where the agent must complete a complex sequence of subtasks to achieve its goal, and achieves a similar performance as using handcrafted programs to guide the agent. Our results demonstrate that our approach can obtain the benefits of program-guided reinforcement learning without requiring the user to provide a new guiding program for every new task. △ Less

Submitted 1 November, 2021; v1 submitted 22 February, 2021; originally announced February 2021.

Journal ref: NeurIPS 2021

Neurosymbolic Transformers for Multi-Agent Communication

Authors: Jeevana Priya Inala, Yichen Yang, James Paulos, Yewen Pu, Osbert Bastani, Vijay Kumar, Martin Rinard, Armando Solar-Lezama

Abstract: We study the problem of inferring communication structures that can solve cooperative multi-agent planning problems while minimizing the amount of communication. We quantify the amount of communication as the maximum degree of the communication graph; this metric captures settings where agents have limited bandwidth. Minimizing communication is challenging due to the combinatorial nature of both t… ▽ More We study the problem of inferring communication structures that can solve cooperative multi-agent planning problems while minimizing the amount of communication. We quantify the amount of communication as the maximum degree of the communication graph; this metric captures settings where agents have limited bandwidth. Minimizing communication is challenging due to the combinatorial nature of both the decision space and the objective; for instance, we cannot solve this problem by training neural networks using gradient descent. We propose a novel algorithm that synthesizes a control policy that combines a programmatic communication policy used to generate the communication graph with a transformer policy network used to choose actions. Our algorithm first trains the transformer policy, which implicitly generates a "soft" communication graph; then, it synthesizes a programmatic communication policy that "hardens" this graph, forming a neurosymbolic transformer. Our experiments demonstrate how our approach can synthesize policies that generate low-degree communication graphs while maintaining near-optimal performance. △ Less

Submitted 4 January, 2021; originally announced January 2021.

Journal ref: NeurIPS 2020

Automatic Synthesis of Parallel Unix Commands and Pipelines with KumQuat

Authors: Jiasi Shen, Martin Rinard, Nikos Vasilakis

Abstract: We present KumQuat, a system for automatically generating data parallel implementations of Unix shell commands and pipelines. The generated parallel versions split input streams, execute multiple instantiations of the original pipeline commands to process the splits in parallel, then combine the resulting parallel outputs to produce the final output stream. KumQuat automatically synthesizes the co… ▽ More We present KumQuat, a system for automatically generating data parallel implementations of Unix shell commands and pipelines. The generated parallel versions split input streams, execute multiple instantiations of the original pipeline commands to process the splits in parallel, then combine the resulting parallel outputs to produce the final output stream. KumQuat automatically synthesizes the combine operators, with a domain-specific combiner language acting as a strong regularizer that promotes efficient inference of correct combiners. We evaluate KumQuat on 70 benchmark scripts that together have a total of 427 stages. KumQuat synthesizes a correct combiner for 113 of the 121 unique commands that appear in these benchmark scripts. The synthesis times vary between 39 seconds and 331 seconds with a median of 60 seconds. We present experimental results that show that these combiners enable the effective parallelization of our benchmark scripts. △ Less

Submitted 22 August, 2021; v1 submitted 30 December, 2020; originally announced December 2020.

An Order-Aware Dataflow Model for Parallel Unix Pipelines

Authors: Shivam Handa, Konstantinos Kallas, Nikos Vasilakis, Martin Rinard

Abstract: We present a dataflow model for modelling parallel Unix shell pipelines. To accurately capture the semantics of complex Unix pipelines, the dataflow model is order-aware, i.e., the order in which a node in the dataflow graph consumes inputs from different edges plays a central role in the semantics of the computation and therefore in the resulting parallelization. We use this model to capture the… ▽ More We present a dataflow model for modelling parallel Unix shell pipelines. To accurately capture the semantics of complex Unix pipelines, the dataflow model is order-aware, i.e., the order in which a node in the dataflow graph consumes inputs from different edges plays a central role in the semantics of the computation and therefore in the resulting parallelization. We use this model to capture the semantics of transformations that exploit data parallelism available in Unix shell computations and prove their correctness. We additionally formalize the translations from the Unix shell to the dataflow model and from the dataflow model back to a parallel shell script. We implement our model and transformations as the compiler and optimization passes of a system parallelizing shell pipelines, and use it to evaluate the speedup achieved on 47 pipelines. △ Less

Submitted 5 July, 2021; v1 submitted 30 December, 2020; originally announced December 2020.

SPPL: Probabilistic Programming with Fast Exact Symbolic Inference

Authors: Feras A. Saad, Martin C. Rinard, Vikash K. Mansinghka

Abstract: We present the Sum-Product Probabilistic Language (SPPL), a new probabilistic programming language that automatically delivers exact solutions to a broad range of probabilistic inference queries. SPPL translates probabilistic programs into sum-product expressions, a new symbolic representation and associated semantic domain that extends standard sum-product networks to support mixed-type distribut… ▽ More We present the Sum-Product Probabilistic Language (SPPL), a new probabilistic programming language that automatically delivers exact solutions to a broad range of probabilistic inference queries. SPPL translates probabilistic programs into sum-product expressions, a new symbolic representation and associated semantic domain that extends standard sum-product networks to support mixed-type distributions, numeric transformations, logical formulas, and pointwise and set-valued constraints. We formalize SPPL via a novel translation strategy from probabilistic programs to sum-product expressions and give sound exact algorithms for conditioning on and computing probabilities of events. SPPL imposes a collection of restrictions on probabilistic programs to ensure they can be translated into sum-product expressions, which allow the system to leverage new techniques for improving the scalability of translation and inference by automatically exploiting probabilistic structure. We implement a prototype of SPPL with a modular architecture and evaluate it on benchmarks the system targets, showing that it obtains up to 3500x speedups over state-of-the-art symbolic systems on tasks such as verifying the fairness of decision tree classifiers, smoothing hidden Markov models, conditioning transformed random variables, and computing rare event probabilities. △ Less

Submitted 11 June, 2021; v1 submitted 7 October, 2020; originally announced October 2020.

Journal ref: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '21), June 20-25, 2021, Virtual, Canada. ACM, New York, NY, USA

Inductive Program Synthesis Over Noisy Data

Authors: Shivam Handa, Martin Rinard

Abstract: We present a new framework and associated synthesis algorithms for program synthesis over noisy data, i.e., data that may contain incorrect/corrupted input-output examples. This framework is based on an extension of finite tree automata called {\em weighted finite tree automata}. We show how to apply this framework to formulate and solve a variety of program synthesis problems over noisy data. Res… ▽ More We present a new framework and associated synthesis algorithms for program synthesis over noisy data, i.e., data that may contain incorrect/corrupted input-output examples. This framework is based on an extension of finite tree automata called {\em weighted finite tree automata}. We show how to apply this framework to formulate and solve a variety of program synthesis problems over noisy data. Results from our implemented system running on problems from the SyGuS 2018 benchmark suite highlight its ability to successfully synthesize programs in the face of noisy data sets, including the ability to synthesize a correct program even when every input-output example in the data set is corrupted. △ Less

Submitted 18 October, 2020; v1 submitted 21 September, 2020; originally announced September 2020.

Dataflow Analysis With Prophecy and History Variables

Authors: Martin Rinard, Austin Gadient

Abstract: Leveraging concepts from state machine refinement proofs, we use prophecy variables, which predict information about the future program execution, to enable forward reasoning for backward dataflow analyses. Drawing prophecy and history variables (concepts from the dynamic execution of the program) from the same lattice as the static program analysis results, we require the analysis results to sati… ▽ More Leveraging concepts from state machine refinement proofs, we use prophecy variables, which predict information about the future program execution, to enable forward reasoning for backward dataflow analyses. Drawing prophecy and history variables (concepts from the dynamic execution of the program) from the same lattice as the static program analysis results, we require the analysis results to satisfy both the dataflow equations and the transition relations in the operational semantics of underlying programming language. This approach eliminates explicit abstraction and concretization functions and promotes a more direct connection between the analysis and program executions, with the connection taking the form of a bisimulation relation between concrete executions and an augmented operational semantics over the analysis results. We present several classical dataflow analyses with this approach (live variables, very busy expressions, defined variables, and reaching definitions) along with proofs that highlight how this approach can enable more streamlined reasoning. To the best of our knowledge, we are the first to use prophecy variables for dataflow analysis. △ Less

Submitted 23 July, 2020; originally announced July 2020.

Towards Context-Agnostic Learning Using Synthetic Data

Authors: Charles **, Martin Rinard

Abstract: We propose a novel setting for learning, where the input domain is the image of a map defined on the product of two sets, one of which completely determines the labels. We derive a new risk bound for this setting that decomposes into a bias and an error term, and exhibits a surprisingly weak dependence on the true labels. Inspired by these results, we present an algorithm aimed at minimizing the b… ▽ More We propose a novel setting for learning, where the input domain is the image of a map defined on the product of two sets, one of which completely determines the labels. We derive a new risk bound for this setting that decomposes into a bias and an error term, and exhibits a surprisingly weak dependence on the true labels. Inspired by these results, we present an algorithm aimed at minimizing the bias term by exploiting the ability to sample from each set independently. We apply our setting to visual classification tasks, where our approach enables us to train classifiers on datasets that consist entirely of a single synthetic example of each class. On several standard benchmarks for real-world image classification, we achieve robust performance in the context-agnostic setting, with good generalization to real world domains, whereas training directly on real world data without our techniques yields classifiers that are brittle to perturbations of the background. △ Less

Submitted 6 December, 2021; v1 submitted 29 May, 2020; originally announced May 2020.

Comments: Appearing at NeurIPS 2021. Code is available at https://github.com/charles**/synthetic_data

Efficient Exact Verification of Binarized Neural Networks

Authors: Kai Jia, Martin Rinard

Abstract: Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robust… ▽ More Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robustness and allow exact and significantly more efficient verification. We present a new system, EEV, for efficient and exact verification of BNNs. EEV consists of two parts: (i) a novel SAT solver that speeds up BNN verification by natively handling the reified cardinality constraints arising in BNN encodings; and (ii) strategies to train solver-friendly robust BNNs by inducing balanced layer-wise sparsity and low cardinality bounds, and adaptively cancelling the gradients. We demonstrate the effectiveness of EEV by presenting the first exact verification results for L-inf-bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Compared to exact verification of real-valued networks of the same architectures on the same tasks, EEV verifies BNNs hundreds to thousands of times faster, while delivering comparable verifiable accuracy in most cases. △ Less

Submitted 27 October, 2020; v1 submitted 7 May, 2020; originally announced May 2020.

Comments: To be published in NeurIPS 2020

Manifold Regularization for Locally Stable Deep Neural Networks

Authors: Charles **, Martin Rinard

Abstract: We apply concepts from manifold regularization to develop new regularization techniques for training locally stable deep neural networks. Our regularizers are based on a sparsification of the graph Laplacian which holds with high probability when the data is sparse in high dimensions, as is common in deep learning. Empirically, our networks exhibit stability in a diverse set of perturbation models… ▽ More We apply concepts from manifold regularization to develop new regularization techniques for training locally stable deep neural networks. Our regularizers are based on a sparsification of the graph Laplacian which holds with high probability when the data is sparse in high dimensions, as is common in deep learning. Empirically, our networks exhibit stability in a diverse set of perturbation models, including $\ell_2$, $\ell_\infty$, and Wasserstein-based perturbations; in particular, we achieve 40% adversarial accuracy on CIFAR-10 against an adaptive PGD attack using $\ell_\infty$ perturbations of size $ε= 8/255$, and state-of-the-art verified accuracy of 21% in the same perturbation model. Furthermore, our techniques are efficient, incurring overhead on par with two additional parallel forward passes through the network. △ Less

Submitted 22 September, 2020; v1 submitted 9 March, 2020; originally announced March 2020.

The Fast Loaded Dice Roller: A Near-Optimal Exact Sampler for Discrete Probability Distributions

Authors: Feras A. Saad, Cameron E. Freer, Martin C. Rinard, Vikash K. Mansinghka

Abstract: This paper introduces a new algorithm for the fundamental problem of generating a random integer from a discrete probability distribution using a source of independent and unbiased random coin flips. We prove that this algorithm, which we call the Fast Loaded Dice Roller (FLDR), is highly efficient in both space and time: (i) the size of the sampler is guaranteed to be linear in the number of bits… ▽ More This paper introduces a new algorithm for the fundamental problem of generating a random integer from a discrete probability distribution using a source of independent and unbiased random coin flips. We prove that this algorithm, which we call the Fast Loaded Dice Roller (FLDR), is highly efficient in both space and time: (i) the size of the sampler is guaranteed to be linear in the number of bits needed to encode the input distribution; and (ii) the expected number of bits of entropy it consumes per sample is at most 6 bits more than the information-theoretically optimal rate. We present fast implementations of the linear-time preprocessing and near-optimal sampling algorithms using unsigned integer arithmetic. Empirical evaluations on a broad set of probability distributions establish that FLDR is 2x-10x faster in both preprocessing and sampling than multiple baseline algorithms, including the widely-used alias and interval samplers. It also uses up to 10000x less space than the information-theoretically optimal sampler, at the expense of less than 1.5x runtime overhead. △ Less

Submitted 1 June, 2020; v1 submitted 8 March, 2020; originally announced March 2020.

Comments: 12 pages, 5 figures, 1 table. Appearing in AISTATS 2020

Journal ref: Proceedings of the 23rd International Conference on Artificial Intelligence and Statistics, PMLR 108:1036-1046, 2020

Exploiting Verified Neural Networks via Floating Point Numerical Error

Authors: Kai Jia, Martin Rinard

Abstract: Researchers have developed neural network verification algorithms motivated by the need to characterize the robustness of deep neural networks. The verifiers aspire to answer whether a neural network guarantees certain properties with respect to all inputs in a space. However, many verifiers inaccurately model floating point arithmetic but do not thoroughly discuss the consequences. We show that… ▽ More Researchers have developed neural network verification algorithms motivated by the need to characterize the robustness of deep neural networks. The verifiers aspire to answer whether a neural network guarantees certain properties with respect to all inputs in a space. However, many verifiers inaccurately model floating point arithmetic but do not thoroughly discuss the consequences. We show that the negligence of floating point error leads to unsound verification that can be systematically exploited in practice. For a pretrained neural network, we present a method that efficiently searches inputs as witnesses for the incorrectness of robustness claims made by a complete verifier. We also present a method to construct neural network architectures and weights that induce wrong results of an incomplete verifier. Our results highlight that, to achieve practically reliable verification of neural networks, any verification system must accurately (or conservatively) model the effects of any floating point computations in the network inference or verification system. △ Less

Submitted 1 October, 2021; v1 submitted 5 March, 2020; originally announced March 2020.

Comments: SAS 2021

Optimal Approximate Sampling from Discrete Probability Distributions

Authors: Feras A. Saad, Cameron E. Freer, Martin C. Rinard, Vikash K. Mansinghka

Abstract: This paper addresses a fundamental problem in random variate generation: given access to a random source that emits a stream of independent fair bits, what is the most accurate and entropy-efficient algorithm for sampling from a discrete probability distribution $(p_1, \dots, p_n)$, where the probabilities of the output distribution $(\hat{p}_1, \dots, \hat{p}_n)$ of the sampling algorithm must be… ▽ More This paper addresses a fundamental problem in random variate generation: given access to a random source that emits a stream of independent fair bits, what is the most accurate and entropy-efficient algorithm for sampling from a discrete probability distribution $(p_1, \dots, p_n)$, where the probabilities of the output distribution $(\hat{p}_1, \dots, \hat{p}_n)$ of the sampling algorithm must be specified using at most $k$ bits of precision? We present a theoretical framework for formulating this problem and provide new techniques for finding sampling algorithms that are optimal both statistically (in the sense of sampling accuracy) and information-theoretically (in the sense of entropy consumption). We leverage these results to build a system that, for a broad family of measures of statistical accuracy, delivers a sampling algorithm whose expected entropy usage is minimal among those that induce the same distribution (i.e., is "entropy-optimal") and whose output distribution $(\hat{p}_1, \dots, \hat{p}_n)$ is a closest approximation to the target distribution $(p_1, \dots, p_n)$ among all entropy-optimal sampling algorithms that operate within the specified $k$-bit precision. This optimal approximate sampler is also a closer approximation than any (possibly entropy-suboptimal) sampler that consumes a bounded amount of entropy with the specified precision, a class which includes floating-point implementations of inversion sampling and related methods found in many software libraries. We evaluate the accuracy, entropy consumption, precision requirements, and wall-clock runtime of our optimal approximate sampling algorithms on a broad set of distributions, demonstrating the ways that they are superior to existing approximate samplers and establishing that they often consume significantly fewer resources than are needed by exact samplers. △ Less

Submitted 13 January, 2020; originally announced January 2020.

Journal ref: Proc. ACM Program. Lang. 4, POPL, Article 36 (January 2020)

Characterizing Developer Use of Automatically Generated Patches

Authors: José Pablo Cambronero, Jiasi Shen, Jürgen Cito, Elena Glassman, Martin Rinard

Abstract: We present a study that characterizes the way developers use automatically generated patches when fixing software defects. Our study tasked two groups of developers with repairing defects in C programs. Both groups were provided with the defective line of code. One was also provided with five automatically generated and validated patches, all of which modified the defective line of code, and one o… ▽ More We present a study that characterizes the way developers use automatically generated patches when fixing software defects. Our study tasked two groups of developers with repairing defects in C programs. Both groups were provided with the defective line of code. One was also provided with five automatically generated and validated patches, all of which modified the defective line of code, and one of which was correct. Contrary to our initial expectations, the group with access to the generated patches did not produce more correct patches and did not produce patches in less time. We characterize the main behaviors observed in experimental subjects: a focus on understanding the defect and the relationship of the patches to the original source code. Based on this characterization, we highlight various potentially productive directions for future developer-centric automatic patch generation systems. △ Less

Submitted 22 November, 2019; v1 submitted 15 July, 2019; originally announced July 2019.

Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling

Authors: Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, Vikash K. Mansinghka

Abstract: We present new techniques for automatically constructing probabilistic programs for data analysis, interpretation, and prediction. These techniques work with probabilistic domain-specific data modeling languages that capture key properties of a broad class of data generating processes, using Bayesian inference to synthesize probabilistic programs in these modeling languages given observed data. We… ▽ More We present new techniques for automatically constructing probabilistic programs for data analysis, interpretation, and prediction. These techniques work with probabilistic domain-specific data modeling languages that capture key properties of a broad class of data generating processes, using Bayesian inference to synthesize probabilistic programs in these modeling languages given observed data. We provide a precise formulation of Bayesian synthesis for automatic data modeling that identifies sufficient conditions for the resulting synthesis procedure to be sound. We also derive a general class of synthesis algorithms for domain-specific languages specified by probabilistic context-free grammars and establish the soundness of our approach for these languages. We apply the techniques to automatically synthesize probabilistic programs for time series data and multivariate tabular data. We show how to analyze the structure of the synthesized programs to compute, for key qualitative properties of interest, the probability that the underlying data generating process exhibits each of these properties. Second, we translate probabilistic programs in the domain-specific language into probabilistic programs in Venture, a general-purpose probabilistic programming system. The translated Venture programs are then executed to obtain predictions of new time series data and new multivariate data records. Experimental results show that our techniques can accurately infer qualitative structure in multiple real-world data sets and outperform standard data analysis methods in forecasting and predicting new data. △ Less

Submitted 14 July, 2019; originally announced July 2019.

Journal ref: Proc. ACM Program. Lang. 3, POPL, Article 37 (January 2019)

Compositional Inference Metaprogramming with Convergence Guarantees

Authors: Shivam Handa, Vikash Mansinghka, Martin Rinard

Abstract: Inference metaprogramming enables effective probabilistic programming by supporting the decomposition of executions of probabilistic programs into subproblems and the deployment of hybrid probabilistic inference algorithms that apply different probabilistic inference algorithms to different subproblems. We introduce the concept of independent subproblem inference (as opposed to entangled subproble… ▽ More Inference metaprogramming enables effective probabilistic programming by supporting the decomposition of executions of probabilistic programs into subproblems and the deployment of hybrid probabilistic inference algorithms that apply different probabilistic inference algorithms to different subproblems. We introduce the concept of independent subproblem inference (as opposed to entangled subproblem inference in which the subproblem inference algorithm operates over the full program trace) and present a mathematical framework for studying convergence properties of hybrid inference algorithms that apply different Markov-Chain Monte Carlo algorithms to different parts of the inference problem. We then use this formalism to prove asymptotic convergence results for probablistic programs with inference metaprogramming. To the best of our knowledge this is the first asymptotic convergence result for hybrid probabilistic inference algorithms defined by (subproblem-based) inference metaprogramming. △ Less

Submitted 15 July, 2019; v1 submitted 11 July, 2019; originally announced July 2019.

Correctness Verification of Neural Networks

Authors: Yichen Yang, Martin Rinard

Abstract: We present a novel framework for specifying and verifying correctness globally for neural networks on perception tasks. Most previous works on neural network verification for perception tasks focus on robustness verification. Unlike robustness verification, which aims to verify that the prediction of a network is stable in some local regions around labelled points, our framework provides a way to… ▽ More We present a novel framework for specifying and verifying correctness globally for neural networks on perception tasks. Most previous works on neural network verification for perception tasks focus on robustness verification. Unlike robustness verification, which aims to verify that the prediction of a network is stable in some local regions around labelled points, our framework provides a way to specify correctness globally in the whole target input space and verify that the network is correct for all target inputs (or find the regions where the network is not correct). We provide a specification through 1) a state space consisting of all relevant states of the world and 2) an observation process that produces neural network inputs from the states of the world. Tiling the state and input spaces with a finite number of tiles, obtaining ground truth bounds from the state tiles and network output bounds from the input tiles, then comparing the ground truth and network output bounds delivers an upper bound on the network output error for any inputs of interest. The presented framework also enables detecting illegal inputs -- inputs that are not contained in (or close to) the target input space as defined by the state space and observation process (the neural network is not designed to work on them), so that we can flag when we don't have guarantees. Results from two case studies highlight the ability of our technique to verify error bounds over the whole target input space and show how the error bounds vary over the state and input spaces. △ Less

Submitted 23 August, 2022; v1 submitted 3 June, 2019; originally announced June 2019.

Cimple: Instruction and Memory Level Parallelism

Authors: Vladimir Kiriansky, Haoran Xu, Martin Rinard, Saman Amarasinghe

Abstract: Modern out-of-order processors have increased capacity to exploit instruction level parallelism (ILP) and memory level parallelism (MLP), e.g., by using wide superscalar pipelines and vector execution units, as well as deep buffers for in-flight memory requests. These resources, however, often exhibit poor utilization rates on workloads with large working sets, e.g., in-memory databases, key-value… ▽ More Modern out-of-order processors have increased capacity to exploit instruction level parallelism (ILP) and memory level parallelism (MLP), e.g., by using wide superscalar pipelines and vector execution units, as well as deep buffers for in-flight memory requests. These resources, however, often exhibit poor utilization rates on workloads with large working sets, e.g., in-memory databases, key-value stores, and graph analytics, as compilers and hardware struggle to expose ILP and MLP from the instruction stream automatically. In this paper, we introduce the IMLP (Instruction and Memory Level Parallelism) task programming model. IMLP tasks execute as coroutines that yield execution at annotated long-latency operations, e.g., memory accesses, divisions, or unpredictable branches. IMLP tasks are interleaved on a single thread, and integrate well with thread parallelism and vectorization. Our DSL embedded in C++, Cimple, allows exploration of task scheduling and transformations, such as buffering, vectorization, pipelining, and prefetching. We demonstrate state-of-the-art performance on core algorithms used in in-memory databases that operate on arrays, hash tables, trees, and skip lists. Cimple applications reach 2.5x throughput gains over hardware multithreading on a multi-core, and 6.4x single thread speedup. △ Less

Submitted 4 July, 2018; originally announced July 2018.

Comments: To appear in PACT'18

A Hardware Platform for Efficient Multi-Modal Sensing with Adaptive Approximation

Authors: Phillip Stanley-Marbell, Martin Rinard

Abstract: We present Warp, a hardware platform to support research in approximate computing, sensor energy optimization, and energy-scavenged systems. Warp incorporates 11 state-of-the-art sensor integrated circuits, computation, and an energy-scavenged power supply, all within a miniature system that is just 3.6 cm x 3.3 cm x 0.5 cm. Warp's sensor integrated circuits together contain a total of 21 sensors… ▽ More We present Warp, a hardware platform to support research in approximate computing, sensor energy optimization, and energy-scavenged systems. Warp incorporates 11 state-of-the-art sensor integrated circuits, computation, and an energy-scavenged power supply, all within a miniature system that is just 3.6 cm x 3.3 cm x 0.5 cm. Warp's sensor integrated circuits together contain a total of 21 sensors with a range of precisions and accuracies for measuring eight sensing modalities of acceleration, angular rate, magnetic flux density (compass heading), humidity, atmospheric pressure (elevation), infrared radiation, ambient temperature, and color. Warp uses a combination of analog circuits and digital control to facilitate further tradeoffs between sensor and communication accuracy, energy efficiency, and performance. This article presents the design of Warp and presents an evaluation of our hardware implementation. The results show how Warp's design enables performance and energy efficiency versus ac- curacy tradeoffs. △ Less

Submitted 6 April, 2018; originally announced April 2018.

Incremental Color Quantization for Color-Vision-Deficient Observers Using Mobile Gaming Data

Authors: Jose Cambronero, Phillip Stanley-Marbell, Martin Rinard

Abstract: The sizes of compressed images depend on their spatial resolution (number of pixels) and on their color resolution (number of color quantization levels). We introduce DaltonQuant, a new color quantization technique for image compression that cloud services can apply to images destined for a specific user with known color vision deficiencies. DaltonQuant improves compression in a user-specific but… ▽ More The sizes of compressed images depend on their spatial resolution (number of pixels) and on their color resolution (number of color quantization levels). We introduce DaltonQuant, a new color quantization technique for image compression that cloud services can apply to images destined for a specific user with known color vision deficiencies. DaltonQuant improves compression in a user-specific but reversible manner thereby improving a user's network bandwidth and data storage efficiency. DaltonQuant quantizes image data to account for user-specific color perception anomalies, using a new method for incremental color quantization based on a large corpus of color vision acuity data obtained from a popular mobile game. Servers that host images can revert DaltonQuant's image requantization and compression when those images must be transmitted to a different user, making the technique practical to deploy on a large scale. We evaluate DaltonQuant's compression performance on the Kodak PC reference image set and show that it improves compression by an additional 22%-29% over the state-of-the-art compressors TinyPNG and pngquant. △ Less

Submitted 22 March, 2018; originally announced March 2018.

The Three Pillars of Machine Programming

Authors: Justin Gottschlich, Armando Solar-Lezama, Nesime Tatbul, Michael Carbin, Martin Rinard, Regina Barzilay, Saman Amarasinghe, Joshua B Tenenbaum, Tim Mattson

Abstract: In this position paper, we describe our vision of the future of machine programming through a categorical examination of three pillars of research. Those pillars are: (i) intention, (ii) invention, and(iii) adaptation. Intention emphasizes advancements in the human-to-computer and computer-to-machine-learning interfaces. Invention emphasizes the creation or refinement of algorithms or core hardwar… ▽ More In this position paper, we describe our vision of the future of machine programming through a categorical examination of three pillars of research. Those pillars are: (i) intention, (ii) invention, and(iii) adaptation. Intention emphasizes advancements in the human-to-computer and computer-to-machine-learning interfaces. Invention emphasizes the creation or refinement of algorithms or core hardware and software building blocks through machine learning (ML). Adaptation emphasizes advances in the use of ML-based constructs to autonomously evolve software. △ Less

Submitted 26 June, 2021; v1 submitted 19 March, 2018; originally announced March 2018.

Unanimous Prediction for 100% Precision with Application to Learning Semantic Map**s

Authors: Fereshte Khani, Martin Rinard, Percy Liang

Abstract: Can we train a system that, on any new input, either says "don't know" or makes a prediction that is guaranteed to be correct? We answer the question in the affirmative provided our model family is well-specified. Specifically, we introduce the unanimity principle: only predict when all models consistent with the training data predict the same output. We operationalize this principle for semantic… ▽ More Can we train a system that, on any new input, either says "don't know" or makes a prediction that is guaranteed to be correct? We answer the question in the affirmative provided our model family is well-specified. Specifically, we introduce the unanimity principle: only predict when all models consistent with the training data predict the same output. We operationalize this principle for semantic parsing, the task of map** utterances to logical forms. We develop a simple, efficient method that reasons over the infinite set of all consistent models by only checking two of the models. We prove that our method obtains 100% precision even with a modest amount of training data from a possibly adversarial distribution. Empirically, we demonstrate the effectiveness of our approach on the standard GeoQuery dataset. △ Less

Submitted 23 June, 2016; v1 submitted 20 June, 2016; originally announced June 2016.

Comments: ACL 2016, Removed the duplicate author name of the previous version

ACM Class: I.2.7; I.2.6

An Analysis of the Search Spaces for Generate and Validate Patch Generation Systems

Authors: Fan Long, Martin Rinard

Abstract: We present the first systematic analysis of the characteristics of patch search spaces for automatic patch generation systems. We analyze the search spaces of two current state-of-the-art systems, SPR and Prophet, with 16 different search space configurations. Our results are derived from an analysis of 1104 different search spaces and 768 patch generation executions. Together these experiments co… ▽ More We present the first systematic analysis of the characteristics of patch search spaces for automatic patch generation systems. We analyze the search spaces of two current state-of-the-art systems, SPR and Prophet, with 16 different search space configurations. Our results are derived from an analysis of 1104 different search spaces and 768 patch generation executions. Together these experiments consumed over 9000 hours of CPU time on Amazon EC2. The analysis shows that 1) correct patches are sparse in the search spaces (typically at most one correct patch per search space per defect), 2) incorrect patches that nevertheless pass all of the test cases in the validation test suite are typically orders of magnitude more abundant, and 3) leveraging information other than the test suite is therefore critical for enabling the system to successfully isolate correct patches. We also characterize a key tradeoff in the structure of the search spaces. Larger and richer search spaces that contain correct patches for more defects can actually cause systems to find fewer, not more, correct patches. We identify two reasons for this phenomenon: 1) increased validation times because of the presence of more candidate patches and 2) more incorrect patches that pass the test suite and block the discovery of correct patches. These fundamental properties, which are all characterized for the first time in this paper, help explain why past systems often fail to generate correct patches and help identify challenges, opportunities, and productive future directions for the field. △ Less

Submitted 17 February, 2016; originally announced February 2016.

ACM Class: D.2.5

(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints

Authors: Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, Martin Rinard

Abstract: We prove several decidability and undecidability results for the satisfiability and validity problems for languages that can express solutions to word equations with length constraints. The atomic formulas over this language are equality over string terms (word equations), linear inequality over the length function (length constraints), and membership in regular sets. These questions are important… ▽ More We prove several decidability and undecidability results for the satisfiability and validity problems for languages that can express solutions to word equations with length constraints. The atomic formulas over this language are equality over string terms (word equations), linear inequality over the length function (length constraints), and membership in regular sets. These questions are important in logic, program analysis, and formal verification. Variants of these questions have been studied for many decades by mathematicians. More recently, practical satisfiability procedures (aka SMT solvers) for these formulas have become increasingly important in the context of security analysis for string-manipulating programs such as web applications. We prove three main theorems. First, we give a new proof of undecidability for the validity problem for the set of sentences written as a forall-exists quantifier alternation applied to positive word equations. A corollary of this undecidability result is that this set is undecidable even with sentences with at most two occurrences of a string variable. Second, we consider Boolean combinations of quantifier-free formulas constructed out of word equations and length constraints. We show that if word equations can be converted to a solved form, a form relevant in practice, then the satisfiability problem for Boolean combinations of word equations and length constraints is decidable. Third, we show that the satisfiability problem for quantifier-free formulas over word equations in regular solved form, length constraints, and the membership predicate over regular expressions is also decidable. △ Less

Submitted 25 June, 2013; originally announced June 2013.

Comments: Invited Paper at ADDCT Workshop 2013 (co-located with CADE 2013)

Cryptographic Path Hardening: Hiding Vulnerabilities in Software through Cryptography

Authors: Vijay Ganesh, Michael Carbin, Martin Rinard

Abstract: We propose a novel approach to improving software security called Cryptographic Path Hardening, which is aimed at hiding security vulnerabilities in software from attackers through the use of provably secure and obfuscated cryptographic devices to harden paths in programs. By "harden" we mean that certain error-checking if-conditionals in a given program P are replaced by equivalent" we mean tha… ▽ More We propose a novel approach to improving software security called Cryptographic Path Hardening, which is aimed at hiding security vulnerabilities in software from attackers through the use of provably secure and obfuscated cryptographic devices to harden paths in programs. By "harden" we mean that certain error-checking if-conditionals in a given program P are replaced by equivalent" we mean that adversaries cannot use semi-automatic program analysis techniques to reason about the hardened program paths and thus cannot discover as-yet-unknown errors along those paths, except perhaps through black-box dictionary attacks or random testing (which we can never prevent). Other than these unpreventable attack methods, we can make program analysis aimed at error-finding "provably hard" for a resource-bounded attacker, in the same sense that cryptographic schemes are hard to break. Unlike security-through-obscurity, in Cryptographic Path Hardening we use provably-secure crypto devices to hide errors and our mathematical arguments of security are the same as the standard ones used in cryptography. One application of Cryptographic Path Hardening is that software patches or filters often reveal enough information to an attacker that they can be used to construct error-revealing inputs to exploit an unpatched version of the program. By "hardening" the patch we make it difficult for the attacker to analyze the patched program to construct error-revealing inputs, and thus prevent him from potentially constructing exploits. △ Less

Submitted 1 February, 2012; originally announced February 2012.

Comments: Accepted as part of Off-the-beaten track at POPL 2012

ARBAC Policy for a Large Multi-National Bank

Authors: Karthick Jayaraman, Vijay Ganesh, Mahesh Tripunitara, Martin C Rinard, Steve J. Chapin

Abstract: Administrative role-based access control (ARBAC) is the first comprehensive administrative model proposed for role-based access control (RBAC). ARBAC has several features for designing highly expressive policies, but current work has not highlighted the utility of these expressive policies. In this report, we present a case study of designing an ARBAC policy for a bank comprising 18 branches. Usin… ▽ More Administrative role-based access control (ARBAC) is the first comprehensive administrative model proposed for role-based access control (RBAC). ARBAC has several features for designing highly expressive policies, but current work has not highlighted the utility of these expressive policies. In this report, we present a case study of designing an ARBAC policy for a bank comprising 18 branches. Using this case study we provide an assessment about the features of ARBAC that are likely to be used in realistic policies. △ Less

Submitted 13 October, 2011; originally announced October 2011.

On Verifying Complex Properties using Symbolic Shape Analysis

Authors: Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, Martin Rinard

Abstract: One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their s… ▽ More One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their specifications expressed in terms of changes to the set of objects stored in the data structure. During the analysis, Bohne infers loop invariants in the form of disjunctions of universally quantified Boolean combinations of formulas. To synthesize loop invariants of this form, Bohne uses a combination of decision procedures for Monadic Second-Order Logic over trees, SMT-LIB decision procedures (currently CVC Lite), and an automated reasoner within the Isabelle interactive theorem prover. This architecture shows that synthesized loop invariants can serve as a useful communication mechanism between different decision procedures. Using Bohne, we have verified operations on data structures such as linked lists with iterators and back pointers, trees with and without parent pointers, two-level skip lists, array data structures, and sorted lists. We have deployed Bohne in the Hob and Jahob data structure analysis systems, enabling us to combine Bohne with analyses of data structure clients and apply it in the context of larger programs. This report describes the Bohne algorithm as well as techniques that Bohne uses to reduce the ammount of annotations and the running time of the analysis. △ Less

Submitted 18 September, 2006; originally announced September 2006.

Report number: MPI-I-2006-2-001

On Algorithms and Complexity for Sets with Cardinality Constraints

Authors: Bruno Marnette, Viktor Kuncak, Martin Rinard

Abstract: Typestate systems ensure many desirable properties of imperative programs, including initialization of object fields and correct use of stateful library interfaces. Abstract sets with cardinality constraints naturally generalize typestate properties: relationships between the typestates of objects can be expressed as subset and disjointness relations on sets, and elements of sets can be represen… ▽ More Typestate systems ensure many desirable properties of imperative programs, including initialization of object fields and correct use of stateful library interfaces. Abstract sets with cardinality constraints naturally generalize typestate properties: relationships between the typestates of objects can be expressed as subset and disjointness relations on sets, and elements of sets can be represented as sets of cardinality one. Motivated by these applications, this paper presents new algorithms and new complexity results for constraints on sets and their cardinalities. We study several classes of constraints and demonstrate a trade-off between their expressive power and their complexity. Our first result concerns a quantifier-free fragment of Boolean Algebra with Presburger Arithmetic. We give a nondeterministic polynomial-time algorithm for reducing the satisfiability of sets with symbolic cardinalities to constraints on constant cardinalities, and give a polynomial-space algorithm for the resulting problem. In a quest for more efficient fragments, we identify several subclasses of sets with cardinality constraints whose satisfiability is NP-hard. Finally, we identify a class of constraints that has polynomial-time satisfiability and entailment problems and can serve as a foundation for efficient program analysis. △ Less

Submitted 28 August, 2005; originally announced August 2005.

Comments: 20 pages. 12 figures

Report number: MIT CSAIL Technical Report MIT-LCS-TR-997

On Spatial Conjunction as Second-Order Logic

Authors: Viktor Kuncak, Martin Rinard

Abstract: Spatial conjunction is a powerful construct for reasoning about dynamically allocated data structures, as well as concurrent, distributed and mobile computation. While researchers have identified many uses of spatial conjunction, its precise expressive power compared to traditional logical constructs was not previously known. In this paper we establish the expressive power of spatial conjunction… ▽ More Spatial conjunction is a powerful construct for reasoning about dynamically allocated data structures, as well as concurrent, distributed and mobile computation. While researchers have identified many uses of spatial conjunction, its precise expressive power compared to traditional logical constructs was not previously known. In this paper we establish the expressive power of spatial conjunction. We construct an embedding from first-order logic with spatial conjunction into second-order logic, and more surprisingly, an embedding from full second order logic into first-order logic with spatial conjunction. These embeddings show that the satisfiability of formulas in first-order logic with spatial conjunction is equivalent to the satisfiability of formulas in second-order logic. These results explain the great expressive power of spatial conjunction and can be used to show that adding unrestricted spatial conjunction to a decidable logic leads to an undecidable logic. As one example, we show that adding unrestricted spatial conjunction to two-variable logic leads to undecidability. On the side of decidability, the embedding into second-order logic immediately implies the decidability of first-order logic with a form of spatial conjunction over trees. The embedding into spatial conjunction also has useful consequences: because a restricted form of spatial conjunction in two-variable logic preserves decidability, we obtain that a correspondingly restricted form of second-order quantification in two-variable logic is decidable. The resulting language generalizes the first-order theory of boolean algebra over sets and is useful in reasoning about the contents of data structures in object-oriented languages. △ Less

Submitted 28 October, 2004; originally announced October 2004.

Comments: 16 pages

Report number: MIT CSAIL 970