Automated Verification and Generation of Voting Rules Using Composable Modules
|Forschungsthema:||Computational Social Choice|
Voting rules describe how a collective decision can be derived from a
collection of individual decisions.
While a voting rule should obviously be fair, it is far from obvious what being
fair even means.
While an individual notion of fairness might exist, it is insufficient for
formal analysis of voting rules.
Therefore, voting rules and their properties have been formally defined and
examined using methods of mathematics and formal logics, and it was proven that
no single voting rule can satisfy all intuitively desirable properties.
In this thesis, we present an automatic approach to the generation of voting rules satisfying certain properties. It is based on a modular framework verified within Isabelle/HOL for constructing voting rules as compositions of simple modules. This allows for proving properties of voting rules in a structured manner from properties of the smaller components. This generation process is implemented and automated such that from a given set of desired properties, an executable voting rule satisfying those is automatically generated, if possible. Moreover, we automatically generate a machine-verified proof that the voting rule does indeed satisfy the required properties. The pipeline can also be used to generate proofs for properties of user-specified voting rules. As a theoretical foundation, we formally define the voting rule generation as a decision problem and prove its general decidability. From this, we obtain well-founded claims decidability results of whether a voting rule satisfying some properties can be defined within the framework or not. Finally, we provide flexible C code snippets for selected modules such that a generated voting rule can be analysed for further properties using the verification technique of software bounded model checking, so that either (for a violated property) we can generate understandable counterexamples, or show that no such counterexample exists up to a specified bound on the number of voters and candidates.
- "Automated Verification for Functional and Relational Properties of Voting Rules" in Sixth International Workshop on Computational Social Choice (COMSOC 2016)
- "Towards automatic argumentation about voting rules" in 4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)
- "Verified Construction of Fair Voting Rules" in 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019)