Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

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