10 citations · 21 across the 10 of their papers we have counts for
11 papers
Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Stefan Zetzsche, Jean-Baptiste Tristan, Tancrede Lepoint +1
The Fisher-Yates shuffle is a well-known algorithm for shuffling a finite sequence, such that every permutation is equally likely. Despite its simplicity, it is prone to implementa…
Verified Foundations for Differential Privacy
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint +7
Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifyi…
On computable learning of continuous features
Nathanael Ackerman, Julian Asilis, Jieqi Di +2
We introduce definitions of computable PAC learning for binary classification over computable metric spaces. We provide sufficient conditions for learners that are empirical risk m…
Conjugate Energy-Based Models
Hao Wu, Babak Esmaeili, Michael Wick +2
In this paper, we propose conjugate energy-based models (CEBMs), a new class of energy-based models that define a joint density over data and latent variables. The joint density of…
Detecting and Exorcising Statistical Demons from Language Models with Anti-Models of Negative Data
Michael L. Wick, Kate Silverstein, Jean-Baptiste Tristan +2
It's been said that "Language Models are Unsupervised Multitask Learners." Indeed, self-supervised language models trained on "positive" examples of English text generalize in desi…
Verification of ML Systems via Reparameterization
Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha +2
As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machin…
A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee +1
We present a formal proof in Lean of probably approximately correct (PAC) learnability of the concept class of decision stumps. This classic result in machine learning theory deriv…
Sketching for Latent Dirichlet-Categorical Models
Joseph Tassarotti, Jean-Baptiste Tristan, Michael Wick
Recent work has explored transforming data sets into smaller, approximate summaries in order to scale Bayesian inference. We examine a related problem in which the parameters of a…
Gradient-based Inference for Networks with Output Constraints
Jay Yoon Lee, Sanket Vaibhav Mehta, Michael Wick +2
Practitioners apply neural networks to increasingly complex problems in natural language processing, such as syntactic parsing and semantic role labeling that have rich output stru…
Using Butterfly-Patterned Partial Sums to Optimize GPU Memory Accesses for Drawing from Discrete Distributions
Guy L. Steele, Jean-Baptiste Tristan
We describe a technique for drawing values from discrete distributions, such as sampling from the random variables of a mixture model, that avoids computing a complete table of par…
Augur: a Modeling Language for Data-Parallel Probabilistic Inference
Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti +3
It is time-consuming and error-prone to implement inference procedures for each new probabilistic model. Probabilistic programming addresses this problem by allowing a user to spec…