arXiv subjects

John O'Leary

Publications and source records attributed to John O'Leary.

7 recordsLinked to original sources

arXiv2023

Metropolis-Hastings transition kernel couplings

Couplings play a central role in the analysis of Markov chain convergence and in the construction of novel Markov chain Monte Carlo estimators, diagnostics, and variance reduction techniques. The set of possible couplings is often intractable, frustrating the search for tight bounds and efficient estimators. To address this challenge for algorithms in the Metropolis-Hastings (MH) family, we establish a simple characterization of the set of MH transition kernel couplings. We then extend this result to describe the set of maximal couplings of the MH kernel, resolving an open question of O'Leary et al.. Our results represent an advance in understanding the MH transition kernel and a step forward for coupling this popular class of algorithms.

math.ST↗

arXiv2021

Couplings of the Random-Walk Metropolis algorithm

Couplings play a central role in contemporary Markov chain Monte Carlo methods and in the analysis of their convergence to stationarity. In most cases, a coupling must induce relatively fast meeting between chains to ensure good performance. In this paper we fix attention on the random walk Metropolis algorithm and examine a range of coupling design choices. We introduce proposal and acceptance step couplings based on geometric, optimal transport, and maximality considerations. We consider the theoretical properties of these choices and examine their implication for the meeting time of the chains. We conclude by extracting a few general principles and hypotheses on the design of effective couplings.

stat.ME↗

arXiv2020

Maximal couplings of the Metropolis-Hastings algorithm

Couplings play a central role in the analysis of Markov chain Monte Carlo algorithms and appear increasingly often in the algorithms themselves, e.g. in convergence diagnostics, parallelization, and variance reduction techniques. Existing couplings of the Metropolis-Hastings algorithm handle the proposal and acceptance steps separately and fall short of the upper bound on one-step meeting probabilities given by the coupling inequality. This paper introduces maximal couplings which achieve this bound while retaining the practical advantages of current methods. We consider the properties of these couplings and examine their behavior on a selection of numerical examples.

stat.CO↗

arXiv2020

Learning Concise Models from Long Execution Traces

Abstract models of system-level behaviour have applications in design exploration, analysis, testing and verification. We describe a new algorithm for automatically extracting useful models, as automata, from execution traces of a HW/SW system driven by software exercising a use-case of interest. Our algorithm leverages modern program synthesis techniques to generate predicates on automaton edges, succinctly describing system behaviour. It employs trace segmentation to tackle complexity for long traces. We learn concise models capturing transaction-level, system-wide behaviour--experimentally demonstrating the approach using traces from a variety of sources, including the x86 QEMU virtual platform and the Real-Time Linux kernel.

cs.FL↗

arXiv2020

Hardware/Software Co-verification Using Path-based Symbolic Execution

Conventional tools for formal hardware/software co-verification use bounded model checking techniques to construct a single monolithic propositional formula. Formulas generated in this way are extremely complex and contain a great deal of irrelevant logic, hence are difficult to solve even by the state-of-the-art Satis ability (SAT) solvers. In a typical hardware/software co-design the firmware only exercises a fraction of the hardware state-space, and we can use this observation to generate simpler and more concise formulas. In this paper, we present a novel verification algorithm for hardware/software co-designs that identify partitions of the firmware and the hardware logic pertaining to the feasible execution paths by means of path-based symbolic simulation with custom path-pruning, property-guided slicing and incremental SAT solving. We have implemented this approach in our tool COVERIF. We have experimentally compared COVERIF with HW-CBMC, a monolithic BMC based co-verification tool, and observed an average speed-up of 5X over HW-CBMC for proving safety properties as well as detecting critical co-design bugs in an open-source Universal Asynchronous Receiver Transmitter design and a large SoC design.

cs.FL↗

arXiv2019

CREST: Hardware Formal Verification with ANSI-C Reference Specifications

This paper presents CREST, a prototype front-end tool intended as an add-on to commercial EDA formal verifcation environments. CREST is an adaptation of the CBMC bounded model checker for C, an academic tool widely used in industry for software analysis and property verification. It leverages the capabilities of CBMC to process hardware datapath specifications written in arbitrary ANSI-C, without limiting restrictions to a synthesizable subset. We briefly sketch the architecture of our tool and show its use in a range of verification case studies.

cs.PL↗

arXiv2019

Unbiased Markov chain Monte Carlo with couplings

Markov chain Monte Carlo (MCMC) methods provide consistent of integrals as the number of iterations goes to infinity. MCMC estimators are generally biased after any fixed number of iterations. We propose to remove this bias by using couplings of Markov chains together with a telescopic sum argument of Glynn and Rhee (2014). The resulting unbiased estimators can be computed independently in parallel. We discuss practical couplings for popular MCMC algorithms. We establish the theoretical validity of the proposed estimators and study their efficiency relative to the underlying MCMC algorithms. Finally, we illustrate the performance and limitations of the method on toy examples, on an Ising model around its critical temperature, on a high-dimensional variable selection problem, and on an approximation of the cut distribution arising in Bayesian inference for models made of multiple modules.

stat.ME↗