Servicenavigation

Project Details

Back

Projekt Print View

Interactive and probabilistically checkable proofs in real number models

Subject Area Theoretical Computer Science
Term from 2011 to 2014
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 195586166
 
Final Report Year 2015

Final Report Abstract

Hauptgegenstand der Untersuchungen war die Frage nach der Stärke interaktiver und probabilistisch prüfbarer Beweise im Rahmen von Rechenmodellen, die auf überabzählbaren Strukturen wie den reellen Zahlen arbeiten. Bei derartigen Beweisen soll sich ein mit gewissen Ressourcen ausgestatteter randomisierter Algorithmus, der sogenannte Verifizierer, von der Richtigkeit einer mathematischen Aussage überzeugen. Dabei wurden verschiedene Szenarien betrachtet. Im Mittelpunkt des Projekts standen sogenannte probabilistisch prüfbare Beweise. Bei diesen überprüft der Verifizierer einen ihm vorgelegten potentiellen Beweis einer Aussage auf Richtigkeit. Eine wesentliche Frage ist jetzt, für welche Klassen von Aussagen dies dem Verifizierer mit welchen Ressourcen gelingt. Eines der zentralen Ergebnisse der theoretischen Informatik in den letzten zwei Dekaden ist der sogenannte PCP-Satz. Er besagt, dass NP-vollständige Probleme im Turingmodell randomisiert verifiziert werden künnen. Dabei erzeugt der Verifizierer eine logarithmische Anzahl von Zufallsbits und prüft anschliessend lediglich konstant viele Stellen des vorgelegten Beweises, um mit hoher Wahrscheinlichkeit richtig zu entscheiden. Im Projekt wurde dieser Satz fiir das Rechenmodell von Blum, Shub und Smale uüber sowohl den reellen wie den komplexen Zahlen untersucht und schlussendlich auch bewiesen. Ein typisches NP-vollständiges Problem über diesen Strukturen ist das Hilbert-Nullstellensatz-Problem. Dabei wird gefragt, ob ein vorgelegtes polynomiales Gleichungssystem über dem entsprechenden Körper eine Lösung besitzt. Die Projektergebnisse zeigen, dass es möglich ist, für die (potentielle) Lösbarkeit eines vorgelegten Systems einen (potentiellen) Beweis anzugeben, der randomisiert nur in konstant vielen Stellen zu prüfen ist, um mit hoher Wahrscheinlichkeit zu schlussfolgern, ob er korrekt ist. Es konnte im Wesentlichen gezeigt werden, dass sich dieser neue PCP-Satz wie auch die diskrete klassische Variante sowohl mit graphentheoretischen als auch mit algebraischen Methoden beweisen lässt. Dabei war es allerdings nötig, die bekannten Beweistechniken deutlich zu erweitern, um den Problemen Rechnung zu tragen, die durch Betrachtung überabzählbarer Strukturen entstehen. Die Ergebnisse implizieren ebenfalls, dass es (unter Standardvoraussetzungen der Komplexitätstheorie) nicht möglich ist, die maximale Anzahl von gemeinsam lösbaren Gleichungen eines Polynomsystems effizient zu approximieren. Beim oben erwähnten zweiten Szenario, den interaktiven Beweisen, tauscht der Verifizierer mit einem beliebig machtvollen sogenannten Beweiser gemäß eines Kommunikationsprotokolls Informationen aus. Am Ende dieses Prozesses trifft der Verifizierer wiederum seine Entscheidung, ob er von der Richtigkeit des Beweises überzeugt ist. Hier wurden im letzten Teil des Projekts erste Ergebnisse zur Mächtigkeit dieser interaktiven Protokolle im reellen Rechenmodell erzielt. Dazu gehören der Nachweis einer oberen Schranke für Probleme, die derart behandelt werden können sowie der Entwurf solcher Protokolle für konkrete Problemklassen.

Publications

 
 

Additional Information

© 2025 DFG Disclaimer / Copyright / Privacy Policy

Textvergrößerung und Kontrastanpassung