22 June 2020 - Jake Palmer Link https://eu.bbcollab.com/guest/97e5b2666aa74b30870a4c83ad03760a Speaker Jake Palmer Title Formal verification for Meek's method of STV Abstract Single Transferable Vote (STV) systems are typically counted by hand, but some are complicated enough for that to be infeasible for mid-to-large scale elections, such as Schulze STV and CPO-STV. One other such complicated variant is Meek's method of STV, which also sees use in practice. It is currently in use in a number of local elections in New Zealand, the Royal Statistical Society, and the Stack Exchange network. We propose to verify its correctness in terms of termination and seat-filling, and prove various important properties it possesses (and those it doesn't), as well as characterise when its convergence-stopping parameter is low enough to not distort outcomes. We discuss our current research on the formalisation of a proof that the surplus transfer phase of Meek's method of STV converges on a unique and valid weight vector for all elected candidates. Other STV methods have seen formal treatments in recent literature, but thus far that does not appear the case for Meek's method specifically. We consider the representational issues in a formal context, problems and gaps in the proof, and the availability of existing material in Isabelle/HOL for facilitating the work. Slides Document J Palmer June 2020 (1.39 MB / PDF) Jun 22 2020 14.00 - 15.00 22 June 2020 - Jake Palmer Formal verification for Meek's method of STV Online
22 June 2020 - Jake Palmer Link https://eu.bbcollab.com/guest/97e5b2666aa74b30870a4c83ad03760a Speaker Jake Palmer Title Formal verification for Meek's method of STV Abstract Single Transferable Vote (STV) systems are typically counted by hand, but some are complicated enough for that to be infeasible for mid-to-large scale elections, such as Schulze STV and CPO-STV. One other such complicated variant is Meek's method of STV, which also sees use in practice. It is currently in use in a number of local elections in New Zealand, the Royal Statistical Society, and the Stack Exchange network. We propose to verify its correctness in terms of termination and seat-filling, and prove various important properties it possesses (and those it doesn't), as well as characterise when its convergence-stopping parameter is low enough to not distort outcomes. We discuss our current research on the formalisation of a proof that the surplus transfer phase of Meek's method of STV converges on a unique and valid weight vector for all elected candidates. Other STV methods have seen formal treatments in recent literature, but thus far that does not appear the case for Meek's method specifically. We consider the representational issues in a formal context, problems and gaps in the proof, and the availability of existing material in Isabelle/HOL for facilitating the work. Slides Document J Palmer June 2020 (1.39 MB / PDF) Jun 22 2020 14.00 - 15.00 22 June 2020 - Jake Palmer Formal verification for Meek's method of STV Online
