Verified Construction of Fair Voting Rules

@InProceedings{DiekhoffKirstenKraemer2020,
  author        = {Karsten Diekhoff and
                   Michael Kirsten and
                   Jonas Kr{\"{a}}mer},
  title         = {Verified Construction of Fair Voting Rules},
  booktitle     = {29th International Symposium on Logic-Based Program
                   Synthesis and Transformation ({LOPSTR} 2019),
                   Revised Selected Papers},
  venue         = {Porto, Portugal},
  eventdate     = {2020-10-08/2020-10-10},
  series        = {Lecture Notes in Computer Science},
  editor        = {Maurizio Gabbrielli},
  year          = {2020},
  month         = apr,
  abstract      = {Voting rules aggregate multiple individual preferences in order to
                   make collective decisions. Commonly, these mechanisms are expected
                   to respect a multitude of different fairness and reliability
                   properties, e.g., to ensure that each voter's ballot accounts for
                   the same proportion of the elected alternatives, or that a voter
                   cannot change the election outcome in her favor by insincerely
                   filling out her ballot. However, no voting rule is fair in all
                   respects, and trade-off attempts between such properties often
                   bring out inconsistencies, which makes the construction of arguably
                   practical and fair voting rules non-trivial and error-prone.
                   \newline

                   In this paper, we present a formal and systematic approach for the
                   flexible and verified construction of voting rules from composable
                   core modules to respect such properties by construction. Formal
                   composition rules guarantee resulting properties from properties of
                   the individual components, which are of generic nature to be reused
                   for various voting rules. We provide a prototypical logic-based
                   implementation with proofs for a selected set of structures and
                   composition rules within the theorem prover Isabelle/HOL. The
                   approach can be readily extended in order to support many voting
                   rules from the literature by extending the set of basic modules and
                   composition rules. We exemplarily construct the well-known voting
                   rule sequential majority comparison (SMC) from simple generic
                   modules, and automatically produce a formal proof that SMC
                   satisfies the fairness property monotonicity. Monotonicity is a
                   well-known social-choice property that is easily violated by voting
                   rules in practice.},
  publisher     = {Springer},
  doi           = {10.1007/978-3-030-45260-5_6},
  volume        = {12042},
  pages         = {90--104}
}