Derandomization with Pseudorandomness

TL;DR

This paper presents a framework for expressing and verifying derandomized algorithms using pseudorandom objects in Isabelle, facilitating the verification of complex randomized algorithms and demonstrating its effectiveness with a space-optimal algorithm example.

Contribution

It introduces a library for pseudorandom objects that simplifies verification of advanced randomized algorithms in Isabelle, abstracting complex algebraic and analytic results.

Findings

Library enables verification of complex randomized algorithms.

Framework was used to verify Blasiok's space-optimal distinct elements algorithm.

Simplifies the process of verifying derandomization techniques.

Abstract

Derandomization techniques are often used within advanced randomized algorithms. In particular, pseudorandom objects, such as hash families and expander graphs, are key components of such algorithms, but their verification presents a challenge. This work shows how such algorithms can be expressed and verified in Isabelle and presents a pseudorandom objects library that abstracts away the deep algebraic/analytic results involved. Moreover, it presents examples that show how the library eases and enables the verification of advanced randomized algorithms. Highlighting the value of this framework is that it was recently used to verify the space-optimal distinct elements algorithm by Blasiok from 2018, which relies on the combination of many derandomization techniques to achieve its optimality.