Showing 101–150 of 181 results for author: Hsu, J

Synthesizing Coupling Proofs of Differential Privacy

Authors: Aws Albarghouthi, Justin Hsu

Abstract: Differential privacy has emerged as a promising probabilistic formulation of privacy, generating intense interest within academia and industry. We present a push-button, automated technique for verifying $\varepsilon$-differential privacy of sophisticated randomized algorithms. We make several conceptual, algorithmic, and practical contributions: (i) Inspired by the recent advances on approximate… ▽ More Differential privacy has emerged as a promising probabilistic formulation of privacy, generating intense interest within academia and industry. We present a push-button, automated technique for verifying $\varepsilon$-differential privacy of sophisticated randomized algorithms. We make several conceptual, algorithmic, and practical contributions: (i) Inspired by the recent advances on approximate couplings and randomness alignment, we present a new proof technique called coupling strategies, which casts differential privacy proofs as a winning strategy in a game where we have finite privacy resources to expend. (ii) To discover a winning strategy, we present a constraint-based formulation of the problem as a set of Horn modulo couplings (HMC) constraints, a novel combination of first-order Horn clauses and probabilistic constraints. (iii) We present a technique for solving HMC constraints by transforming probabilistic constraints into logical constraints with uninterpreted functions. (iv) Finally, we implement our technique in the FairSquare verifier and provide the first automated privacy proofs for a number of challenging algorithms from the differential privacy literature, including Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism. △ Less

Submitted 8 November, 2017; v1 submitted 15 September, 2017; originally announced September 2017.

Learning 6-DOF Gras** Interaction via Deep Geometry-aware 3D Representations

Authors: Xinchen Yan, Jasmine Hsu, Mohi Khansari, Yunfei Bai, Arkanath Pathak, Abhinav Gupta, James Davidson, Honglak Lee

Abstract: This paper focuses on the problem of learning 6-DOF gras** with a parallel jaw gripper in simulation. We propose the notion of a geometry-aware representation in gras** based on the assumption that knowledge of 3D geometry is at the heart of interaction. Our key idea is constraining and regularizing gras** interaction learning through 3D geometry prediction. Specifically, we formulate the le… ▽ More This paper focuses on the problem of learning 6-DOF gras** with a parallel jaw gripper in simulation. We propose the notion of a geometry-aware representation in gras** based on the assumption that knowledge of 3D geometry is at the heart of interaction. Our key idea is constraining and regularizing gras** interaction learning through 3D geometry prediction. Specifically, we formulate the learning of deep geometry-aware gras** model in two steps: First, we learn to build mental geometry-aware representation by reconstructing the scene (i.e., 3D occupancy grid) from RGBD input via generative 3D shape modeling. Second, we learn to predict gras** outcome with its internal geometry-aware representation. The learned outcome prediction model is used to sequentially propose gras** solutions via analysis-by-synthesis optimization. Our contributions are fourfold: (1) To best of our knowledge, we are presenting for the first time a method to learn a 6-DOF gras** net from RGBD input; (2) We build a gras** dataset from demonstrations in virtual reality with rich sensory and interaction annotations. This dataset includes 101 everyday objects spread across 7 categories, additionally, we propose a data augmentation strategy for effective learning; (3) We demonstrate that the learned geometry-aware representation leads to about 10 percent relative performance improvement over the baseline CNN on gras** objects from our dataset. (4) We further demonstrate that the model generalizes to novel viewpoints and object instances. △ Less

Submitted 14 June, 2018; v1 submitted 24 August, 2017; originally announced August 2017.

Comments: Published at ICRA 2018

Proving Expected Sensitivity of Probabilistic Programs

Authors: Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Abstract: Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program's input lead to bounded changes in the output. We propose an average notion of program sensitivity for probabilistic programs---expected sensitivity---that averages a distance function over a probabilistic coupling of two output distributions from two similar inputs. By varying the distance, expected… ▽ More Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program's input lead to bounded changes in the output. We propose an average notion of program sensitivity for probabilistic programs---expected sensitivity---that averages a distance function over a probabilistic coupling of two output distributions from two similar inputs. By varying the distance, expected sensitivity recovers useful notions of probabilistic function sensitivity, including stability of machine learning algorithms and convergence of Markov chains. Furthermore, expected sensitivity satisfies clean compositional properties and is amenable to formal verification. We develop a relational program logic called $\mathbb{E}$pRHL for proving expected sensitivity properties. Our logic features two key ideas. First, relational pre-conditions and post-conditions are expressed using distances, a real-valued generalization of typical boolean-valued (relational) assertions. Second, judgments are interpreted in terms of expectation coupling, a novel, quantitative generalization of probabilistic couplings which supports compositional reasoning. We demonstrate our logic on examples beyond the reach of prior relational logics. Our main example formalizes uniform stability of the stochastic gradient method. Furthermore, we prove rapid mixing for a probabilistic model of population dynamics. We also extend our logic with a transitivity principle for expectation couplings to capture the path coupling proof technique by Bubley and Dyer, and formalize rapid mixing of the Glauber dynamics from statistical physics. △ Less

Submitted 8 November, 2017; v1 submitted 8 August, 2017; originally announced August 2017.

Confining Quark Model with General Yang-Mills Symmetry and Inadequate Faddeev-Popov Ghost

Authors: Jong-** Hsu

Abstract: A quark model with general Yang-Mills $SU_3$ symmetry leads to fourth-order field equations and linear confining potential. The confining gauge bosons (`confions') are treated as off-mass-shell particles and their indefinite energies are unobservable due to confinement. The ultraviolet divergence of the model appears to be no worse than that of QCD by power counting. Explicit calculations of the c… ▽ More A quark model with general Yang-Mills $SU_3$ symmetry leads to fourth-order field equations and linear confining potential. The confining gauge bosons (`confions') are treated as off-mass-shell particles and their indefinite energies are unobservable due to confinement. The ultraviolet divergence of the model appears to be no worse than that of QCD by power counting. Explicit calculations of the confion self-energy show that the usual Faddeev-Popov ghosts are inadequate to restore gauge symmetry for gauge invariant Lagrangians with higher order derivatives. `Computer experiments' with FeynCalc lead to a simple empirical method to restore the gauge invariance of the second-order confion self-energy with arbitrary gauge parameters. The approximate results of third-order vertex corrections suggest that the confining model could be asymptotically free. △ Less

Submitted 11 July, 2017; originally announced July 2017.

Comments: 9 pages

Probabilistic Program Equivalence for NetKAT

Authors: Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, Dexter Kozen, Alexandra Silva

Abstract: We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language by develo** an effective decision procedure based on stochastic matrices. The main challenge lies in reasoning… ▽ More We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language by develo** an effective decision procedure based on stochastic matrices. The main challenge lies in reasoning about iteration, which we address by designing an encoding of the program semantics as a finite-state absorbing Markov chain, whose limiting distribution can be computed exactly. In an extended case study on a real-world data center network, we automatically verify various quantitative properties of interest, including resilience in the presence of failures, by analyzing the Markov chain semantics. △ Less

Submitted 24 March, 2018; v1 submitted 10 July, 2017; originally announced July 2017.

Graphene-Complex-oxide Nanoscale Device Concepts

Authors: Giriraj Jnawali, Hyungwoo Lee, Jung-Woo Lee, Mengchen Huang, Jen-Feng Hsu, Bi Feng, Rongpu Zhou, Guanglei Cheng, Brian DUrso, Patrick Irvin, Chang-Beom Eom, Jeremy Levy

Abstract: The integration of graphene with complex-oxide heterostructures such as LaAlO$_3$/SrTiO$_3$ offers the opportunity to combine the multifunctional properties of an oxide interface with the electronic properties of graphene. The ability to control interface conduction through graphene and understanding how it affects the intrinsic properties of an oxide interface are critical to the technological de… ▽ More The integration of graphene with complex-oxide heterostructures such as LaAlO$_3$/SrTiO$_3$ offers the opportunity to combine the multifunctional properties of an oxide interface with the electronic properties of graphene. The ability to control interface conduction through graphene and understanding how it affects the intrinsic properties of an oxide interface are critical to the technological development of novel multifunctional devices. Here we demonstrate several device archetypes in which electron transport at an oxide interface is modulated using a patterned graphene top gate. Nanoscale devices are fabricated at the oxide interface by conductive atomic force microscope (c-AFM) lithography, and transport measurements are performed as a function of the graphene gate voltage. Experiments are performed with devices written adjacent to or directly underneath the graphene gate. Unique capabilities of this approach include the ability to create highly flexible device configurations, the ability to modulate carrier density at the oxide interface, and the ability to control electron transport up to the single-electron-tunneling regime, while maintaining intrinsic transport properties of the oxide interface. Our results facilitate the design of a variety of nanoscale devices that combine unique transport properties of these two intimately coupled two-dimensional electron systems. △ Less

Submitted 4 April, 2018; v1 submitted 30 June, 2017; originally announced June 2017.

Comments: 27 pages, 10 figures

Relational $\star$-Liftings for Differential Privacy

Authors: Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub

Abstract: Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. This construction can be defined in two styles. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of s… ▽ More Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. This construction can be defined in two styles. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have each have their own strengths: the universal version is more general than the existential ones, while existential liftings are known to satisfy more precise composition principles. We propose a novel, existential version of approximate lifting, called $\star$-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, yielding cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and consider more general approximate liftings based on $f$-divergences. △ Less

Submitted 18 December, 2019; v1 submitted 29 April, 2017; originally announced May 2017.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 4 (December 19, 2019) lmcs:4380

Time-Contrastive Networks: Self-Supervised Learning from Video

Authors: Pierre Sermanet, Corey Lynch, Yevgen Chebotar, Jasmine Hsu, Eric Jang, Stefan Schaal, Sergey Levine

Abstract: We propose a self-supervised approach for learning representations and robotic behaviors entirely from unlabeled videos recorded from multiple viewpoints, and study how this representation can be used in two robotic imitation settings: imitating object interactions from videos of humans, and imitating human poses. Imitation of human behavior requires a viewpoint-invariant representation that captu… ▽ More We propose a self-supervised approach for learning representations and robotic behaviors entirely from unlabeled videos recorded from multiple viewpoints, and study how this representation can be used in two robotic imitation settings: imitating object interactions from videos of humans, and imitating human poses. Imitation of human behavior requires a viewpoint-invariant representation that captures the relationships between end-effectors (hands or robot grippers) and the environment, object attributes, and body pose. We train our representations using a metric learning loss, where multiple simultaneous viewpoints of the same observation are attracted in the embedding space, while being repelled from temporal neighbors which are often visually similar but functionally different. In other words, the model simultaneously learns to recognize what is common between different-looking images, and what is different between similar-looking images. This signal causes our model to discover attributes that do not change across viewpoint, but do change across time, while ignoring nuisance variables such as occlusions, motion blur, lighting and background. We demonstrate that this representation can be used by a robot to directly mimic human poses without an explicit correspondence, and that it can be used as a reward function within a reinforcement learning algorithm. While representations are learned from an unlabeled collection of task-related videos, robot behaviors such as pouring are learned by watching a single 3rd-person demonstration by a human. Reward functions obtained by following the human demonstrations under the learned representation enable efficient reinforcement learning that is practical for real-world robotic systems. Video results, open-source code and dataset are available at https://sermanet.github.io/imitate △ Less

Submitted 19 March, 2018; v1 submitted 23 April, 2017; originally announced April 2017.

A Semantic Account of Metric Preservation

Authors: Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui

Abstract: Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an $r$-sensitive function map inputs that are at distance $d$ to outputs that are at distance at mo… ▽ More Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an $r$-sensitive function map inputs that are at distance $d$ to outputs that are at distance at most $r \cdot d$. Program sensitivity is thus an analogue of Lipschitz continuity for programs. Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz. △ Less

Submitted 23 October, 2022; v1 submitted 1 February, 2017; originally announced February 2017.

The $L^2$-cutoffs for reversible Markov chains

Authors: Guan-Yu Chen, Jui-Ming Hsu, Yuan-Chung Sheu

Abstract: In this article, we considers reversible Markov chains of which $L^2$-distances can be expressed in terms of Laplace transforms. The cutoff of Laplace transforms was first discussed by Chen and Saloff-Coste in [8], while we provide here a completely different pathway to analyze the $L^2$-distance. Consequently, we obtain several considerably simplified criteria and this allows us to proceed advanc… ▽ More In this article, we considers reversible Markov chains of which $L^2$-distances can be expressed in terms of Laplace transforms. The cutoff of Laplace transforms was first discussed by Chen and Saloff-Coste in [8], while we provide here a completely different pathway to analyze the $L^2$-distance. Consequently, we obtain several considerably simplified criteria and this allows us to proceed advanced theoretical studies, including the comparison of cutoffs between discrete time lazy chains and continuous time chains. For an illustration, we consider product chains, a rather complicated model which could be involved to analyze using the method in [8], and derive the equivalence of their $L^2$-cutoffs. △ Less

Submitted 23 January, 2017; originally announced January 2017.

MSC Class: 60J10; 60J27

Proving uniformity and independence by self-composition and coupling

Authors: Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Abstract: Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and… ▽ More Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL---whose proofs are formal versions of proofs by coupling---can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant. △ Less

Submitted 1 April, 2017; v1 submitted 23 January, 2017; originally announced January 2017.

Neutrino Oscillation, Finite Self-Mass and General Yang-Mills Symmetry

Authors: Jong-** Hsu

Abstract: The conservation of lepton number is assumed to be associated with a general Yang-Mills symmetry. New transformations involve (Lorentz) vector gauge functions and characteristic phase functions, and they form a group. General Yang-Mills fields are associated with new fourth-order equations and linear potentials. Lepton self-masses turn out to be finite and proportional to the inverse of lepton mas… ▽ More The conservation of lepton number is assumed to be associated with a general Yang-Mills symmetry. New transformations involve (Lorentz) vector gauge functions and characteristic phase functions, and they form a group. General Yang-Mills fields are associated with new fourth-order equations and linear potentials. Lepton self-masses turn out to be finite and proportional to the inverse of lepton masses, which implies that neutrinos should have non-zero masses. Thus, general Yang-Mills symmetry could provide an understanding of neutrino oscillations and suggests that neutrinos with masses and very weak leptonic force may play a role in dark matter. △ Less

Submitted 18 October, 2016; v1 submitted 16 September, 2016; originally announced October 2016.

Comments: 9 pages, to be published in Modern Physics Letters A (2016)

Journal ref: Mod. Phys. Lett. A, Vol. 31, No. 34 (2016) 1650200

Quark Confinement, New Cosmic Expansion and General Yang-Mills Symmetry

Authors: Jong-** Hsu

Abstract: We discuss a unified model of quark confinement and new cosmic expansion with linear potentials based on a general $(SU_3)_{color} \times (U_1)_{baryon}$ symmetry. The phase functions in the usual gauge transformations are generalized to new `action integrals'. The general Yang-Mills transformations have group properties and reduce to usual gauge transformations in special cases. Both quarks and `… ▽ More We discuss a unified model of quark confinement and new cosmic expansion with linear potentials based on a general $(SU_3)_{color} \times (U_1)_{baryon}$ symmetry. The phase functions in the usual gauge transformations are generalized to new `action integrals'. The general Yang-Mills transformations have group properties and reduce to usual gauge transformations in special cases. Both quarks and `gauge bosons' are permanently confined by linear potentials. In this unified model of particle-cosmology, physics in the largest cosmos and that in the smallest quark system appear to both be dictated by the general Yang-Mills symmetry and characterized by a universal length. The basic force between two baryons is independent of distance. However, the cosmic repulsive force exerted on a baryonic supernova by a uniform sphere of galaxies is proportional to the distance from the center of the sphere. The new general Yang-Mills field may give a field-theoretic explanation of the accelerated cosmic expansion. The prediction could be tested experimentally by measuring the frequency shifts of supernovae at different distances. △ Less

Submitted 8 March, 2018; v1 submitted 24 August, 2016; originally announced September 2016.

Comments: 8 pages, to be published in the Chinese Physics C (2017). (to replace the previous submission by the same author.)

Hierarchical Attention Model for Improved Machine Comprehension of Spoken Content

Authors: Wei Fang, Jui-Yang Hsu, Hung-yi Lee, Lin-Shan Lee

Abstract: Multimedia or spoken content presents more attractive information than plain text content, but the former is more difficult to display on a screen and be selected by a user. As a result, accessing large collections of the former is much more difficult and time-consuming than the latter for humans. It's therefore highly attractive to develop machines which can automatically understand spoken conten… ▽ More Multimedia or spoken content presents more attractive information than plain text content, but the former is more difficult to display on a screen and be selected by a user. As a result, accessing large collections of the former is much more difficult and time-consuming than the latter for humans. It's therefore highly attractive to develop machines which can automatically understand spoken content and summarize the key information for humans to browse over. In this endeavor, a new task of machine comprehension of spoken content was proposed recently. The initial goal was defined as the listening comprehension test of TOEFL, a challenging academic English examination for English learners whose native languages are not English. An Attention-based Multi-hop Recurrent Neural Network (AMRNN) architecture was also proposed for this task, which considered only the sequential relationship within the speech utterances. In this paper, we propose a new Hierarchical Attention Model (HAM), which constructs multi-hopped attention mechanism over tree-structured rather than sequential representations for the utterances. Improved comprehension performance robust with respect to ASR errors were obtained. △ Less

Submitted 1 January, 2017; v1 submitted 28 August, 2016; originally announced August 2016.

Comments: Copyright 2016 IEEE. Published in the 2016 IEEE Workshop on Spoken Language Technology (SLT 2016)

Coupling proofs are probabilistic product programs

Authors: Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Abstract: Couplings are a powerful mathematical tool for reasoning about pairs of probabilistic processes. Recent developments in formal verification identify a close connection between couplings and pRHL, a relational program logic motivated by applications to provable security, enabling formal construction of couplings from the probability theory literature. However, existing work using pRHL merely shows… ▽ More Couplings are a powerful mathematical tool for reasoning about pairs of probabilistic processes. Recent developments in formal verification identify a close connection between couplings and pRHL, a relational program logic motivated by applications to provable security, enabling formal construction of couplings from the probability theory literature. However, existing work using pRHL merely shows existence of a coupling and does not give a way to prove quantitative properties about the coupling, which are need to reason about mixing and convergence of probabilistic processes. Furthermore, pRHL is inherently incomplete, and is not able to capture some advanced forms of couplings such as shift couplings. We address both problems as follows. First, we define an extension of pRHL, called xpRHL, which explicitly constructs the coupling in a pRHL derivation in the form of a probabilistic product program that simulates two correlated runs of the original program. Existing verification tools for probabilistic programs can then be directly applied to the probabilistic product to prove quantitative properties of the coupling. Second, we equip pRHL with a new rule for while loops, where reasoning can freely mix synchronized and unsynchronized loop iterations. Our proof rule can capture examples of shift couplings, and the logic is relatively complete for deterministic programs. We show soundness of xpRHL and use it to analyze two classes of examples. First, we verify rapid mixing using different tools from coupling: standard coupling, shift coupling, and path coupling, a compositional principle for combining local couplings into a global coupling. Second, we verify (approximate) equivalence between a source and an optimized program for several instances of loop optimizations from the literature. △ Less

Submitted 7 November, 2016; v1 submitted 12 July, 2016; originally announced July 2016.

Method for Transferring High-Mobility CVD-Grown Graphene with Perfluoropolymers

Authors: Jianan Li, Jen-Feng Hsu, Hyungwoo Lee, Shivendra Tripathi, Qing Guo, Lu Chen, Mengchen Huang, Shonali Dhingra, Jung-Woo Lee, Chang-Beom Eom, Patrick Irvin, Jeremy Levy, Brian D'Urso

Abstract: The transfer of graphene grown by chemical vapor deposition (CVD) using amorphous polymers represents a widely implemented method for graphene-based electronic device fabrication. However, the most commonly used polymer, poly(methyl methacrylate) (PMMA), leaves a residue on the graphene that limits the mobility. Here we report a method for graphene transfer and patterning that employs a perfluorop… ▽ More The transfer of graphene grown by chemical vapor deposition (CVD) using amorphous polymers represents a widely implemented method for graphene-based electronic device fabrication. However, the most commonly used polymer, poly(methyl methacrylate) (PMMA), leaves a residue on the graphene that limits the mobility. Here we report a method for graphene transfer and patterning that employs a perfluoropolymer---Hyflon---as a transfer handle and to protect graphene against contamination from photoresists or other polymers. CVD-grown graphene transferred this way onto LaAlO$_3$/SrTiO$_3$ heterostructures is atomically clean, with high mobility (~30,000 cm$^2$V$^{-1}$s$^{-1}$) near the Dirac point at 2 K and clear, quantized Hall and magneto-resistance. Local control of the LaAlO$_3$/SrTiO$_3$ interfacial metal-insulator transition---through the graphene---is preserved with this transfer method. The use of perfluoropolymers such as Hyflon with CVD-grown graphene and other 2D materials can readily be implemented with other polymers or photoresists. △ Less

Submitted 28 June, 2016; originally announced June 2016.

Comments: 6 pages, 4 figures

Advanced Probabilistic Couplings for Differential Privacy

Authors: Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Abstract: Differential privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information. Several tools have been developed for the formal verification of differentially private algorithms, including program logics and type systems. However, these tools do not capture fundamental techniques that have emerged… ▽ More Differential privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information. Several tools have been developed for the formal verification of differentially private algorithms, including program logics and type systems. However, these tools do not capture fundamental techniques that have emerged in recent years, and cannot be used for reasoning about cutting-edge differentially private algorithms. Existing techniques fail to handle three broad classes of algorithms: 1) algorithms where privacy depends accuracy guarantees, 2) algorithms that are analyzed with the advanced composition theorem, which shows slower growth in the privacy cost, 3) algorithms that interactively accept adaptive inputs. We address these limitations with a new formalism extending apRHL, a relational program logic that has been used for proving differential privacy of non-interactive algorithms, and incorporating aHL, a (non-relational) program logic for accuracy properties. We illustrate our approach through a single running example, which exemplifies the three classes of algorithms and explores new variants of the Sparse Vector technique, a well-studied algorithm from the privacy literature. We implement our logic in EasyCrypt, and formally verify privacy. We also introduce a novel coupling technique called \emph{optimal subset coupling} that may be of independent interest. △ Less

Submitted 17 August, 2016; v1 submitted 22 June, 2016; originally announced June 2016.

Alternator Coins

Authors: Benjamin Chen, Ezra Erives, Leon Fan, Michael Gerovitch, Jonathan Hsu, Tanya Khovanova, Neil Malur, Ashwin Padaki, Nastia Polina, Will Sun, Jacob Tan, Andrew The

Abstract: We introduce a new type of coin: \textit{the alternator}. The alternator can pretend to be either a real or a fake coin (which is lighter than a real one). Each time it is put on a balance scale it switches between pretending to be either a real coin or a fake one. In this paper, we solve the following problem: You are given $N$ coins that look identical, but one of them is the alternator. All r… ▽ More We introduce a new type of coin: \textit{the alternator}. The alternator can pretend to be either a real or a fake coin (which is lighter than a real one). Each time it is put on a balance scale it switches between pretending to be either a real coin or a fake one. In this paper, we solve the following problem: You are given $N$ coins that look identical, but one of them is the alternator. All real coins weigh the same. You have a balance scale which you can use to find the alternator. What is the smallest number of weighings that guarantees that you will find the alternator? △ Less

Submitted 17 May, 2016; originally announced May 2016.

Comments: 10 pages

MSC Class: 05A15; 00A08

Discovering Effect Modification in an Observational Study of Surgical Mortality at Hospitals with Superior Nursing

Authors: Kwonsang Lee, Dylan S. Small, Jesse Y. Hsu, Jeffrey H. Silber, Paul R. Rosenbaum

Abstract: There is effect modification if the magnitude or stability of a treatment effect varies systematically with the level of an observed covariate. A larger or more stable treatment effect is typically less sensitive to bias from unmeasured covariates, so it is important to recognize effect modification when it is present. We illustrate a recent proposal for conducting a sensitivity analysis that empi… ▽ More There is effect modification if the magnitude or stability of a treatment effect varies systematically with the level of an observed covariate. A larger or more stable treatment effect is typically less sensitive to bias from unmeasured covariates, so it is important to recognize effect modification when it is present. We illustrate a recent proposal for conducting a sensitivity analysis that empirically discovers effect modification by exploratory methods, but controls the family-wise error rate in discovered groups. The example concerns a study of mortality and use of the intensive care unit in 23,715 matched pairs of two Medicare patients, one of whom underwent surgery at a hospital identified for superior nursing, the other at a conventional hospital. The pairs were matched exactly for 130 four-digit ICD-9 surgical procedure codes and balanced 172 observed covariates. The pairs were then split into five groups of pairs by CART in its effort to locate effect modification. The evidence of a beneficial effect of magnet hospitals on mortality is least sensitive to unmeasured biases in a large group of patients undergoing rather serious surgical procedures, but in the absence of other life-threatening conditions, such as a comorbidity of congestive heart failure or an emergency admission leading to surgery. △ Less

Submitted 8 December, 2016; v1 submitted 12 May, 2016; originally announced May 2016.

Comments: 20 pages, 1 figure

Synthesizing Probabilistic Invariants via Doob's Decomposition

Authors: Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu

Abstract: When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then apply the optional stop** theorem in order to infer properties at termination time. One of the main challenges, then, is to systematically find martingales. We propose a novel procedure to synthesize martingale expr… ▽ More When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then apply the optional stop** theorem in order to infer properties at termination time. One of the main challenges, then, is to systematically find martingales. We propose a novel procedure to synthesize martingale expressions from an arbitrary initial expression. Contrary to state-of-the-art approaches, we do not rely on constraint solving. Instead, we use a symbolic construction based on Doob's decomposition. This procedure can produce very complex martingales, expressed in terms of conditional expectations. We show how to automatically generate and simplify these martingales, as well as how to apply the optional stop** theorem to infer properties at termination time. This last step typically involves some simplification steps, and is usually done manually in current approaches. We implement our techniques in a prototype tool and demonstrate our process on several classical examples. Some of them go beyond the capability of current semi-automatic approaches. △ Less

Submitted 9 May, 2016; originally announced May 2016.

Differentially Private Bayesian Programming

Authors: Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesùs Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub

Abstract: We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic programming language with constructs for performing Bayesian inference. Then, differential privacy of programs is established using a relational refinement type system, in which refinements on proba… ▽ More We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic programming language with constructs for performing Bayesian inference. Then, differential privacy of programs is established using a relational refinement type system, in which refinements on probability types are indexed by a metric on distributions. Our framework leverages recent developments in Bayesian inference, probabilistic programming languages, and in relational refinement types. We demonstrate the expressiveness of PrivInfer by verifying privacy for several examples of private Bayesian inference. △ Less

Submitted 17 August, 2016; v1 submitted 1 May, 2016; originally announced May 2016.

Cooling the Motion of Diamond Nanocrystals in a Magneto-Gravitational Trap in High Vacuum

Authors: Jen-Feng Hsu, Peng Ji, Charles W. Lewandowski, Brian D'Urso

Abstract: Levitated diamond nanocrystals with nitrogen-vacancy (NV) centres in high vacuum have been proposed as a unique system for experiments in fundamental quantum mechanics, including the generation of large quantum superposition states and tests of quantum gravity. This system promises extreme isolation from its environment while providing quantum control and sensing through the NV centre spin. While… ▽ More Levitated diamond nanocrystals with nitrogen-vacancy (NV) centres in high vacuum have been proposed as a unique system for experiments in fundamental quantum mechanics, including the generation of large quantum superposition states and tests of quantum gravity. This system promises extreme isolation from its environment while providing quantum control and sensing through the NV centre spin. While optical trap** has been the most explored method of levitation, recent results indicate that excessive optical heating of the nanodiamonds under vacuum may make the method impractical with currently available materials. Here, we study an alternative magneto-gravitational trap for diamagnetic particles, such as diamond nanocrystals, with stable levitation from atmospheric pressure to high vacuum. Magnetic field gradients from permanent magnets confine the particle in two dimensions, while confinement in the third dimension is gravitational. We demonstrate that feedback cooling of the centre-of-mass motion of a trapped nanodiamond cluster results in cooling of one degree of freedom to less than 1 K. △ Less

Submitted 1 May, 2016; v1 submitted 30 March, 2016; originally announced March 2016.

Comments: 8 pages, 5 figures, and 2 pages of supplementary information. One Reference was added. Typographical errors are corrected. Figure file format was changed for compactness

Journal ref: Scientific Reports 6, Article number: 30125 (2016)

Who Is Guilty?

Authors: Benjamin Chen, Ezra Erives, Leon Fan, Michael Gerovitch, Jonathan Hsu, Tanya Khovanova, Neil Malur, Ashwin Padaki, Nastia Polina, Will Sun, Jacob Tan, Andrew The

Abstract: We discuss a generalization of logic puzzles in which truth-tellers and liars are allowed to deviate from their pattern in case of one particular question: "Are you guilty?" We discuss a generalization of logic puzzles in which truth-tellers and liars are allowed to deviate from their pattern in case of one particular question: "Are you guilty?" △ Less

Submitted 23 March, 2016; originally announced March 2016.

Comments: 11 pages

MSC Class: 00A08; 03B99

A program logic for union bounds

Authors: Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Abstract: We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms, the union bound allows flexible and compositional reasoning over possible ways an algorithm may go wrong. It also enables a clean separation between reasoning abo… ▽ More We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms, the union bound allows flexible and compositional reasoning over possible ways an algorithm may go wrong. It also enables a clean separation between reasoning about probabilities and reasoning about events, which are expressed as standard first-order formulas in our logic. Notably, assertions in our logic are non-probabilistic, even though we can conclude probabilistic facts from the judgments. Our logic can also prove accuracy properties for interactive programs, where the program must produce intermediate outputs as soon as pieces of the input arrive, rather than accessing the entire input at once. This setting also enables adaptivity, where later inputs may depend on earlier intermediate outputs. We show how to prove accuracy for several examples from the differential privacy literature, both interactive and non-interactive. △ Less

Submitted 8 November, 2019; v1 submitted 18 February, 2016; originally announced February 2016.

Room-temperature quantum transport signatures in graphene/LaAlO3/SrTiO3 heterostructures

Authors: Giriraj Jnawali, Mengchen Huang, Jen-Feng Hsu, Hyungwoo Lee, Jung-Woo Lee, Patrick Irvin, Chang-Beom Eom, Brian D'Urso, Jeremy Levy

Abstract: The pseudospin quantum degree of freedom is one of the most remarkable properties of graphene that distinguishes it from ordinary two-dimensional metals and semiconductors. Pseudospin quantum interference leads to weak antilocalization (WAL) and is influenced strongly by point defects and thermal perturbations that break chirality and destroy phase coherence. Preserving and manipulating quantum tr… ▽ More The pseudospin quantum degree of freedom is one of the most remarkable properties of graphene that distinguishes it from ordinary two-dimensional metals and semiconductors. Pseudospin quantum interference leads to weak antilocalization (WAL) and is influenced strongly by point defects and thermal perturbations that break chirality and destroy phase coherence. Preserving and manipulating quantum transport properties up to room temperature is key to realizing practical pseudospin-based graphene devices. Here we report fabrication and transport characterization of graphene field-effect devices on a complex-oxide heterostructure, LaAlO3/SrTiO3. Signatures of WAL, a consequence of pseudospin quantum interference, persist up to room temperature. The LaAlO3/SrTiO3 substrate plays a critical role in suppressing short-range impurity scattering and electron-phonon coupling. The observation of quantum transport signatures at room temperature is unique to this system and presents new opportunities for the development of pseudospin-based devices and novel multifunctional devices that couple to the complex-oxide interface. △ Less

Submitted 2 July, 2016; v1 submitted 9 February, 2016; originally announced February 2016.

Comments: 38 pages, 5 figures (Suppl. Info. 17 pages, 10 figures, 1 table)

Proving Differential Privacy via Probabilistic Couplings

Authors: Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Abstract: In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based on the observation that differential privacy has deep connections with a generalization of probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition th… ▽ More In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based on the observation that differential privacy has deep connections with a generalization of probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition theorem is not helpful, we can often prove privacy by a coupling argument. We demonstrate our methods on two algorithms: the Exponential mechanism and the Above Threshold algorithm, the critical component of the famous Sparse Vector algorithm. We verify these examples in a relational program logic apRHL+, which can construct approximate couplings. This logic extends the existing apRHL logic with more general rules for the Laplace mechanism and the one-sided Laplace mechanism, and new structural rules enabling pointwise reasoning about privacy; all the rules are inspired by the connection with coupling. While our paper is presented from a formal verification perspective, we believe that its main insight is of independent interest for the differential privacy community. △ Less

Submitted 14 March, 2021; v1 submitted 19 January, 2016; originally announced January 2016.

ACM Class: F.3.1

Do Prices Coordinate Markets?

Authors: Justin Hsu, Jamie Morgenstern, Ryan Rogers, Aaron Roth, Rakesh Vohra

Abstract: Walrasian equilibrium prices can be said to coordinate markets: They support a welfare optimal allocation in which each buyer is buying bundle of goods that is individually most preferred. However, this clean story has two caveats. First, the prices alone are not sufficient to coordinate the market, and buyers may need to select among their most preferred bundles in a coordinated way to find a fea… ▽ More Walrasian equilibrium prices can be said to coordinate markets: They support a welfare optimal allocation in which each buyer is buying bundle of goods that is individually most preferred. However, this clean story has two caveats. First, the prices alone are not sufficient to coordinate the market, and buyers may need to select among their most preferred bundles in a coordinated way to find a feasible allocation. Second, we don't in practice expect to encounter exact equilibrium prices tailored to the market, but instead only approximate prices, somehow encoding "distributional" information about the market. How well do prices work to coordinate markets when tie-breaking is not coordinated, and they encode only distributional information? We answer this question. First, we provide a genericity condition such that for buyers with Matroid Based Valuations, overdemand with respect to equilibrium prices is at most 1, independent of the supply of goods, even when tie-breaking is done in an uncoordinated fashion. Second, we provide learning-theoretic results that show that such prices are robust to changing the buyers in the market, so long as all buyers are sampled from the same (unknown) distribution. △ Less

Submitted 22 June, 2016; v1 submitted 3 November, 2015; originally announced November 2015.

Relational reasoning via probabilistic coupling

Authors: Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub

Abstract: Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance---a… ▽ More Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance---a probabilistic version of a monotonicity property. While the mathematical definition of coupling looks rather complex and cumbersome to manipulate, we show that the relational program logic pRHL---the logic underlying the EasyCrypt cryptographic proof assistant---already internalizes a generalization of probabilistic coupling. With this insight, constructing couplings is no harder than constructing logical proofs. We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verify several couplings in EasyCrypt. △ Less

Submitted 14 October, 2015; v1 submitted 11 September, 2015; originally announced September 2015.

Online Assignment of Heterogeneous Tasks in Crowdsourcing Markets

Authors: Sepehr Assadi, Justin Hsu, Shahin Jabbari

Abstract: We investigate the problem of heterogeneous task assignment in crowdsourcing markets from the point of view of the requester, who has a collection of tasks. Workers arrive online one by one, and each declare a set of feasible tasks they can solve, and desired payment for each feasible task. The requester must decide on the fly which task (if any) to assign to the worker, while assigning workers on… ▽ More We investigate the problem of heterogeneous task assignment in crowdsourcing markets from the point of view of the requester, who has a collection of tasks. Workers arrive online one by one, and each declare a set of feasible tasks they can solve, and desired payment for each feasible task. The requester must decide on the fly which task (if any) to assign to the worker, while assigning workers only to feasible tasks. The goal is to maximize the number of assigned tasks with a fixed overall budget. We provide an online algorithm for this problem and prove an upper bound on the competitive ratio of this algorithm against an arbitrary (possibly worst-case) sequence of workers who want small payments relative to the requester's total budget. We further show an almost matching lower bound on the competitive ratio of any algorithm in this setting. Finally, we propose a different algorithm that achieves an improved competitive ratio in the random permutation model, where the order of arrival of the workers is chosen uniformly at random. Apart from these strong theoretical guarantees, we carry out experiments on simulated data which demonstrates the practical applicability of our algorithms. △ Less

Submitted 14 August, 2015; originally announced August 2015.

Comments: Extended version of paper in HCOMP 2015

Efficient and Parsimonious Agnostic Active Learning

Authors: Tzu-Kuo Huang, Alekh Agarwal, Daniel J. Hsu, John Langford, Robert E. Schapire

Abstract: We develop a new active learning algorithm for the streaming setting satisfying three important properties: 1) It provably works for any classifier representation and classification problem including those with severe noise. 2) It is efficiently implementable with an ERM oracle. 3) It is more aggressive than all previous approaches satisfying 1 and 2. To do this we create an algorithm based on a n… ▽ More We develop a new active learning algorithm for the streaming setting satisfying three important properties: 1) It provably works for any classifier representation and classification problem including those with severe noise. 2) It is efficiently implementable with an ERM oracle. 3) It is more aggressive than all previous approaches satisfying 1 and 2. To do this we create an algorithm based on a newly defined optimization problem and analyze it. We also conduct the first experimental analysis of all efficient agnostic active learning algorithms, evaluating their strengths and weaknesses in different settings. △ Less

Submitted 7 January, 2016; v1 submitted 29 June, 2015; originally announced June 2015.

Loading an Optical Trap with Diamond Nanocrystals Containing Nitrogen-Vacancy Centers from a Surface

Authors: Jen-Feng Hsu, Peng Ji, M. V. Gurudev Dutt, Brian R. D'Urso

Abstract: We present a simple and effective method of loading particles into an optical trap in air at atmospheric pressure. Material which is highly absorptive at the trap** laser wavelength, such as tartrazine dye, is used as media to attach photoluminescent diamond nanocrystals. The mix is burnt into a cloud of air-borne particles as the material is swept near the trap** laser focus on a glass slide.… ▽ More We present a simple and effective method of loading particles into an optical trap in air at atmospheric pressure. Material which is highly absorptive at the trap** laser wavelength, such as tartrazine dye, is used as media to attach photoluminescent diamond nanocrystals. The mix is burnt into a cloud of air-borne particles as the material is swept near the trap** laser focus on a glass slide. Particles are then trapped with the laser used for burning or transferred to a second laser trap at a different wavelength. Evidence of successfully loading diamond nanocrystals into the trap presented includes high sensitivity of the photoluminecscence (PL) to an excitation laser at 520~nm wavelength and the PL spectra of the optically trapped particles. This method provides a convenient technique for the study of the nitrogen-vacancy (NV) centers contained in optically trapped diamond nanocrystals. △ Less

Submitted 26 June, 2015; originally announced June 2015.

Comments: 6 pages and 8 figures

Really Natural Linear Indexed Type Checking

Authors: Arthur Azevedo de Amorim, Emilio Jesús Gallego Arias, Marco Gaboardi, Justin Hsu

Abstract: Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy. A natural way to enhance the expressiveness of this approach is… ▽ More Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy. A natural way to enhance the expressiveness of this approach is by allowing the indices to depend on runtime information, in the spirit of dependent types. This approach is used in DFuzz, a language for differential privacy. The DFuzz type system relies on an index language supporting real and natural number arithmetic over constants and variables. Moreover, DFuzz uses a subty** mechanism to make types more flexible. By themselves, linearity, dependency, and subty** each require delicate handling when performing type checking or type inference; their combination increases this challenge substantially, as the features can interact in non-trivial ways. In this paper, we study the type-checking problem for DFuzz. We show how we can reduce type checking for (a simple extension of) DFuzz to constraint solving over a first-order theory of naturals and real numbers which, although undecidable, can often be handled in practice by standard numeric solvers. △ Less

Submitted 16 March, 2015; originally announced March 2015.

Computer-aided verification in mechanism design

Authors: Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub

Abstract: In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility and Bayesian incentive compatibility. These solution concepts relieve the (possibly unsophisticated) bidders from the need to engage in complicated strategizing. While incentive properties are simple to state, their proofs are specific to the mechanism and can be quite complex. This raises two co… ▽ More In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility and Bayesian incentive compatibility. These solution concepts relieve the (possibly unsophisticated) bidders from the need to engage in complicated strategizing. While incentive properties are simple to state, their proofs are specific to the mechanism and can be quite complex. This raises two concerns. From a practical perspective, checking a complex proof can be a tedious process, often requiring experts knowledgeable in mechanism design. Furthermore, from a modeling perspective, if unsophisticated agents are unconvinced of incentive properties, they may strategize in unpredictable ways. To address both concerns, we explore techniques from computer-aided verification to construct formal proofs of incentive properties. Because formal proofs can be automatically checked, agents do not need to manually check the properties, or even understand the proof. To demonstrate, we present the verification of a sophisticated mechanism: the generic reduction from Bayesian incentive compatible mechanism design to algorithm design given by Hartline, Kleinberg, and Malekian. This mechanism presents new challenges for formal verification, including essential use of randomness from both the execution of the mechanism and from the prior type distributions. As an immediate consequence, our work also formalizes Bayesian incentive compatibility for the entire family of mechanisms derived via this reduction. Finally, as an intermediate step in our formalization, we provide the first formal verification of incentive compatibility for the celebrated Vickrey-Clarke-Groves mechanism. △ Less

Submitted 24 December, 2016; v1 submitted 13 February, 2015; originally announced February 2015.

Jointly Private Convex Programming

Authors: Justin Hsu, Zhiyi Huang, Aaron Roth, Zhiwei Steven Wu

Abstract: In this paper we present an extremely general method for approximately solving a large family of convex programs where the solution can be divided between different agents, subject to joint differential privacy. This class includes multi-commodity flow problems, general allocation problems, and multi-dimensional knapsack problems, among other examples. The accuracy of our algorithm depends on the… ▽ More In this paper we present an extremely general method for approximately solving a large family of convex programs where the solution can be divided between different agents, subject to joint differential privacy. This class includes multi-commodity flow problems, general allocation problems, and multi-dimensional knapsack problems, among other examples. The accuracy of our algorithm depends on the \emph{number} of constraints that bind between individuals, but crucially, is \emph{nearly independent} of the number of primal variables and hence the number of agents who make up the problem. As the number of agents in a problem grows, the error we introduce often becomes negligible. We also consider the setting where agents are strategic and have preferences over their part of the solution. For any convex program in this class that maximizes \emph{social welfare}, there is a generic reduction that makes the corresponding optimization \emph{approximately dominant strategy truthful} by charging agents prices for resources as a function of the approximately optimal dual variables, which are themselves computed under differential privacy. Our results substantially expand the class of problems that are known to be solvable under both privacy and incentive constraints. △ Less

Submitted 5 November, 2014; v1 submitted 4 November, 2014; originally announced November 2014.

Subgroup Mixable Inference in Personalized Medicine, with an Application to Time-to-Event Outcomes

Authors: Ying Ding, Hui-Min Lin, Jason C. Hsu

Abstract: Measuring treatment efficacy in mixture of subgroups from a randomized clinical trial is a fundamental problem in personalized medicine development, in deciding whether to treat the entire patient population or to target a subgroup. We show that some commonly used efficacy measures are not suitable for a mixture population. We also show that, while it is important to adjust for imbalance in the da… ▽ More Measuring treatment efficacy in mixture of subgroups from a randomized clinical trial is a fundamental problem in personalized medicine development, in deciding whether to treat the entire patient population or to target a subgroup. We show that some commonly used efficacy measures are not suitable for a mixture population. We also show that, while it is important to adjust for imbalance in the data using least squares means (LSmeans) (not marginal means) estimation, the current practice of applying LSmeans to directly estimate the efficacy in a mixture population for any type of outcome is inappropriate. Proposing a new principle called {\em subgroup mixable estimation}, we establish the logical relationship among parameters that represent efficacy and develop a general inference procedure to confidently infer efficacy in subgroups and their mixtures. Using oncology studies with time-to-event outcomes as an example, we show that Hazard Ratio is not suitable for measuring efficacy in a mixture population, and provide alternative efficacy measures with a valid inference procedure. △ Less

Submitted 2 September, 2014; originally announced September 2014.

Comments: 5 figures, 6 tables

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Authors: Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub

Abstract: Mechanism design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlike typical programmatic properties, it is not sufficient for algorithms to merely satisfy the property---incentive properties are only useful if the strategic agents also believe this fact. Verification is an attractive… ▽ More Mechanism design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlike typical programmatic properties, it is not sufficient for algorithms to merely satisfy the property---incentive properties are only useful if the strategic agents also believe this fact. Verification is an attractive way to convince agents that the incentive properties actually hold, but mechanism design poses several unique challenges: interesting properties can be sophisticated relational properties of probabilistic computations involving expected values, and mechanisms may rely on other probabilistic properties, like differential privacy, to achieve their goals. We introduce a relational refinement type system, called $\mathsf{HOARe}^2$, for verifying mechanism design and differential privacy. We show that $\mathsf{HOARe}^2$ is sound w.r.t. a denotational semantics, and correctly models $(ε,δ)$-differential privacy; moreover, we show that it subsumes DFuzz, an existing linear dependent type system for differential privacy. Finally, we develop an SMT-based implementation of $\mathsf{HOARe}^2$ and use it to verify challenging examples of mechanism design, including auctions and aggregative games, and new proposed examples from differential privacy. △ Less

Submitted 29 October, 2014; v1 submitted 25 July, 2014; originally announced July 2014.

Proving differential privacy in Hoare logic

Authors: Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub

Abstract: Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output d… ▽ More Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output distributions of a probabilistic program on adjacent inputs. Like many 2-safety properties, differential privacy lies outside the scope of traditional verification techniques. Existing approaches to enforce privacy are based on intricate, non-conventional type systems, or customized relational logics. These approaches are difficult to implement and often cumbersome to use. We present an alternative approach that verifies differential privacy by standard, non-relational reasoning on non-probabilistic programs. Our approach transforms a probabilistic program into a non-probabilistic program which simulates two executions of the original program. We prove that if the target program is correct with respect to a Hoare specification, then the original probabilistic program is differentially private. We provide a variety of examples from the differential privacy literature to demonstrate the utility of our approach. Finally, we compare our approach with existing verification techniques for privacy. △ Less

Submitted 10 July, 2014; originally announced July 2014.

Comments: Published at the Computer Security Foundations Symposium (CSF), 2014

A confining quark model and new gauge symmetry

Authors: Jong-** Hsu

Abstract: We discuss a confining model for quark-antiquark system with a new color $SU_3$ gauge symmetry. New gauge transformations involve non-integrable phase factors and lead to the fourth-order gauge field equations and a linear potential. The massless gauge bosons have non-definite energies, which are not observable because they are permanently confined in quark systems by the linear potential. We use… ▽ More We discuss a confining model for quark-antiquark system with a new color $SU_3$ gauge symmetry. New gauge transformations involve non-integrable phase factors and lead to the fourth-order gauge field equations and a linear potential. The massless gauge bosons have non-definite energies, which are not observable because they are permanently confined in quark systems by the linear potential. We use the empirical potentials of charmonium to determine the coupling strength of the color charge $g_s$ and find $g_s^2/(4π) \approx 0.2.$ We discuss Feynman-Dyson rules for the confining quark model, which involve propagators with poles of order 2 associated with new gauge fields. The confining quark model may be renormalizable by power counting and compatible with perturbation theory. △ Less

Submitted 8 July, 2014; originally announced July 2014.

Comments: 10 pages

Journal ref: Modern Physics Letters A, Vol.29, No. 22 (2014) 1450120

A Confining Model for Charmonium and New Gauge Invariant Field Equations

Authors: Jong-** Hsu

Abstract: We discuss a confining model for charmonium in which the attractive force are derived from a new type of gauge field equation with a generalized $SU_3$ gauge symmetry. The new gauge transformations involve non-integrable phase factors with vector gauge functions $\om^a_μ(x)$. These transformations reduce to the usual $SU_3$ gauge transformations in the special case $\om^a_μ(x) = \p_μξ^a(x)$. Such… ▽ More We discuss a confining model for charmonium in which the attractive force are derived from a new type of gauge field equation with a generalized $SU_3$ gauge symmetry. The new gauge transformations involve non-integrable phase factors with vector gauge functions $\om^a_μ(x)$. These transformations reduce to the usual $SU_3$ gauge transformations in the special case $\om^a_μ(x) = \p_μξ^a(x)$. Such a generalized gauge symmetry leads to the fourth-order equations for new gauge fields and to the linear confining potentials. The fourth-order field equation implies that the corresponding massless gauge boson has non-definite energy. However, the new gauge boson is permanently confined in a quark system by the linear potential. We use the empirical potentials of the Cornell group for charmonium to obtain the coupling strength $f^2/(4π) \approx 0.19$ for the strong interaction. Such a confining model of quark dynamics could be compatible with perturbation. The model can be applied to other quark-antiquark systems. △ Less

Submitted 3 June, 2014; originally announced June 2014.

Comments: 6 pages

Journal ref: Eur. Phys. J. Plus (2014) 129: 108

Privately Solving Linear Programs

Authors: Justin Hsu, Aaron Roth, Tim Roughgarden, Jonathan Ullman

Abstract: In this paper, we initiate the systematic study of solving linear programs under differential privacy. The first step is simply to define the problem: to this end, we introduce several natural classes of private linear programs that capture different ways sensitive data can be incorporated into a linear program. For each class of linear programs we give an efficient, differentially private solver… ▽ More In this paper, we initiate the systematic study of solving linear programs under differential privacy. The first step is simply to define the problem: to this end, we introduce several natural classes of private linear programs that capture different ways sensitive data can be incorporated into a linear program. For each class of linear programs we give an efficient, differentially private solver based on the multiplicative weights framework, or we give an impossibility result. △ Less

Submitted 8 May, 2014; v1 submitted 14 February, 2014; originally announced February 2014.

A Generalization of Gauge Symmetry, Fourth-Order Gauge Field Equations and Accelerated Cosmic-Expansion

Authors: Jong-** Hsu

Abstract: A generalization of the usual gauge symmetry leads to fourth-order gauge field equations, which imply a new constant force independent of distances. The force associated with the new $U_1$ gauge symmetry is repulsive among baryons. Such a constant force based on baryon charge conservation gives a field-theoretic understanding of the accelerated cosmic-expansion in the observable portion of the uni… ▽ More A generalization of the usual gauge symmetry leads to fourth-order gauge field equations, which imply a new constant force independent of distances. The force associated with the new $U_1$ gauge symmetry is repulsive among baryons. Such a constant force based on baryon charge conservation gives a field-theoretic understanding of the accelerated cosmic-expansion in the observable portion of the universe dominated by baryon galaxies. In consistent with all conservation laws and known forces, a simple rotating `dumbbell model' of the universe is briefly discussed. △ Less

Submitted 14 February, 2014; originally announced February 2014.

Comments: 15 pages, to be published in Modern Physics Letters A, 29 (2014)

Journal ref: Mod. Phys. Lett. A, Vol. 29, No. 6 (2014) 1450031

Differential Privacy: An Economic Method for Choosing Epsilon

Authors: Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan, Benjamin C. Pierce, Aaron Roth

Abstract: Differential privacy is becoming a gold standard for privacy research; it offers a guaranteed bound on loss of privacy due to release of query results, even under worst-case assumptions. The theory of differential privacy is an active research area, and there are now differentially private algorithms for a wide range of interesting problems. However, the question of when differential privacy wor… ▽ More Differential privacy is becoming a gold standard for privacy research; it offers a guaranteed bound on loss of privacy due to release of query results, even under worst-case assumptions. The theory of differential privacy is an active research area, and there are now differentially private algorithms for a wide range of interesting problems. However, the question of when differential privacy works in practice has received relatively little attention. In particular, there is still no rigorous method for choosing the key parameter $ε$, which controls the crucial tradeoff between the strength of the privacy guarantee and the accuracy of the published results. In this paper, we examine the role that these parameters play in concrete applications, identifying the key questions that must be addressed when choosing specific values. This choice requires balancing the interests of two different parties: the data analyst and the prospective participant, who must decide whether to allow their data to be included in the analysis. We propose a simple model that expresses this balance as formulas over a handful of parameters, and we use our model to choose $ε$ on a series of simple statistical studies. We also explore a surprising insight: in some circumstances, a differentially private study can be more accurate than a non-private study for the same cost, under our model. Finally, we discuss the simplifying assumptions in our model and outline a research agenda for possible refinements. △ Less

Submitted 13 February, 2014; originally announced February 2014.

Dual Query: Practical Private Query Release for High Dimensional Data

Authors: Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Zhiwei Steven Wu

Abstract: We present a practical, differentially private algorithm for answering a large number of queries on high dimensional datasets. Like all algorithms for this task, ours necessarily has worst-case complexity exponential in the dimension of the data. However, our algorithm packages the computationally hard step into a concisely defined integer program, which can be solved non-privately using standard… ▽ More We present a practical, differentially private algorithm for answering a large number of queries on high dimensional datasets. Like all algorithms for this task, ours necessarily has worst-case complexity exponential in the dimension of the data. However, our algorithm packages the computationally hard step into a concisely defined integer program, which can be solved non-privately using standard solvers. We prove accuracy and privacy theorems for our algorithm, and then demonstrate experimentally that our algorithm performs well in practice. For example, our algorithm can efficiently and accurately answer millions of queries on the Netflix dataset, which has over 17,000 attributes; this is an improvement on the state of the art by multiple orders of magnitude. △ Less

Submitted 18 November, 2015; v1 submitted 6 February, 2014; originally announced February 2014.

Journal ref: Journal of Privacy and Confidentiality 7(2) 53--77 (2017)

Thim's Experiment and Exact Rotational Space-Time Transformations

Authors: Leonardo Hsu, Jong-** Hsu

Abstract: Thim measured the transverse Doppler shift using a system consisting of a stationary antenna and pickup, in addition to a number of intermediate antennas mounted on the rim of a rotating disk. No such shift was detected, although the experiment should have had enough sensitivity to measure it, as predicted by the Lorentz transformations. However, using the Lorentz transformations to analyze the re… ▽ More Thim measured the transverse Doppler shift using a system consisting of a stationary antenna and pickup, in addition to a number of intermediate antennas mounted on the rim of a rotating disk. No such shift was detected, although the experiment should have had enough sensitivity to measure it, as predicted by the Lorentz transformations. However, using the Lorentz transformations to analyze the results of experiments involving circular motion, while commonly done, is inappropriate because such an analysis involves non-inertial frames, which are outside the range of validity of special relativity. In this paper, we re-analyze Thim's experiment using exact rotational space-time transformations, finding that his null result is consistent with theoretical predictions. △ Less

Submitted 30 January, 2014; originally announced January 2014.

Comments: 8 pages

Journal ref: Eur. Phys. J. Plus (2014) 129: 16

Private Matchings and Allocations

Authors: Justin Hsu, Zhiyi Huang, Aaron Roth, Tim Roughgarden, Zhiwei Steven Wu

Abstract: We consider a private variant of the classical allocation problem: given k goods and n agents with individual, private valuation functions over bundles of goods, how can we partition the goods amongst the agents to maximize social welfare? An important special case is when each agent desires at most one good, and specifies her (private) value for each good: in this case, the problem is exactly the… ▽ More We consider a private variant of the classical allocation problem: given k goods and n agents with individual, private valuation functions over bundles of goods, how can we partition the goods amongst the agents to maximize social welfare? An important special case is when each agent desires at most one good, and specifies her (private) value for each good: in this case, the problem is exactly the maximum-weight matching problem in a bipartite graph. Private matching and allocation problems have not been considered in the differential privacy literature, and for good reason: they are plainly impossible to solve under differential privacy. Informally, the allocation must match agents to their preferred goods in order to maximize social welfare, but this preference is exactly what agents wish to hide. Therefore, we consider the problem under the relaxed constraint of joint differential privacy: for any agent i, no coalition of agents excluding i should be able to learn about the valuation function of agent i. In this setting, the full allocation is no longer published---instead, each agent is told what good to get. We first show that with a small number of identical copies of each good, it is possible to efficiently and accurately solve the maximum weight matching problem while guaranteeing joint differential privacy. We then consider the more general allocation problem, when bidder valuations satisfy the gross substitutes condition. Finally, we prove that the allocation problem cannot be solved to non-trivial accuracy under joint differential privacy without requiring multiple copies of each type of good. △ Less

Submitted 19 August, 2016; v1 submitted 12 November, 2013; originally announced November 2013.

Comments: Journal version published in SIAM Journal on Computation; an extended abstract appeared in STOC 2014

Journal ref: SIAM Journal on Computing 45(6) 1953--1984 (2016)

Exact Space-Time Gauge Symmetry of Gravity, Its Couplings and Approximate Internal Symmetries in a Total-Unified Model

Authors: Jong-** Hsu

Abstract: Gravitational field is the manifestation of space-time translational ($T_4$) gauge symmetry, which enables gravitational interaction to be unified with the strong and the electroweak interactions. Such a total-unified model is based on a generalized Yang-Mills framework in flat space-time. Following the idea of Glashow-Salam-Ward-Weinberg, we gauge the groups… ▽ More Gravitational field is the manifestation of space-time translational ($T_4$) gauge symmetry, which enables gravitational interaction to be unified with the strong and the electroweak interactions. Such a total-unified model is based on a generalized Yang-Mills framework in flat space-time. Following the idea of Glashow-Salam-Ward-Weinberg, we gauge the groups $T_4 \times (SU_3)_{color} \times SU_2 \times U_1\times U_{1b}$ on equal-footing, so that we have the total-unified gauge covariant derivative ${\bf \d}_μ = \p_μ - igφ_μ^ν p_ν+ig_{s}{G_μ^{a}}(\ld^a/2) +if{W_μ^{k}}{t^k} + if' U_μt_{o} + ig_{b}B_μ$. The generators of the external $T_4$ group have the representation $p_μ=i\p_μ$, which differs from other generators of all internal groups, which have constant matrix representations. Consequently, the total-unified model leads to the following new results: (a) All internal $(SU_3)_{color}, SU_2, U_1$ and baryonic $U_{1b}$ gauge symmetries have extremely small violations due to the gravitational interaction. (b) The $T_4$ gauge symmetry remains exact and dictates the universal coupling of gravitons. (c) Such a gravitational violation of internal gauge symmetries leads to modified eikonal and Hamilton-Jacobi type equations, which are obtained in the geometric-optics limit and involve effective Riemann metric tensors. (d) The rules for Feynman diagrams involving new couplings of photon-graviton, gluon-graviton and quark-gaviton are obtained. △ Less

Submitted 17 September, 2013; originally announced September 2013.

Comments: 19 pages, to be published in the Chinese Journal of Physics, 2013

Exact Rotational Space-time Transformations, Davies-Jennison Experiments and Limiting Lorentz-Poincaré Invariance

Authors: Leonardo Hsu, Jong-** Hsu

Abstract: Jennison deduced from the rotational experiments that a rotating radius $r_r$ measured by the rotating observer is contracted by $r_r = r(1-\om^2 r^2/c^2)^{1/2}$, compared with the radius $r$ measured in an inertial frame. This conclusion differs from the result based on Lorentz transformations. Since rotational frames are not equivalent to inertial frames, we analyze the rotational experiments by… ▽ More Jennison deduced from the rotational experiments that a rotating radius $r_r$ measured by the rotating observer is contracted by $r_r = r(1-\om^2 r^2/c^2)^{1/2}$, compared with the radius $r$ measured in an inertial frame. This conclusion differs from the result based on Lorentz transformations. Since rotational frames are not equivalent to inertial frames, we analyze the rotational experiments by using the exact rotational space-time transformations rather than the Lorentz transformations. We derive exact rotational transformations on the basis of the principle of limiting Lorentz-Poincaré invariance. The exact rotational transformations form a pseudo-group rather than the usual Lie group. They support Jennison's contraction of a rotating radius and are consistent with two Davies-Jennison experiments. We also suggest new experimental tests for the exact rotational transformations. △ Less

Submitted 2 July, 2013; originally announced July 2013.

Comments: 23 pages, to be published in Euro. Phys. J. Plus, vol. 128 (2013)

Journal ref: Eur. Phys. J. Plus (2013) 128:74

Creating high density ensembles of nitrogen-vacancy centers in nitrogen-rich type Ib nanodiamonds

Authors: Long-Jyun Su, Chia-Yi Fang, Yu-Tang Chang, Kuan-Ming Chen, Yueh-Chung Yu, Jui-Hung Hsu, Huan-Cheng Chang

Abstract: This work explores the possibility of increasing the density of negatively charged nitrogen-vacancy centers [NV-] in nanodiamonds using nitrogen-rich type Ib diamond powders as the starting materials. The nanodiamonds (10 - 100 nm in diameters) were prepared by ball-milling of microdiamonds, in which the density of neutral and automatically dispersed nitrogen atoms [N0] was measured by diffuse ref… ▽ More This work explores the possibility of increasing the density of negatively charged nitrogen-vacancy centers [NV-] in nanodiamonds using nitrogen-rich type Ib diamond powders as the starting materials. The nanodiamonds (10 - 100 nm in diameters) were prepared by ball-milling of microdiamonds, in which the density of neutral and automatically dispersed nitrogen atoms [N0] was measured by diffuse reflectance infrared Fourier transform spectroscopy (DRIFT). A systematic measurement for the fluorescence intensities and lifetimes of the crushed monocrystalline diamonds as a function of [N0] indicated that the [NV-] increases nearly linearly with [N0] at 100 - 200 ppm. The trend, however, failed to continue for nanodiamonds with higher [N0] (up to 390 ppm) but poorer crystallinity. We attribute the result to a combined effect of fluorescence quenching as well as the lower conversion efficiency of vacancies to NV- due to the presence of more impurities and defects in these as-grown diamond crystallites. The principles and practice of fabricating brighter and smaller fluorescent nanodiamonds (FNDs) are discussed. △ Less

Submitted 6 June, 2013; originally announced June 2013.

Compression as a universal principle of animal behavior

Authors: R. Ferrer-i-Cancho, A. Hernández-Fernández, D. Lusseau, G. Agoramoorthy, M. J. Hsu, S. Semple

Abstract: A key aim in biology and psychology is to identify fundamental principles underpinning the behavior of animals, including humans. Analyses of human language and the behavior of a range of non-human animal species have provided evidence for a common pattern underlying diverse behavioral phenomena: words follow Zipf's law of brevity (the tendency of more frequently used words to be shorter), and con… ▽ More A key aim in biology and psychology is to identify fundamental principles underpinning the behavior of animals, including humans. Analyses of human language and the behavior of a range of non-human animal species have provided evidence for a common pattern underlying diverse behavioral phenomena: words follow Zipf's law of brevity (the tendency of more frequently used words to be shorter), and conformity to this general pattern has been seen in the behavior of a number of other animals. It has been argued that the presence of this law is a sign of efficient coding in the information theoretic sense. However, no strong direct connection has been demonstrated between the law and compression, the information theoretic principle of minimizing the expected length of a code. Here we show that minimizing the expected code length implies that the length of a word cannot increase as its frequency increases. Furthermore, we show that the mean code length or duration is significantly small in human language, and also in the behavior of other species in all cases where agreement with the law of brevity has been found. We argue that compression is a general principle of animal behavior, that reflects selection for efficiency of coding. △ Less

Submitted 25 March, 2013; originally announced March 2013.

Comments: This is the pre-proofed version. The published version will be available at http://onlinelibrary.wiley.com/journal/10.1111/%28ISSN%291551-6709

Experimental Tests on Yang-Mills Gravity with Accurate Measurements of the Deflection of Light

Authors: Jong-** Hsu

Abstract: In the geometric-optics limit, Yang-Mills gravity with space-time translational gauge symmetry predicts $\D φ=7Gm/(2R) \approx 1.53''$ for the deflection of a light ray by the sun. The result, which is about 12% smaller than that in the conventional theory, is consistent with experiments involving optical frequencies that had an accuracy of 10-20%. In the geometric-optics limit, Yang-Mills gravity with space-time translational gauge symmetry predicts $\D φ=7Gm/(2R) \approx 1.53''$ for the deflection of a light ray by the sun. The result, which is about 12% smaller than that in the conventional theory, is consistent with experiments involving optical frequencies that had an accuracy of 10-20%. △ Less

Submitted 27 February, 2013; originally announced February 2013.

Comments: 7 pages. To be published in The European Physical Journal - Plus (2013)

Journal ref: Eur. Phys. J. Plus (2013) 128: 31