arXiv subjects

Benjamin Sherman

Publications and source records attributed to Benjamin Sherman.

3 recordsLinked to original sources

arXiv2020

$\lambda_S$: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes

Deep learning is moving towards increasingly sophisticated optimization objectives that employ higher-order functions, such as integration, continuous optimization, and root-finding. Since differentiable programming frameworks such as PyTorch and TensorFlow do not have first-class representations of these functions, developers must reason about the semantics of such objectives and manually translate them to differentiable code. We present a differentiable programming language, $\lambda_S$, that is the first to deliver a semantics for higher-order functions, higher-order derivatives, and Lipschitz but nondifferentiable functions. Together, these features enable $\lambda_S$ to expose differentiable, higher-order functions for integration, optimization, and root-finding as first-class functions with automatically computed derivatives. $\lambda_S$'s semantics is computable, meaning that values can be computed to arbitrary precision, and we implement $\lambda_S$ as an embedded language in Haskell. We use $\lambda_S$ to construct novel differentiable libraries for representing probability distributions, implicit surfaces, and generalized parametric surfaces -- all as instances of higher-order datatypes -- and present case studies that rely on computing the derivatives of these higher-order functions and datatypes. In addition to modeling existing differentiable algorithms, such as a differentiable ray tracer for implicit surfaces, without requiring any user-level differentiation code, we demonstrate new differentiable algorithms, such as the Hausdorff distance of generalized parametric surfaces.

cs.PL↗

arXiv2019

Reactive Probabilistic Programming

Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or Scade used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty -- probabilistic aspects of software's environment or behavior -- even though modeling uncertainty is a primary activity when designing a control system. In this paper we present ProbZelus the first synchronous probabilistic programming language. ProbZelus conservatively provides the facilities of a synchronous language to write control software, with probabilistic constructs to model uncertainties and perform inference-in-the-loop. We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to separate deterministic and probabilistic expressions. We demonstrate a semantics-preserving compilation into a first-order functional language that lends itself to a simple presentation of inference algorithms for streaming models. We also redesign the delayed sampling inference algorithm to provide efficient streaming inference. Together with an evaluation on several reactive applications, our results demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.

cs.PL↗

arXiv2018

Computable decision making on the reals and other spaces via partiality and nondeterminism

Though many safety-critical software systems use floating point to represent real-world input and output, programmers usually have idealized versions in mind that compute with real numbers. Significant deviations from the ideal can cause errors and jeopardize safety. Some programming systems implement exact real arithmetic, which resolves this matter but complicates others, such as decision making. In these systems, it is impossible to compute (total and deterministic) discrete decisions based on connected spaces such as $\mathbb{R}$. We present programming-language semantics based on constructive topology with variants allowing nondeterminism and/or partiality. Either nondeterminism or partiality suffices to allow computable decision making on connected spaces such as $\mathbb{R}$. We then introduce pattern matching on spaces, a language construct for creating programs on spaces, generalizing pattern matching in functional programming, where patterns need not represent decidable predicates and also may overlap or be inexhaustive, giving rise to nondeterminism or partiality, respectively. Nondeterminism and/or partiality also yield formal logics for constructing approximate decision procedures. We implemented these constructs in the Marshall language for exact real arithmetic.

cs.LO↗