Home  |  english  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Logic-Based Synthesis of Fair Voting Rules Using Composable Modules

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Karsten Diekhoff, Michael Kirsten und Jonas Krämer
In:29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019)
Jahr:2019

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.
In this paper, we present a formal systematic approach for the flexible synthesis 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 synthesize the well-known voting rule sequential majority comparison (SMC) from simple generic modules, and automatically produce a 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.

Anmerkung

To appear.

BibTeX

@InProceedings{DiekhoffKirstenKraemer2019b,
  author        = {Karsten Diekhoff and
                   Michael Kirsten and
                   Jonas Kr{\"{a}}mer},
  title         = {Logic-Based Synthesis of Fair Voting Rules Using Composable Modules},
  booktitle     = {29th International Symposium on Logic-Based Program
                   Synthesis and Transformation ({LOPSTR} 2019)},
  editor        = {Maurizio Gabbrielli},
  year          = {2019},
  month         = oct,
  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 systematic approach for the
                   flexible synthesis 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 synthesize the well-known voting rule sequential
                   majority comparison (SMC) from simple generic modules, and
                   automatically produce a 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.},
  note          = {To appear.}
}