Automatic Logic-Based Margin Computation for Efficient Election Audits
Forschungsthema: | Social Choice |
---|---|
Typ: | BA |
Datum: | 2017-05-14 |
Betreuer: | Michael Kirsten |
Aushang: |
Beschreibung
Eine sogenannte risk-limiting audit ist ein effizientes Prüfungsverfahren,
das ein konkretes Wahlergebnis mit einem konfigurierbaren Konfidenzwert auf seine
(entsprechend wahrscheinliche) Korrektheit prüft.
Hierzu werden nach einem bestimmten Verfahren zufällig gewählte Stichproben von
Wahlzetteln mit ihrer ausgewerteten Interpretation verglichen.
Allerdings hängt die Größe dieser Stichproben, die sich entscheidend auf den
Aufwand des Prüfverfahrens auswirkt, vom sogenannten margin of victory ab,
der beschreibt, wie viele Stimmzettel man mindestens ändern müsste, um ein
anderes Wahlergebnis zu erhalten.
Je nach Wahlverfahren kann die Berechnung dieser Zahl alleine schon sehr
kompliziert und aufwändig sein.
Am Lehrstuhl für Anwendungsorientierte Formale Verifikation haben wir hierzu
ein allgemeines logik-basiertes Verfahren entwickelt, das diesen Wert für eine
Vielzahl von Wahlverfahren automatisch berechnen kann.
Hierzu wird allerdings einerseits eine gewisse Worst-Case-Annahme getroffen,
nach der jede Änderung eines Stimmzettels einen maximalen Effekt haben kann,
andererseits ist man bei der Prüfung eines konkreten Wahlergebnisses oft an
konkreteren Ausssagen interessiert, beispielsweise ob (im Fall des deutschen
Bundestags) die Koalition bestimmter Parteien wirklich eine Mehrheit aller
Stimmen erhalten hat.
Solche (und eventuell weitere) Anpassungen des am Lehrstuhl entwickelten
Verfahrens sollen innerhalb dieser Bachelorarbeit umgesetzt und an echten
Wahlergebnissen evaluiert werden.
Hierzu ist insbesondere ein gewisses Verständnis der statistischen Grundlagen
von risk-limiting audits notwendig, bzw. die Bereitschaft sich diese anzueignen.
Voraussetzungen
- Grundkenntnisse in und Interesse an formalen Methoden, wie sie z. B. in der Vorlesung Formale Methoden vermittelt werden
- Gründliche Arbeitsweise sowie ein gutes Abstraktionsvermögen
Kontakt
Interesse? Weitergehende Fragen? Dann melden Sie sich unverbindlich bei Michael Kirsten (Raum 228, Geb. 50.34).
Literatur
- "Automatic Margin Computation for Risk-Limiting Audits"
in International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016) - "Risk-Limiting Post-Election Audits: Why and How" in Whitepaper University of California, Berkeley (2012)
- "A Gentle Introduction to Risk-Limiting Audits." in IEEE Security & Privacy 10(5) (2012)
- "A Tool for Checking ANSI-C Programs" in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)