Risk-limiting audits (RLAs) are the established techniques for verifying large elections. While they provide rigorous guarantees of correctness, widespread adoption has been impeded by both efficiency concerns and the fact they offer statistical, rather than absolute, conclusions. We define new families of audits that help to address these issues. Our new audits are enabled by revisiting the standard notion of a cast-vote record so that it can declare multiple possible mark interpretations rather than a single decision; this can reflect the presence of ambiguous marks, which appear regularly on hand-marked ballots. We show that this simple expedient can offer significant efficiency improvements with only minor changes to existing auditing infrastructure. We establish that these "Bayesian" comparison audits are indeed risk-limiting in the formal sense of (Fuller, Harrison, and Russell, 2022). We then define a new type of post-election audit we call a contested audit. These call for each candidate to provide a cast-vote record table advancing their own claim to victory. We prove that these audits offer remarkable sample efficiency: they guarantee negligible risk with only a constant number of ballot inspections. This is a first for an audit with provable soundness. These results are formulated in a game-based security model that specify quantitative soundness and completeness guarantees. Finally, we observe that these audits provide a direct means to handle contestation of election results affirmed by conventional RLAs.
View on arXiv