Nonlinear Arithmetic with SMTLIB Division is Undecidable

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Rätsel mit Hilfe eines sehr strengen Regelwerks zu lösen. In der Welt der Informatik werden diese Regeln „Theorien" genannt, und sie helfen Computern dabei zu entscheiden, ob ein mathematisches Rätsel eine Lösung hat oder nicht.

Diese Arbeit behandelt einen spezifischen Satz von Regeln namens Nichtlineare Reelle Arithmetik (NRA). Betrachten Sie dies als ein Spiel mit reellen Zahlen (wie 3,14, -5 oder 0,001), bei dem Sie diese addieren, subtrahieren, multiplizieren und dividieren können.

Die „magische" Regel, die das Spiel zerstört

Lange Zeit glaubten Mathematiker, dieses Spiel sei perfekt lösbar. Wenn Sie einem Computer ein Rätsel mit diesen Zahlen gaben, konnte er schließlich sagen: „Ja, es gibt eine Lösung" oder „Nein, es gibt keine."

Der Autor, Dejan Jovanović, entdeckte jedoch eine versteckte Falle im offiziellen Regelbuch (dem SMTLIB-Standard). Die Falle liegt darin, wie die Regeln mit der Division durch Null umgehen.

In der normalen Mathematik ist die Division durch Null ein großes „Nein". Aber in diesem spezifischen Computer-Regelbuch besagen die Regeln: „Wenn Sie durch Null teilen, ist es uns egal, was das Ergebnis ist. Es kann alles sein, solange es sich wie eine normale Zahl verhält, wenn Sie nicht durch Null teilen."

Der Autor nennt dies eine „nicht interpretierte Funktion". Um eine Analogie zu verwenden: Stellen Sie sich einen Automaten vor, der für jeden Snack, den Sie kaufen, perfekt funktioniert. Aber wenn Sie versuchen, einen „Null-Snack" zu kaufen, stürzt der Automat nicht ab; stattdessen spuckt er einfach etwas aus – vielleicht einen Schokoriegel, vielleicht einen Stein, vielleicht eine Wolke. Die Regeln sagen Ihnen nicht, was es sein wird; sie sagen nur: „Es wird etwas sein."

Wie dies das Spiel unlösbar macht

Die Arbeit argumentiert, dass diese „alles ist erlaubt"-Regel für die Division durch Null der Schlüssel ist, der eine Tür zum Chaos öffnet.

Hier ist die Logik, vereinfacht:

1. Das Ziel: Der Autor möchte beweisen, dass Sie mit dieser „magischen" Divisionsregel den Computer dazu bringen können, Ganzzahl-Rätsel zu lösen (Rätsel mit ganzen Zahlen wie 1, 2, 3).
2. Das Problem: Es ist bekannt, dass es für Computer unmöglich ist, Ganzzahl-Rätsel in jedem Fall perfekt zu lösen (dies ist als Hilberts zehntes Problem bekannt). Es ist wie der Versuch, eine Nadel in einem Heuhaufen zu finden, der ständig wächst.
3. Der Trick: Der Autor zeigt, dass Sie durch die Verwendung der „magischen" Division durch Null eine mathematische Brücke bauen können. Sie können ein schwieriges Ganzzahl-Rätsel nehmen und es mit diesem Divisions-Trick in ein Reellzahler-Rätsel übersetzen.
   • Analogie: Stellen Sie sich vor, Sie haben einen geheimen Code in einer Sprache, die nur Menschen verstehen (Ganzzahlen). Sie bauen eine Maschine (den Divisions-Trick), die diesen Code in eine Sprache übersetzt, die Computer verstehen (reelle Zahlen). Da die Computersprache diese „magische" Null-Divisions-Regel hat, kann der Computer versehentlich den menschlichen Code lösen.
4. Das Ergebnis: Da wir wissen, dass Computer nicht alle Ganzzahl-Rätsel lösen können, und dieser Trick es ihnen ermöglicht, Ganzzahl-Rätsel mit reellen Zahlen zu lösen, bedeutet dies, dass der Computer auch nicht alle Reellzahler-Rätsel lösen kann. Das Spiel wird unentscheidbar.

Die Analogie der „Gaußklammer"-Funktion

Um dies zu beweisen, verwendet der Autor einen cleveren Trick. Er zeigt, dass Sie mit dieser „magischen" Division den Computer dazu zwingen können, sich wie eine Gaußklammer-Funktion zu verhalten (eine Funktion, die eine Zahl auf die nächste ganze Zahl abrundet, wie zum Beispiel die Umwandlung von 3,9 in 3).

Sobald der Computer Zahlen abrunden kann, kann er anfangen, Ganzzahlen zu zählen. Sobald er Ganzzahlen zählen kann, kann er versuchen, diese unmöglichen Ganzzahl-Rätsel zu lösen. Da diese Rätsel im Allgemeinen unlösbar sind, wird das gesamte System der Mathematik mit reellen Zahlen unter dieser Divisionsregel im Allgemeinen unlösbar.

Was dies für die reale Welt bedeutet (laut der Arbeit)

Die Arbeit spricht nicht über zukünftige KI oder medizinische Anwendungen. Sie konzentriert sich auf den aktuellen Stand der Computer-Benchmarks (Testprobleme):

• Die Falle: Viele bestehende Testprobleme in der SMTLIB-Bibliothek (eine riesige Sammlung mathematischer Rätsel zur Überprüfung von Computern) verwenden Division mit Variablen (wie x / y). Wenn y zufällig Null ist, fallen diese Rätsel in die „unentscheidbare" Falle.
• Die Lösung? Der Autor schlägt zwei Wege vor, um das Regelbuch zu korrigieren:
  1. Eine spezifische Antwort wählen: Entscheiden Sie, dass die Division durch Null immer einer bestimmten Zahl entspricht (wie 0 oder 1), genau wie einige Computersysteme dies für Binärzahlen handhaben.
  2. Das Spiel aufteilen: Erstellen Sie eine neue, separate Kategorie für Probleme, bei denen Sie durch Variablen teilen, und behalten Sie die „sichere" Kategorie für Probleme bei, bei denen Sie nur durch bekannte Zahlen (Konstanten) teilen.

Das Fazit

Die Arbeit behauptet, dass eine spezifische, scheinbar harmlose Regel darüber, wie Computer mit „Division durch Null" umgehen, versehentlich die Fähigkeit von Computern zerstört, alle mathematischen Probleme mit reellen Zahlen zu lösen. Sie verwandelt ein lösbares Spiel in ein unlösbares, indem sie dem Computer erlaubt, heimlich Probleme zu lösen, die er nicht lösen dürfte.