-
Iterative Methods for Navier--Stokes Inverse Problems
Authors:
Liam O'Connor,
Daniel Lecoanet,
Evan H. Anders,
Kyle C. Augustson,
Keaton J. Burns,
Geoffrey M. Vasil,
Jeffrey S. Oishi,
Benjamin P. Brown
Abstract:
Even when the partial differential equation underlying a physical process can be evolved forward in time, the retrospective (backward in time) inverse problem often has its own challenges and applications. Direct Adjoint Loo** (DAL) is the defacto approach for solving retrospective inverse problems, but it has not been applied to deterministic retrospective Navier--Stokes inverse problems in 2D…
▽ More
Even when the partial differential equation underlying a physical process can be evolved forward in time, the retrospective (backward in time) inverse problem often has its own challenges and applications. Direct Adjoint Loo** (DAL) is the defacto approach for solving retrospective inverse problems, but it has not been applied to deterministic retrospective Navier--Stokes inverse problems in 2D or 3D. In this paper, we demonstrate that DAL is ill-suited for solving retrospective 2D Navier--Stokes inverse problems. Alongside DAL, we study two other iterative methods: Simple Backward Integration (SBI) and the Quasi-Reversible Method (QRM). Our iterative SBI approach is novel while iterative QRM has previously been used. Using these three iterative methods, we solve two retrospective inverse problems: 1D Korteweg--de Vries--Burgers (decaying nonlinear wave) and 2D Navier--Stokes (unstratified Kelvin--Helmholtz vortex). In both cases, SBI and QRM reproduce the target final states more accurately and in fewer iterations than DAL. We attribute this performance gap to additional terms present in SBI and QRM's respective backward integrations which are absent in DAL.
△ Less
Submitted 1 March, 2024;
originally announced March 2024.
-
Data Quality Over Quantity: Pitfalls and Guidelines for Process Analytics
Authors:
Lim C. Siang,
Shams Elnawawi,
Lee D. Rippon,
Daniel L. O'Connor,
R. Bhushan Gopaluni
Abstract:
A significant portion of the effort involved in advanced process control, process analytics, and machine learning involves acquiring and preparing data. Literature often emphasizes increasingly complex modelling techniques with incremental performance improvements. However, when industrial case studies are published they often lack important details on data acquisition and preparation. Although da…
▽ More
A significant portion of the effort involved in advanced process control, process analytics, and machine learning involves acquiring and preparing data. Literature often emphasizes increasingly complex modelling techniques with incremental performance improvements. However, when industrial case studies are published they often lack important details on data acquisition and preparation. Although data pre-processing is unfairly maligned as trivial and technically uninteresting, in practice it has an out-sized influence on the success of real-world artificial intelligence applications. This work describes best practices for acquiring and preparing operating data to pursue data-driven modelling and control opportunities in industrial processes. We present practical considerations for pre-processing industrial time series data to inform the efficient development of reliable soft sensors that provide valuable process insights.
△ Less
Submitted 5 April, 2023; v1 submitted 11 November, 2022;
originally announced November 2022.
-
Holbert: Reading, Writing, Proving and Learning in the Browser
Authors:
Liam O'Connor,
Rayhana Amjad
Abstract:
This paper presents Holbert: a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the…
▽ More
This paper presents Holbert: a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.
△ Less
Submitted 16 October, 2022;
originally announced October 2022.
-
Primrose: Selecting Container Data Types by Their Properties
Authors:
Xueying Qin,
Liam O'Connor,
Michel Steuwer
Abstract:
Context: Container data types are ubiquitous in computer programming, enabling developers to efficiently store and process collections of data with an easy-to-use programming interface. Many programming languages offer a variety of container implementations in their standard libraries based on data structures offering different capabilities and performance characteristics.
Inquiry: Choosing the…
▽ More
Context: Container data types are ubiquitous in computer programming, enabling developers to efficiently store and process collections of data with an easy-to-use programming interface. Many programming languages offer a variety of container implementations in their standard libraries based on data structures offering different capabilities and performance characteristics.
Inquiry: Choosing the *best* container for an application is not always straightforward, as performance characteristics can change drastically in different scenarios, and as real-world performance is not always correlated to theoretical complexity.
Approach: We present Primrose, a language-agnostic tool for selecting the best performing valid container implementation from a set of container data types that satisfy *properties* given by application developers. Primrose automatically selects the set of valid container implementations for which the *library specifications*, written by the developers of container libraries, satisfies the specified properties. Finally, Primrose ranks the valid library implementations based on their runtime performance.
Knowledge: With Primrose, application developers can specify the expected behaviour of a container as a type refinement with *semantic properties*, e.g., if the container should only contain unique values (such as a `set`) or should satisfy the LIFO property of a `stack`. Semantic properties nicely complement *syntactic properties* (i.e., traits, interfaces, or type classes), together allowing developers to specify a container's programming interface *and* behaviour without committing to a concrete implementation.
Grounding: We present our prototype implementation of Primrose that preprocesses annotated Rust code, selects valid container implementations and ranks them on their performance. The design of Primrose is, however, language-agnostic, and is easy to integrate into other programming languages that support container data types and traits, interfaces, or type classes. Our implementation encodes properties and library specifications into verification conditions in Rosette, an interface for SMT solvers, which determines the set of valid container implementations. We evaluate Primrose by specifying several container implementations, and measuring the time taken to select valid implementations for various combinations of properties with the solver. We automatically validate that container implementations conform to their library specifications via property-based testing.
Importance: This work provides a novel approach to bring abstract modelling and specification of container types directly into the programmer's workflow. Instead of selecting concrete container implementations, application programmers can now work on the level of specification, merely stating the behaviours they require from their container types, and the best implementation can be selected automatically.
△ Less
Submitted 20 February, 2023; v1 submitted 19 May, 2022;
originally announced May 2022.
-
Quickstrom: Property Based Acceptance Testing with LTL Specifications
Authors:
Liam O'Connor,
Oskar Wickström
Abstract:
We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated inte…
▽ More
We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.
△ Less
Submitted 22 March, 2022;
originally announced March 2022.
-
A Simple Discretization Scheme for Gain Matrix Conditioning
Authors:
Daniel L. O'Connor,
Lim C. Siang,
Shams Elnawawi
Abstract:
In industrial model predictive controllers (MPCs), models generated from regression-based system identification methods typically contain small or even physically non-existent degrees of freedom. Control issues can arise when the steady-state optimizer uses these small degrees of freedom to calculate targets for plant operation due to matrix ill-conditioning. Mathematical techniques like Relative…
▽ More
In industrial model predictive controllers (MPCs), models generated from regression-based system identification methods typically contain small or even physically non-existent degrees of freedom. Control issues can arise when the steady-state optimizer uses these small degrees of freedom to calculate targets for plant operation due to matrix ill-conditioning. Mathematical techniques like Relative Gain Array (RGA) and Singular Value Decomposition (SVD) are helpful for analyzing controller gain interactions and identifying conditioning issues, which can be corrected relatively easily in small models. However, these techniques are difficult and tedious to apply for larger, more complex models. This paper describes a novel, non-iterative, RGA-based, binning technique for discretizing the gain matrix and quickly solving 2x2 conditioning issues for any model size, while guaranteeing gain adjustments below a certain threshold. Higher order interactions are also discussed.
△ Less
Submitted 9 June, 2022; v1 submitted 26 February, 2022;
originally announced February 2022.
-
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Authors:
Louis Cheung,
Liam O'Connor,
Christine Rizkallah
Abstract:
Cogent is a restricted functional language designed to reduce the cost of develo** verified systems code. Because of its sometimes-onerous restrictions, such as the lack of support for recursion and its strict uniqueness type system, Cogent provides an escape hatch in the form of a foreign function interface (FFI) to C code. This poses a problem when verifying Cogent programs, as imported C comp…
▽ More
Cogent is a restricted functional language designed to reduce the cost of develo** verified systems code. Because of its sometimes-onerous restrictions, such as the lack of support for recursion and its strict uniqueness type system, Cogent provides an escape hatch in the form of a foreign function interface (FFI) to C code. This poses a problem when verifying Cogent programs, as imported C components do not enjoy the same level of static guarantees that Cogent does. Previous verification of file systems implemented in Cogent merely assumed that their C components were correct and that they preserved the invariants of Cogent's type system. In this paper, we instead prove such obligations. We demonstrate how they smoothly compose with existing Cogent theorems, and result in a correctness theorem of the overall Cogent-C system. The Cogent FFI constraints ensure that key invariants of Cogent's type system are maintained even when calling C code. We verify reusable higher-order and polymorphic functions including a generic loop combinator and array iterators and demonstrate their application to several examples including binary search and the BilbyFs file system. We demonstrate the feasibility of verification of mixed Cogent-C systems, and provide some insight into verification of software comprised of code in multiple languages with differing levels of static guarantees.
△ Less
Submitted 13 December, 2021; v1 submitted 11 December, 2021;
originally announced December 2021.
-
Marginally-Stable Thermal Equilibria of Rayleigh-Bénard Convection
Authors:
Liam O'Connor,
Daniel Lecoanet,
Evan H. Anders
Abstract:
Natural convection is ubiquitous throughout the physical sciences and engineering, yet many of its important properties remain elusive. To study convection in a novel context, we derive and solve a quasilinear form of the Rayleigh-Bénard problem by representing the perturbations in terms of marginally-stable eigenmodes. The amplitude of each eigenmode is determined by requiring that the background…
▽ More
Natural convection is ubiquitous throughout the physical sciences and engineering, yet many of its important properties remain elusive. To study convection in a novel context, we derive and solve a quasilinear form of the Rayleigh-Bénard problem by representing the perturbations in terms of marginally-stable eigenmodes. The amplitude of each eigenmode is determined by requiring that the background state maintains marginal stability. The background temperature profile evolves due to the advective flux of every marginally-stable eigenmode, as well as diffusion. To ensure marginal stability and to obtain the eigenfunctions at every timestep, we perform a one-dimensional eigenvalue solve on each of the allowable wavenumbers. The background temperature field evolves to an equilibrium state, where the advective flux from the marginally-stable eigenmodes and the diffusive flux sum to a constant. These marginally-stable thermal equilibria (MSTE) are exact solutions of the quasilinear equations. The mean temperature profile has thinner boundary layers and larger Nusselt numbers than thermally-equilibrated 2D and 3D simulations of the full nonlinear equations. We find the Nusselt number scales like $\rm{Nu} \sim\rm{Ra}^{1/3}$. When an MSTE is used as initial conditions for a 2D simulation, we find that Nu quickly equilibrates without the burst of turbulence often induced by purely conductive initial conditions, but we also find that the kinetic energy is too large and viscously attenuates on a long viscous time scale. This is due to the thin temperature boundary layers which diffuse heat very effectively, thereby requiring high-velocity advective flows to reach an equilibrium.
△ Less
Submitted 27 February, 2024; v1 submitted 28 May, 2021;
originally announced May 2021.
-
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Authors:
Louis Cheung,
Liam O'Connor,
Christine Rizkallah
Abstract:
Cogent is a restricted functional language designed to reduce the cost of develo** verified systems code. Because of its sometimes-onerous restrictions, such as the lack of support for recursion and its strict uniqueness type system, Cogent provides an escape hatch in the form of a foreign function interface (FFI) to C code. This poses a problem when verifying Cogent programs, as imported C comp…
▽ More
Cogent is a restricted functional language designed to reduce the cost of develo** verified systems code. Because of its sometimes-onerous restrictions, such as the lack of support for recursion and its strict uniqueness type system, Cogent provides an escape hatch in the form of a foreign function interface (FFI) to C code. This poses a problem when verifying Cogent programs, as imported C components do not enjoy the same level of static guarantees that Cogent does. Previous verification of file systems implemented in Cogent merely assumed that their C components were correct and that they preserved the invariants of Cogent's type system. In this paper, we instead prove such obligations. We demonstrate how they smoothly compose with existing Cogent theorems, and result in a correctness theorem of the overall Cogent-C system. The Cogent FFI constraints ensure that key invariants of Cogent's type system are maintained even when calling C code. We verify reusable higher-order and polymorphic functions including a generic loop combinator and array iterators and demonstrate their application to several examples including binary search and the BilbyFs file system. We demonstrate the feasibility of verification of mixed Cogent-C systems, and provide some insight into verification of software comprised of code in multiple languages with differing levels of static guarantees.
△ Less
Submitted 21 December, 2021; v1 submitted 19 February, 2021;
originally announced February 2021.
-
Distinguishing correlation from causation using genome-wide association studies
Authors:
Luke J. O'Connor,
Alkes L. Price
Abstract:
Genome-wide association studies (GWAS) have emerged as a rich source of genetic clues into disease biology, and they have revealed strong genetic correlations among many diseases and traits. Some of these genetic correlations may reflect causal relationships. We developed a method to quantify causal relationships between genetically correlated traits using GWAS summary association statistics. In p…
▽ More
Genome-wide association studies (GWAS) have emerged as a rich source of genetic clues into disease biology, and they have revealed strong genetic correlations among many diseases and traits. Some of these genetic correlations may reflect causal relationships. We developed a method to quantify causal relationships between genetically correlated traits using GWAS summary association statistics. In particular, our method quantifies what part of the genetic component of trait 1 is also causal for trait 2 using mixed fourth moments $E(α_1^2α_1α_2)$ and $E(α_2^2α_1α_2)$ of the bivariate effect size distribution. If trait 1 is causal for trait 2, then SNPs affecting trait 1 (large $α_1^2$) will have correlated effects on trait 2 (large $α_1α_2$), but not vice versa. We validated this approach in extensive simulations. Across 52 traits (average $N=331$k), we identified 30 putative genetically causal relationships, many novel, including an effect of LDL cholesterol on decreased bone mineral density. More broadly, we demonstrate that it is possible to distinguish between genetic correlation and causation using genetic association data.
△ Less
Submitted 21 November, 2018;
originally announced November 2018.
-
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML
Authors:
Yutaka Nagashima,
Liam O'Connor
Abstract:
We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.
We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.
△ Less
Submitted 10 August, 2016;
originally announced August 2016.
-
COGENT: Certified Compilation for a Functional Systems Language
Authors:
Liam O'Connor,
Christine Rizkallah,
Zilin Chen,
Sidney Amani,
Japheth Lim,
Yutaka Nagashima,
Thomas Sewell,
Alex Hixon,
Gabriele Keller,
Toby Murray,
Gerwin Klein
Abstract:
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing suc…
▽ More
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
△ Less
Submitted 21 January, 2016;
originally announced January 2016.
-
Maximum Likelihood Latent Space Embedding of Logistic Random Dot Product Graphs
Authors:
Luke O'Connor,
Muriel Médard,
Soheil Feizi
Abstract:
A latent space model for a family of random graphs assigns real-valued vectors to nodes of the graph such that edge probabilities are determined by latent positions. Latent space models provide a natural statistical framework for graph visualizing and clustering. A latent space model of particular interest is the Random Dot Product Graph (RDPG), which can be fit using an efficient spectral method;…
▽ More
A latent space model for a family of random graphs assigns real-valued vectors to nodes of the graph such that edge probabilities are determined by latent positions. Latent space models provide a natural statistical framework for graph visualizing and clustering. A latent space model of particular interest is the Random Dot Product Graph (RDPG), which can be fit using an efficient spectral method; however, this method is based on a heuristic that can fail, even in simple cases. Here, we consider a closely related latent space model, the Logistic RDPG, which uses a logistic link function to map from latent positions to edge likelihoods. Over this model, we show that asymptotically exact maximum likelihood inference of latent position vectors can be achieved using an efficient spectral method. Our method involves computing top eigenvectors of a normalized adjacency matrix and scaling eigenvectors using a regression step. The novel regression scaling step is an essential part of the proposed method. In simulations, we show that our proposed method is more accurate and more robust than common practices. We also show the effectiveness of our approach over standard real networks of the karate club and political blogs.
△ Less
Submitted 30 August, 2017; v1 submitted 3 October, 2015;
originally announced October 2015.
-
A CM construction for curves of genus 2 with p-rank 1
Authors:
Laura Hitt O'Connor,
Gary McGuire,
Michael Naehrig,
Marco Streng
Abstract:
We construct Weil numbers corresponding to genus-2 curves with $p$-rank 1 over the finite field $\F_{p^2}$ of $p^2$ elements. The corresponding curves can be constructed using explicit CM constructions. In one of our algorithms, the group of $\F_{p^2}$-valued points of the Jacobian has prime order, while another allows for a prescribed embedding degree with respect to a subgroup of prescribed or…
▽ More
We construct Weil numbers corresponding to genus-2 curves with $p$-rank 1 over the finite field $\F_{p^2}$ of $p^2$ elements. The corresponding curves can be constructed using explicit CM constructions. In one of our algorithms, the group of $\F_{p^2}$-valued points of the Jacobian has prime order, while another allows for a prescribed embedding degree with respect to a subgroup of prescribed order. The curves are defined over $\F_{p^2}$ out of necessity: we show that curves of $p$-rank 1 over $\F_p$ for large $p$ cannot be efficiently constructed using explicit CM constructions.
△ Less
Submitted 11 May, 2010; v1 submitted 20 November, 2008;
originally announced November 2008.
