Search

Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism., Comment: Draft version

The calculations of the first and the second ionization potentials of lawrencium and lutetium and the electron affinity of lawrencium are performed within the relativistic coupled cluster framework. These results are corrected by including the contributions of extrapolation to the complete basis set limit and higher order contributions due to relativity and electron correlation. The excellent agreement between our predictions of the ionization potentials of Lu and Lr and experimental values supports the accuracy of our predictions of the second ionization potential and the electron affinity of Lr.

We theoretically investigate nonequilibrium spin fluctuations in a ferromagnet induced by a light pulse. Using a Lindblad equation consistent with the Landau-Lifshitz-Gilbert equation, we compute the autocorrelation function of magnetization. Our analysis reveals that this function comprises both thermal and nonequilibrium components. To examine the latter in detail, we introduce a Fano factor similar to nonequilibrium current noise in electronic circuits. We demonstrate that this factor encapsulates insights into the transfer of spin units to the environment. Our findings lay the groundwork for nonequilibrium spin noise spectroscopy, offering valuable insights into spin relaxation dynamics., Comment: 11 pages, 3 figures

We propose a formal language for describing and explaining statistical causality. Concretely, we define Statistical Causality Language (StaCL) for expressing causal effects and specifying the requirements for causal inference. StaCL incorporates modal operators for interventions to express causal properties between probability distributions in different possible worlds in a Kripke model. We formalize axioms for probability distributions, interventions, and causal predicates using StaCL formulas. These axioms are expressive enough to derive the rules of Pearl's do-calculus. Finally, we demonstrate by examples that StaCL can be used to specify and explain the correctness of statistical causal inference., Comment: Full version for the paper accepted at JELIA 2023 (the 18th European Conference on Logics in Artificial Intelligence)

We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, we define belief Hoare logic (BHL) for formalizing and reasoning about the statistical beliefs acquired via hypothesis testing. This program logic is sound and relatively complete with respect to a Kripke model for hypothesis tests. We demonstrate by examples that BHL is useful for reasoning about practical issues in hypothesis testing. In our framework, we clarify the importance of prior beliefs in acquiring statistical beliefs through hypothesis testing, and discuss the whole picture of the justification of statistical inference inside and outside the program logic., Comment: Accepted to the journal Artificial Intelligence (AI); an extended version of the KR'21 conference paper https://proceedings.kr.org/2021/39/

Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Towards a general framework for such logics, in this paper, we formalize quantitative difference between computational effects as divergence on monad, then develop a relational program logic acRL that supports generic computational effects and divergences on them. To give a categorical semantics of acRL supporting divergences, we give a method to obtain graded strong relational liftings from divergences on monads. We derive two instantiations of acRL for the verification of 1) various differential privacy of higher-order functional probabilistic programs and 2) difference of distribution of costs between higher-order functional programs with probabilistic choice and cost counting operations., Comment: Preprint

General relations for nonequilibrium spin transport at a magnetic junction between a normal metal and a ferromagnetic insulator are derived from the quantum fluctuation theorem. They include the extended Onsager relations between the spin conductance and the spin-current noise that hold for nonequilibrium states driven by an external current. These relations, that are valid for a general setup of spin Hall magnetoresistance, provide a comprehensive viewpoint for understanding of unidirectional spin Hall magnetoresistance in insulating ferromagnetic junctions., Comment: 8 pages, 1 figure

Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed $\lambda$-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples., Comment: Full version of ICFP 21 paper

Ferromagnetism was observed in a Pt(100) ultrathin film deposited on a SrTiO3(100) substrate. The ferromagnetism, which appears in films with thicknesses of 2.2-4.4 nm, periodically changes with a period of approximately 1 nm (5-6 monolayers) depending on the film thickness. This is consistent with the period derived from the quantum-well states formed in the thin film. X-ray magnetic circular dichroism measurements show the evidence of appearance of intrinsic ferromagnetism in Pt(100) ultra-thin film. In addition, present results suggest a possibility that the orbital magnetic moment of pure Pt is much smaller than that of the Pt/ferromagnetic multilayer system. These results will provide a potential new mechanism for origin of the large magnetic anisotropy in Pt components., Comment: 7 pages, 4 figures

Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.

Differential privacy is a de facto standard in data privacy, with applications in the public and private sectors. A way to explain differential privacy, which is particularly appealing to statistician and social scientists is by means of its statistical hypothesis testing interpretation. Informally, one cannot effectively test whether a specific individual has contributed her data by observing the output of a private mechanism---any test cannot have both high significance and high power. In this paper, we identify some conditions under which a privacy definition given in terms of a statistical divergence satisfies a similar interpretation. These conditions are useful to analyze the distinguishability power of divergences and we use them to study the hypothesis testing interpretation of some relaxations of differential privacy based on Renyi divergence. This analysis also results in an improved conversion rule between these definitions and differential privacy.

We demonstrate control of the magnetism of Pd(100) ultrathin films, which show d-electron quantum-well induced ferromagnetism, via modulation of the interface electronic state using density functional calculation. From an analysis based on the phase model, forming the Au/Pd(100) interface induces hybridization of the wave function of d-electron quantum-well states, and modulates the term of the scattering phase shift as a function of the reciprocal lattice point. In contrast, forming the Al interface, which has only s-electrons at the Fermi energy, cannot modify the scattering phase shift. Our finding indicates the possibility of modifying the phase shift by tailoring the interface electronic states using hybridization of the wave function, and this efficiently changes the density of states near the Fermi energy of Pd films, and the switching between paramagnetism and ferromagnetism occurs based on the condition for ferromagnetism (Stoner criterion)., Comment: 10 pages, 7 figures

The magnetization of Pd(100) ultrathin films that show ferromagnetism due to quantum well states was manipulated by changing the quantum well state with an applied bias voltage. The voltage dependence of the magnetic moment of Pd/SrTiO$_{3-x}$/Ti/Au intrinsically depends on the Pd film thickness. The induced change in the magnetic moment is due to the modulation of the phase shift at the interface between the Pd thin film and the semiconductor SrTiO$_{3-x}$ substrate., Comment: 5 pages, accepted for publication in Applied Physics Letters

We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations which were not supported by its precursor, categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended pseudometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We also introduce the dual method called density lifting of comonads. We next study the liftings of algebraic operations to the codensity liftings of monads. We also give a characterisation of the class of liftings of monads along posetal fibrations with fibred small meets as a limit of a certain large diagram., Comment: Extended version of the paper presented at CALCO 2015, accepted for publication in LMCS

Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru, derive their expressiveness from a powerful combination of continuous distributions, conditioning, and higher-order functions. Although very important for practical applications, these combined features raise fundamental challenges for program semantics and verification. Several recent works offer promising answers to these challenges, but their primary focus is on semantical issues. In this paper, we take a step further and we develop a set of program logics, named PPV, for proving properties of programs written in an expressive probabilistic higher-order language with continuous distributions and operators for conditioning distributions by real-valued functions. Pleasingly, our program logics retain the comfortable reasoning style of informal proofs thanks to carefully selected axiomatizations of key results from probability theory. The versatility of our logics is illustrated through the formal verification of several intricate examples from statistics, probabilistic inference, and machine learning. We further show the expressiveness of our logics by giving sound embeddings of existing logics. In particular, we do this in a parametric way by showing how the semantics idea of (unary and relational) TT-lifting can be internalized in our logics. The soundness of PPV follows by interpreting programs and assertions in quasi-Borel spaces (QBS), a recently proposed variant of Borel spaces with a good structure for interpreting higher order probabilistic programs.

We develop new abstractions for reasoning about relaxations of differential privacy: R\'enyi differential privacy, zero-concentrated differential privacy, and truncated concentrated differential privacy, which express different bounds on statistical divergences between two output probability distributions. In order to reason about such properties compositionally, we introduce approximate span-lifting, a novel construction extending the approximate relational lifting approaches previously developed for standard differential privacy to a more general class of divergences, and also to continuous distributions. As an application, we develop a program logic based on approximate span-liftings capable of proving relaxations of differential privacy and other statistical divergence properties.

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.

We study the crystal structure of Pd(100) ultrathin films, which show ferromagnetism induced by the quantum confinement effect, using in-situ X-ray crystal truncation rod measurement and density functional calculation. The energy gain due to the appearance of ferromagnetism in Pd results in flatter and uniform film growth of ferromagnetic Pd films compared with paramagnetic Pd. In addition, ferromagnetic Pd films expand the lattice constant in order to suppress the increase in kinetic energy of electrons accompanied by the occurrence of exchange splitting. Although the traditional theory of magnetism in metals indicates that the increase in density of states that induces ferromagnetism (Stoner criterion), our present finding reveals a mechanism of modulation in the density of states via the appearance of ferromagnetism, i.e., the inverse mechanism of Stoner's theory., Comment: 5 pages, 4 figures

We show that the Giry monad is not strong with respect to the canonical symmetric monoidal closed structure on the category Meas of all measurable spaces and measurable functions.