-
Echoes in the Noise: Posterior Samples of Faint Galaxy Surface Brightness Profiles with Score-Based Likelihoods and Priors
Authors:
Alexandre Adam,
Connor Stone,
Connor Bottrell,
Ronan Legin,
Yashar Hezaveh,
Laurence Perreault-Levasseur
Abstract:
Examining the detailed structure of galaxy populations provides valuable insights into their formation and evolution mechanisms. Significant barriers to such analysis are the non-trivial noise properties of real astronomical images and the point spread function (PSF) which blurs structure. Here we present a framework which combines recent advances in score-based likelihood characterization and dif…
▽ More
Examining the detailed structure of galaxy populations provides valuable insights into their formation and evolution mechanisms. Significant barriers to such analysis are the non-trivial noise properties of real astronomical images and the point spread function (PSF) which blurs structure. Here we present a framework which combines recent advances in score-based likelihood characterization and diffusion model priors to perform a Bayesian analysis of image deconvolution. The method, when applied to minimally processed \emph{Hubble Space Telescope} (\emph{HST}) data, recovers structures which have otherwise only become visible in next-generation \emph{James Webb Space Telescope} (\emph{JWST}) imaging.
△ Less
Submitted 29 November, 2023;
originally announced November 2023.
-
Towards Exploratory Reformulation of Constraint Models
Authors:
Ian Miguel,
András Z. Salamon,
Christopher Stone
Abstract:
It is well established that formulating an effective constraint model of a problem of interest is crucial to the efficiency with which it can subsequently be solved. Following from the observation that it is difficult, if not impossible, to know a priori which of a set of candidate models will perform best in practice, we envisage a system that explores the space of models through a process of ref…
▽ More
It is well established that formulating an effective constraint model of a problem of interest is crucial to the efficiency with which it can subsequently be solved. Following from the observation that it is difficult, if not impossible, to know a priori which of a set of candidate models will perform best in practice, we envisage a system that explores the space of models through a process of reformulation from an initial model, guided by performance on a set of training instances from the problem class under consideration. We plan to situate this system in a refinement-based approach, where a user writes a constraint specification describing a problem above the level of abstraction at which many modelling decisions are made. In this position paper we set out our plan for an exploratory reformulation system, and discuss progress made so far.
△ Less
Submitted 20 November, 2023;
originally announced November 2023.
-
Exploring Benchmarks for Self-Driving Labs using Color Matching
Authors:
Tobias Ginsburg,
Kyle Hippe,
Ryan Lewis,
Doga Ozgulbas,
Aileen Cleary,
Rory Butler,
Casey Stone,
Abraham Stroka,
Ian Foster
Abstract:
Self Driving Labs (SDLs) that combine automation of experimental procedures with autonomous decision making are gaining popularity as a means of increasing the throughput of scientific workflows. The task of identifying quantities of supplied colored pigments that match a target color, the color matching problem, provides a simple and flexible SDL test case, as it requires experiment proposal, sam…
▽ More
Self Driving Labs (SDLs) that combine automation of experimental procedures with autonomous decision making are gaining popularity as a means of increasing the throughput of scientific workflows. The task of identifying quantities of supplied colored pigments that match a target color, the color matching problem, provides a simple and flexible SDL test case, as it requires experiment proposal, sample creation, and sample analysis, three common components in autonomous discovery applications. We present a robotic solution to the color matching problem that allows for fully autonomous execution of a color matching protocol. Our solution leverages the WEI science factory platform to enable portability across different robotic hardware, the use of alternative optimization methods for continuous refinement, and automated publication of results for experiment tracking and post-hoc analysis.
△ Less
Submitted 30 September, 2023;
originally announced October 2023.
-
A Large Language Model Approach to Educational Survey Feedback Analysis
Authors:
Michael J. Parker,
Caitlin Anderson,
Claire Stone,
YeaRim Oh
Abstract:
This paper assesses the potential for the large language models (LLMs) GPT-4 and GPT-3.5 to aid in deriving insight from education feedback surveys. Exploration of LLM use cases in education has focused on teaching and learning, with less exploration of capabilities in education feedback analysis. Survey analysis in education involves goals such as finding gaps in curricula or evaluating teachers,…
▽ More
This paper assesses the potential for the large language models (LLMs) GPT-4 and GPT-3.5 to aid in deriving insight from education feedback surveys. Exploration of LLM use cases in education has focused on teaching and learning, with less exploration of capabilities in education feedback analysis. Survey analysis in education involves goals such as finding gaps in curricula or evaluating teachers, often requiring time-consuming manual processing of textual responses. LLMs have the potential to provide a flexible means of achieving these goals without specialized machine learning models or fine-tuning. We demonstrate a versatile approach to such goals by treating them as sequences of natural language processing (NLP) tasks including classification (multi-label, multi-class, and binary), extraction, thematic analysis, and sentiment analysis, each performed by LLM. We apply these workflows to a real-world dataset of 2500 end-of-course survey comments from biomedical science courses, and evaluate a zero-shot approach (i.e., requiring no examples or labeled training data) across all tasks, reflecting education settings, where labeled data is often scarce. By applying effective prompting practices, we achieve human-level performance on multiple tasks with GPT-4, enabling workflows necessary to achieve typical goals. We also show the potential of inspecting LLMs' chain-of-thought (CoT) reasoning for providing insight that may foster confidence in practice. Moreover, this study features development of a versatile set of classification categories, suitable for various course types (online, hybrid, or in-person) and amenable to customization. Our results suggest that LLMs can be used to derive a range of insights from survey text.
△ Less
Submitted 26 June, 2024; v1 submitted 29 September, 2023;
originally announced September 2023.
-
Towards a Modular Architecture for Science Factories
Authors:
Rafael Vescovi,
Tobias Ginsburg,
Kyle Hippe,
Doga Ozgulbas,
Casey Stone,
Abraham Stroka,
Rory Butler,
Ben Blaiszik,
Tom Brettin,
Kyle Chard,
Mark Hereld,
Arvind Ramanathan,
Rick Stevens,
Aikaterini Vriza,
Jie Xu,
Qingteng Zhang,
Ian Foster
Abstract:
Advances in robotic automation, high-performance computing (HPC), and artificial intelligence (AI) encourage us to conceive of science factories: large, general-purpose computation- and AI-enabled self-driving laboratories (SDLs) with the generality and scale needed both to tackle large discovery problems and to support thousands of scientists. Science factories require modular hardware and softwa…
▽ More
Advances in robotic automation, high-performance computing (HPC), and artificial intelligence (AI) encourage us to conceive of science factories: large, general-purpose computation- and AI-enabled self-driving laboratories (SDLs) with the generality and scale needed both to tackle large discovery problems and to support thousands of scientists. Science factories require modular hardware and software that can be replicated for scale and (re)configured to support many applications. To this end, we propose a prototype modular science factory architecture in which reconfigurable modules encapsulating scientific instruments are linked with manipulators to form workcells, that can themselves be combined to form larger assemblages, and linked with distributed computing for simulation, AI model training and inference, and related tasks. Workflows that perform sets of actions on modules can be specified, and various applications, comprising workflows plus associated computational and data manipulation steps, can be run concurrently. We report on our experiences prototy** this architecture and applying it in experiments involving 15 different robotic apparatus, five applications (one in education, two in biology, two in materials), and a variety of workflows, across four laboratories. We describe the reuse of modules, workcells, and workflows in different applications, the migration of applications between workcells, and the use of digital twins, and suggest directions for future work aimed at yet more generality and scalability. Code and data are available at https://ad-sdl.github.io/wei2023 and in the Supplementary Information
△ Less
Submitted 17 October, 2023; v1 submitted 18 August, 2023;
originally announced August 2023.
-
Adelie: Continuous Address Space Layout Re-randomization for Linux Drivers
Authors:
Ruslan Nikolaev,
Hassan Nadeem,
Cathlyn Stone,
Binoy Ravindran
Abstract:
While address space layout randomization (ASLR) has been extensively studied for user-space programs, the corresponding OS kernel's KASLR support remains very limited, making the kernel vulnerable to just-in-time (JIT) return-oriented programming (ROP) attacks. Furthermore, commodity OSs such as Linux restrict their KASLR range to 32 bits due to architectural constraints (e.g., x86-64 only support…
▽ More
While address space layout randomization (ASLR) has been extensively studied for user-space programs, the corresponding OS kernel's KASLR support remains very limited, making the kernel vulnerable to just-in-time (JIT) return-oriented programming (ROP) attacks. Furthermore, commodity OSs such as Linux restrict their KASLR range to 32 bits due to architectural constraints (e.g., x86-64 only supports 32-bit immediate operands for most instructions), which makes them vulnerable to even unsophisticated brute-force ROP attacks due to low entropy. Most in-kernel pointers remain static, exacerbating the problem when pointers are leaked.
Adelie, our kernel defense mechanism, overcomes KASLR limitations, increases KASLR entropy, and makes successful ROP attacks on the Linux kernel much harder to achieve. First, Adelie enables the position-independent code (PIC) model so that the kernel and its modules can be placed anywhere in the 64-bit virtual address space, at any distance apart from each other. Second, Adelie implements stack re-randomization and address encryption on modules. Finally, Adelie enables efficient continuous KASLR for modules by using the PIC model to make it (almost) impossible to inject ROP gadgets through these modules regardless of gadget's origin.
Since device drivers (typically compiled as modules) are often developed by third parties and are typically less tested than core OS parts, they are also often more vulnerable. By fully re-randomizing device drivers, the last two contributions together prevent most JIT ROP attacks since vulnerable modules are very likely to be a starting point of an attack. Furthermore, some OS instances in virtualized environments are specifically designated to run device drivers, where drivers are the primary target of JIT ROP attacks. Our evaluation shows high efficiency of Adelie's approach.
[full abstract is in the paper]
△ Less
Submitted 20 January, 2022;
originally announced January 2022.
-
SoK: Untangling File-based Encryption on Mobile Devices
Authors:
David Galindo,
Jia Liu,
Chris McMahon Stone,
Mihai Ordean
Abstract:
File-based encryption (FBE) schemes have been developed by software vendors to address security concerns related to data storage. While methods of encrypting data-at-rest may seem relatively straightforward, the main proponents of these technologies in mobile devices have nonetheless created seemingly different FBE solutions. As most of the underlying design decisions are described either at a hig…
▽ More
File-based encryption (FBE) schemes have been developed by software vendors to address security concerns related to data storage. While methods of encrypting data-at-rest may seem relatively straightforward, the main proponents of these technologies in mobile devices have nonetheless created seemingly different FBE solutions. As most of the underlying design decisions are described either at a high-level in whitepapers, or are accessible at a low-level by examining the corresponding source code (Android) or through reverse-engineering (iOS), comparisons between schemes and discussions on their relative strengths are scarce. In this paper, we propose a formal framework for the study of file-based encryption systems, focusing on two prominent implementations: the FBE scheme used in Android and Linux operating systems, as well as the FBE scheme used in iOS. Our proposed formal model and our detailed description of the existing algorithms are based on documentation of diverse nature, such as whitepapers, technical reports, presentations and blog posts, among others. Using our framework we validate the security of the existing key derivation chains, as well as the security of the overall designs, under widely-known security assumptions for symmetric ciphers, such as IND-CPA or INT-CTXT security, in the random-oracle model.
△ Less
Submitted 24 November, 2021;
originally announced November 2021.
-
Realistic galaxy image simulation via score-based generative models
Authors:
Michael J. Smith,
James E. Geach,
Ryan A. Jackson,
Nikhil Arora,
Connor Stone,
Stéphane Courteau
Abstract:
We show that a Denoising Diffusion Probabalistic Model (DDPM), a class of score-based generative model, can be used to produce realistic mock images that mimic observations of galaxies. Our method is tested with Dark Energy Spectroscopic Instrument (DESI) grz imaging of galaxies from the Photometry and Rotation curve OBservations from Extragalactic Surveys (PROBES) sample and galaxies selected fro…
▽ More
We show that a Denoising Diffusion Probabalistic Model (DDPM), a class of score-based generative model, can be used to produce realistic mock images that mimic observations of galaxies. Our method is tested with Dark Energy Spectroscopic Instrument (DESI) grz imaging of galaxies from the Photometry and Rotation curve OBservations from Extragalactic Surveys (PROBES) sample and galaxies selected from the Sloan Digital Sky Survey. Subjectively, the generated galaxies are highly realistic when compared with samples from the real dataset. We quantify the similarity by borrowing from the deep generative learning literature, using the `Fréchet Inception Distance' to test for subjective and morphological similarity. We also introduce the `Synthetic Galaxy Distance' metric to compare the emergent physical properties (such as total magnitude, colour and half light radius) of a ground truth parent and synthesised child dataset. We argue that the DDPM approach produces sharper and more realistic images than other generative methods such as Adversarial Networks (with the downside of more costly inference), and could be used to produce large samples of synthetic observations tailored to a specific imaging survey. We demonstrate two potential uses of the DDPM: (1) accurate in-painting of occluded data, such as satellite trails, and (2) domain transfer, where new input images can be processed to mimic the properties of the DDPM training set. Here we `DESI-fy' cartoon images as a proof of concept for domain transfer. Finally, we suggest potential applications for score-based approaches that could motivate further research on this topic within the astronomical community.
△ Less
Submitted 31 January, 2022; v1 submitted 2 November, 2021;
originally announced November 2021.
-
The Closer You Look, The More You Learn: A Grey-box Approach to Protocol State Machine Learning
Authors:
Chris McMahon Stone,
Sam L. Thomas,
Mathy Vanhoef,
James Henderson,
Nicolas Bailluet,
Tom Chothia
Abstract:
In this paper, we propose a new approach to infer state machine models from protocol implementations. Our method, STATEINSPECTOR, learns protocol states by using novel program analyses to combine observations of run-time memory and I/O. It requires no access to source code and only lightweight execution monitoring of the implementation under test. We demonstrate and evaluate STATEINSPECTOR's effec…
▽ More
In this paper, we propose a new approach to infer state machine models from protocol implementations. Our method, STATEINSPECTOR, learns protocol states by using novel program analyses to combine observations of run-time memory and I/O. It requires no access to source code and only lightweight execution monitoring of the implementation under test. We demonstrate and evaluate STATEINSPECTOR's effectiveness on numerous TLS and WPA/2 implementations. In the process, we show STATEINSPECTOR enables deeper state discovery, increased learning efficiency, and more insightful post-mortem analyses than existing approaches. Further to improved learning, our method led us to discover several concerning deviations from the standards and a high impact vulnerability in a prominent Wi-Fi implementation.
△ Less
Submitted 7 June, 2021; v1 submitted 4 June, 2021;
originally announced June 2021.
-
Pix2Prof: fast extraction of sequential information from galaxy imagery via a deep natural language 'captioning' model
Authors:
Michael J. Smith,
Nikhil Arora,
Connor Stone,
Stéphane Courteau,
James E. Geach
Abstract:
We present 'Pix2Prof', a deep learning model that can eliminate any manual steps taken when extracting galaxy profiles. We argue that a galaxy profile of any sort is conceptually similar to a natural language image caption. This idea allows us to leverage image captioning methods from the field of natural language processing, and so we design Pix2Prof as a float sequence 'captioning' model suitabl…
▽ More
We present 'Pix2Prof', a deep learning model that can eliminate any manual steps taken when extracting galaxy profiles. We argue that a galaxy profile of any sort is conceptually similar to a natural language image caption. This idea allows us to leverage image captioning methods from the field of natural language processing, and so we design Pix2Prof as a float sequence 'captioning' model suitable for galaxy profile inference. We demonstrate the technique by approximating a galaxy surface brightness (SB) profile fitting method that contains several manual steps. Pix2Prof processes $\sim$1 image per second on an Intel Xeon E5 2650 v3 CPU, improving on the speed of the manual interactive method by more than two orders of magnitude. Crucially, Pix2Prof requires no manual interaction, and since galaxy profile estimation is an embarrassingly parallel problem, we can further increase the throughput by running many Pix2Prof instances simultaneously. In perspective, Pix2Prof would take under an hour to infer profiles for $10^5$ galaxies on a single NVIDIA DGX-2 system. A single human expert would take approximately two years to complete the same task. Automated methodology such as this will accelerate the analysis of the next generation of large area sky surveys expected to yield hundreds of millions of targets. In such instances, all manual approaches -- even those involving a large number of experts -- will be impractical.
△ Less
Submitted 28 April, 2021; v1 submitted 1 October, 2020;
originally announced October 2020.
-
Exploring Instance Generation for Automated Planning
Authors:
Özgür Akgün,
Nguyen Dang,
Joan Espasa,
Ian Miguel,
András Z. Salamon,
Christopher Stone
Abstract:
Many of the core disciplines of artificial intelligence have sets of standard benchmark problems well known and widely used by the community when develo** new algorithms. Constraint programming and automated planning are examples of these areas, where the behaviour of a new algorithm is measured by how it performs on these instances. Typically the efficiency of each solving method varies not onl…
▽ More
Many of the core disciplines of artificial intelligence have sets of standard benchmark problems well known and widely used by the community when develo** new algorithms. Constraint programming and automated planning are examples of these areas, where the behaviour of a new algorithm is measured by how it performs on these instances. Typically the efficiency of each solving method varies not only between problems, but also between instances of the same problem. Therefore, having a diverse set of instances is crucial to be able to effectively evaluate a new solving method. Current methods for automatic generation of instances for Constraint Programming problems start with a declarative model and search for instances with some desired attributes, such as hardness or size. We first explore the difficulties of adapting this approach to generate instances starting from problem specifications written in PDDL, the de-facto standard language of the automated planning community. We then propose a new approach where the whole planning problem description is modelled using Essence, an abstract modelling language that allows expressing high-level structures without committing to a particular low level representation in PDDL.
△ Less
Submitted 21 September, 2020;
originally announced September 2020.
-
Design and Implementation of the Andromeda Proof Assistant
Authors:
Andrej Bauer,
Gaëtan Gilbert,
Philipp G. Haselwarter,
Matija Pretnar,
Christopher A. Stone
Abstract:
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments.
Since the nucleus does not perform complex…
▽ More
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments.
Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. %even if the AML code (or interpreter) is untrusted.
To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization).
The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped $λ$-calculus, and by implementing a simple automated system for managing a universe of types.
△ Less
Submitted 17 February, 2018;
originally announced February 2018.
-
Accelerating finite-rate chemical kinetics with coprocessors: comparing vectorization methods on GPUs, MICs, and CPUs
Authors:
Christopher P. Stone,
Andrew T. Alferman,
Kyle E. Niemeyer
Abstract:
Efficient ordinary differential equation solvers for chemical kinetics must take into account the available thread and instruction-level parallelism of the underlying hardware, especially on many-core coprocessors, as well as the numerical efficiency. A stiff Rosenbrock and nonstiff Runge-Kutta solver are implemented using the single instruction, multiple thread (SIMT) and single instruction, mult…
▽ More
Efficient ordinary differential equation solvers for chemical kinetics must take into account the available thread and instruction-level parallelism of the underlying hardware, especially on many-core coprocessors, as well as the numerical efficiency. A stiff Rosenbrock and nonstiff Runge-Kutta solver are implemented using the single instruction, multiple thread (SIMT) and single instruction, multiple data (SIMD) paradigms with OpenCL. The performances of these parallel implementations were measured with three chemical kinetic models across several multicore and many-core platforms. Two runtime benchmarks were conducted to clearly determine any performance advantage offered by either method: evaluating the right-hand-side source terms in parallel, and integrating a series of constant-pressure homogeneous reactors using the Rosenbrock and Runge-Kutta solvers. The right-hand-side evaluations with SIMD parallelism on the host multicore Xeon CPU and many-core Xeon Phi co-processor performed approximately three times faster than the baseline multithreaded code. The SIMT model on the host and Phi was 13-35% slower than the baseline while the SIMT model on the GPU provided approximately the same performance as the SIMD model on the Phi. The runtimes for both ODE solvers decreased 2.5-2.7x with the SIMD implementations on the host CPU and 4.7-4.9x with the Xeon Phi coprocessor compared to the baseline parallel code. The SIMT implementations on the GPU ran 1.4-1.6 times faster than the baseline multithreaded CPU code; however, this was significantly slower than the SIMD versions on the host CPU or the Xeon Phi. The performance difference between the three platforms was attributed to thread divergence caused by the adaptive step-sizes within the ODE integrators. Analysis showed that the wider vector width of the GPU incurs a higher level of divergence than the narrower Sandy Bridge or Xeon Phi.
△ Less
Submitted 28 August, 2017; v1 submitted 20 August, 2016;
originally announced August 2016.
-
Observationally Cooperative Multithreading
Authors:
Christopher A. Stone,
Melissa E. O'Neill,
Sonja A. Bohr,
Adam M. Cozzette,
M. Joe DeBlasio,
Julia Matsieva,
Stuart A. Pernsteiner,
Ari D. Schumer
Abstract:
Despite widespread interest in multicore computing, concur- rency models in mainstream languages often lead to subtle, error-prone code.
Observationally Cooperative Multithreading (OCM) is a new approach to shared-memory parallelism. Programmers write code using the well-understood cooperative (i.e., nonpreemptive) multithreading model for uniprocessors. OCM then allows threads to run in paralle…
▽ More
Despite widespread interest in multicore computing, concur- rency models in mainstream languages often lead to subtle, error-prone code.
Observationally Cooperative Multithreading (OCM) is a new approach to shared-memory parallelism. Programmers write code using the well-understood cooperative (i.e., nonpreemptive) multithreading model for uniprocessors. OCM then allows threads to run in parallel, so long as results remain consistent with the cooperative model.
Programmers benefit because they can reason largely sequentially. Remaining interthread interactions are far less chaotic than in other models, permitting easier reasoning and debugging. Programmers can also defer the choice of concurrency-control mechanism (e.g., locks or transactions) until after they have written their programs, at which point they can compare concurrency-control strategies and choose the one that offers the best performance. Implementers and researchers also benefit from the agnostic nature of OCM -- it provides a level of abstraction to investigate, compare, and combine a variety of interesting concurrency-control techniques.
△ Less
Submitted 17 February, 2015;
originally announced February 2015.
-
Coevolving Cellular Automata with Memory for Chemical Computing: Boolean Logic Gates in the B-Z Reaction
Authors:
Christopher Stone,
Rita Toth,
Ben de Lacy Costello,
Larry Bull,
Andrew Adamatzky
Abstract:
We propose that the behaviour of non-linear media can be controlled automatically through coevolutionary systems. By extension, forms of unconventional computing, i.e., massively parallel non-linear computers, can be realised by such an approach. In this study a light-sensitive sub-excitable Belousov-Zhabotinsky reaction is controlled using various heterogeneous cellular automata. A checkerboard i…
▽ More
We propose that the behaviour of non-linear media can be controlled automatically through coevolutionary systems. By extension, forms of unconventional computing, i.e., massively parallel non-linear computers, can be realised by such an approach. In this study a light-sensitive sub-excitable Belousov-Zhabotinsky reaction is controlled using various heterogeneous cellular automata. A checkerboard image comprising of varying light intensity cells is projected onto the surface of a catalyst-loaded gel resulting in rich spatio-temporal chemical wave behaviour. The coevolved cellular automata are shown to be able to control chemical activity through dynamic control of the light intensity. The approach is demonstrated through the creation of a number of simple Boolean logic gates.
△ Less
Submitted 12 December, 2012;
originally announced December 2012.
