💻 computer science

Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability

Dieser Beitrag adressiert die Einschränkungen bestehender Synthesewerkzeuge bei nicht realisierbaren Spezifikationen der nichtlinearen reellen Arithmetik, indem er ein Framework vorschlägt, das Programme mit rationalen Ein- und Ausgängen synthetisiert, die entweder die Spezifikation erfüllen oder das Nichtvorhandensein korrekt melden, und zwar mit einem vollständigen Algorithmus für Fälle mit einem Ausgang sowie einem korrekten, aber unvollständigen Ansatz für allgemeine Spezifikationen, die im Werkzeug NQSynth implementiert sind.

Ursprüngliche Autoren: S. Akshay, Supratik Chakraborty, R. Govind, Aniruddha R. Joshi

Veröffentlicht 2026-05-26

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: S. Akshay, Supratik Chakraborty, R. Govind, Aniruddha R. Joshi

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie sind ein Meisterkoch (der Computer), der versucht, ein sehr strenges Rezept (die Spezifikation) zu befolgen, um ein Gericht (die Programmausgabe) zuzubereiten.

Das Problem: Das „unmögliche" Rezept

In der Welt der Informatik gibt es eine beliebte Methode namens SyGuS (Syntax-Guided Synthesis). Sie ist wie ein Roboter-Koch, der versucht, ein Rezept zu finden, das für jede denkbare Kombination von Zutaten funktioniert, die man ihm vorlegen könnte.

Manchmal ist das Rezept, das Sie dem Roboter geben, jedoch fehlerhaft. Stellen Sie sich zum Beispiel ein Rezept vor, das sagt: „Backen Sie einen Kuchen, der genau 1 Meter breit ist, aber Sie haben nur eine Backform, die 10 Zentimeter breit ist."

Wenn Sie dem Roboter eine kleine Form geben, kann er einen winzigen Kuchen backen.
Wenn Sie ihm eine riesige Form geben, ist es physikalisch unmöglich, einen 1-Meter-Kuchen darin zu backen.

Alte Werkzeuge (wie SyGuS) betrachten dies und sagen: „Ich gebe auf! Dieses Rezept ist für jeden Fall nicht befolgbaar, also werde ich überhaupt keinen Code schreiben." Sie verweigern die Hilfe sogar für die Fälle, in denen es möglich ist (wie wenn Sie eine kleine Form haben).

Der neue Ansatz: Der „kluge" Koch

Die Autoren dieses Papers, Akshay, Chakraborty, Govind und Joshi, sagen: „Das ist nicht gut genug. Wir brauchen einen Koch, der kochen kann, wenn es möglich ist, und höflich sagt: ‚Das kann ich nicht', wenn es unmöglich ist."

Sie entwickelten eine neue Methode zum Erstellen von Programmen, die nichtlineare reelle Arithmetik (Mathematik mit Kurven, Quadraten und komplexen Beziehungen, nicht nur einfache Addition) handhabt. Ihr Ziel ist es, ein Programm zu synthetisieren, das:

Erfolgt: Wenn die Eingabe eine korrekte Antwort zulässt, berechnet es diese perfekt.
Gibt sich geschlagen: Wenn die Eingabe die Antwort unmöglich macht, stürzt es nicht ab oder rät; es sagt explizit: „Hier existiert keine Lösung."

Die „rationale" Regel: Keine Rundungsfehler

Ein entscheidender Teil ihrer Arbeit ist der Umgang mit Zahlen. Computer verwenden normalerweise „Gleitkommazahlen" (wie 3.14159...), die Annäherungen sind. Wenn Sie Mathematik mit Annäherungen betreiben, entstehen winzige Fehler (Rundungsfehler), die sich zu großen Fehlern aufsummieren können.

Die Autoren entschieden sich für rationale Zahlen (Brüche wie 22/7 oder 3/4).

Analogie: Stellen Sie sich vor, Sie bauen ein Haus. Die Mathematik mit Gleitkommazahlen ist wie die Verwendung eines leicht verbogenen Lineals; Ihre Wände könnten schief stehen. Die rationale Mathematik ist wie die Verwendung eines laserpräzisen Bauplans, bei dem jede Messung exakt ist.
Der Kompromiss: Exakte Mathematik ist langsamer zu berechnen, garantiert aber null Fehler. Die Autoren wollten ein Programm, das mathematisch perfekt ist, nicht nur „gut genug".

Die drei großen Entdeckungen

1. Das „unlösbare" Rätsel (Theoretische Grenzen)
Die Autoren bewiesen, dass das Erstellen eines perfekten Programms für jedes mögliche mathematische Problem so schwer ist wie die Lösung eines berühmten, ungelösten Rätsels in der Mathematik namens Hilberts zehntes Problem (das fragt, ob wir immer feststellen können, ob eine bestimmte Art von Gleichung eine Lösung hat).

Die Metapher: Sie zeigten, dass einen Computer zu bitten, jede mögliche Version dieses Problems zu lösen, wie die Bitte ist, ein Rätsel zu lösen, das selbst die größten Mathematiker noch nicht gelöst haben.
Das Ergebnis: Aus diesem Grund bewiesen sie, dass es unmöglich ist, ein „schleifenfreies" Programm (ein einfaches, geradliniges Rezept) zu schreiben, das jeden Fall löst. Sie benötigen Schleifen (wiederholte Schritte), um die Komplexität zu bewältigen.

2. Das „Einzel-Ausgabe"-Wunder
Während das allgemeine Problem schwierig ist, fanden sie einen „Sweet Spot". Wenn das Programm nur eine einzige Zahl als Ausgabe produzieren muss (wie das Finden nur der Höhe eines Dreiecks), schufen sie einen perfekten, vollständigen Algorithmus.

Wie es funktioniert: Sie verwenden zwei klassische mathematische Tricks:
- Isolierung reeller Wurzeln: Das Finden der exakten „Lücken" auf einer Zahlengeraden, in denen eine Lösung existieren muss.
- Rationaler-Wurzeln-Theorem: Eine Regel, die die Suche nach Antworten auf eine kleine, endliche Liste von Möglichkeiten beschränkt.
Das Ergebnis: Für Probleme mit einer Ausgabe ist ihr Werkzeug (genannt NQSynth) garantiert, die Antwort zu finden, wenn sie existiert, oder korrekt zu sagen, dass sie nicht existiert.

3. Die „gut genug" allgemeine Lösung
Für Probleme mit mehreren Ausgaben (wie das Finden sowohl der Höhe als auch der Breite) ist eine perfekte Lösung zu schwer zu garantieren. Daher bauten sie einen „sound, aber unvollständigen" Algorithmus.

Die Metapher: Denken Sie daran wie an einen Detektiv, der nicht jedes Verbrechen in der Stadt aufklären kann, aber sehr gut darin ist, die zu lösen, denen er begegnet. Wenn sie eine Lösung finden, wissen sie, dass sie zu 100 % korrekt ist. Wenn sie keine finden, haben sie vielleicht nur die Zeit verloren, nicht weil keine Lösung existiert.
Das Ergebnis: Ihr Werkzeug, NQSynth, löste erfolgreich viele schwierige mathematische Probleme, die andere hochmoderne Werkzeuge (wie CVC5) nicht einmal angefasst hatten, selbst wenn diesen anderen Werkzeugen „einfachere" Versionen der Probleme gegeben wurden.

Das Werkzeug: NQSynth

Das Team entwickelte ein Prototyp-Werkzeug namens NQSynth.

Was es tut: Es nimmt eine komplexe mathematische Regel und schreibt ein Python-Programm, das diese Regel perfekt mit Brüchen befolgt.
Die Leistung: In ihren Tests löste NQSynth 59 von 83 schwierigen Benchmarks, während das zweitbeste Werkzeug nur 26 löste. Es war besonders gut darin, „nicht realisierbare" Spezifikationen (die „unmöglichen" Rezepte) zu handhaben, indem es korrekt identifizierte, wann eine Lösung möglich war und wann nicht.

Zusammenfassung

Dieses Paper handelt davon, Computern beizubringen, ehrliche und präzise Mathematiker zu sein. Anstatt aufzugeben, wenn ein Problem unmöglich aussieht, lehrt die neue Methode den Computer:

Exakte Brüche zu verwenden, um Fehler zu vermeiden.
Das Problem zu lösen, wenn es möglich ist.
Selbstbewusst zu sagen: „Das kann ich nicht", wenn es unmöglich ist.

Sie bewiesen, dass zwar eine „perfekte" Lösung für jedes Szenario mathematisch unmöglich ist, sie jedoch ein Werkzeug bauen können, das für Probleme mit einer Variablen perfekt funktioniert und für komplexe Probleme mit mehreren Variablen eine bemerkenswert gute Arbeit leistet, wodurch es die derzeit besten Werkzeuge in diesem Bereich schlägt.

Technischer Überblick: Programmsynthese für nichtlineare reelle Arithmetik: Über die Realisierbarkeit hinaus

Problemdefinition
Dieser Beitrag adressiert das Problem der Synthese von Programmen aus Spezifikationen in der quantorenfreien Theorie der nichtlinearen reellen Arithmetik (NRA). Im Gegensatz zur traditionellen Syntax-gesteuerten Synthese (SyGuS), die versagt, wenn eine Spezifikation „nicht realisierbar" ist (d. h., es existieren Eingabewerte, für die keine Ausgabe die Spezifikation erfüllt), schlägt diese Arbeit ein neues Syntheseziel vor. Das Ziel besteht darin, ein Programm zu synthetisieren, das für jede rationale Eingabe entweder eine rationale Ausgabe erzeugt, die die Spezifikation erfüllt, oder explizit das Nichtvorhandensein einer solchen Ausgabe meldet (bezeichnet durch $\bot$ ).

Um Rundungsfehler zu vermeiden, die in der Festkomma-Arithmetik mit begrenzter Präzision inhärent sind und dazu führen können, dass gültige reelle Lösungen bei der Auswertung mit Approximationen scheitern, beschränken die Autoren den Bereich auf rationale Eingaben und Ausgaben. Dies definiert die Problemklasse RPSQ (Real Program Synthesis with Rational inputs and outputs – Reale Programmsynthese mit rationalen Eingaben und Ausgaben). Die synthetisierten Programme dürfen Schleifen, Verzweigungen und Zuweisungen enthalten, die mit rationalen Zahlen operieren.

Theoretische Härte und Grenzen
Die Autoren etablieren signifikante theoretische Grenzen für dieses Problem:

Inter-Reduzierbarkeit mit Hilberts zehntem Problem: Sie beweisen, dass RPSQ inter-reduzierbar mit Hilberts zehntem Problem über den rationalen Zahlen ( $HTP_{\mathbb{Q}}$ ) ist. Da $HTP_{\mathbb{Q}}$ ein langjähriges offenes Problem der Zahlentheorie ist, impliziert dies, dass ein allgemeiner korrekter und vollständiger Synthesealgorithmus für RPSQ wahrscheinlich nicht existiert.
Unmöglichkeit der Schleifen-freien Synthese: Der Beitrag zeigt, dass RPSQ nicht ausschließlich mit Schleifen-freien Programmen gelöst werden kann. Würde eine Schleifen-freie Lösung existieren, würde dies implizieren, dass die Theorie der rationalen Arithmetik eine Quantorenelimination zulässt, ein Ergebnis, das als unentscheidbar bekannt ist (Robinson, 1959).

Methodik und Algorithmen
Angesichts der allgemeinen Unentscheidbarkeit schlagen die Autoren einen gestuften Ansatz vor:

Realisierbarkeit über Reelle vs. Rationale Zahlen: Sie zeigen, dass, wenn eine Spezifikation über den reellen Zahlen realisierbar ist, jedes von bestehenden SyGuS-Tools synthetisierte Programm (die über reellen Zahlen operieren) auch als gültige Lösung für den rationalen Fall dient, sofern Eingaben und Ausgaben rational sind. Dies gilt jedoch nicht umgekehrt; eine Lösung für rationale Zahlen impliziert nicht notwendigerweise eine Lösung für reelle Zahlen.
Korrekter und vollständiger Algorithmus für einzelne Ausgaben ( $|Y|=1$ ): Für Spezifikationen mit einer einzelnen Ausgabeparameter stellen die Autoren einen korrekten und vollständigen Algorithmus (Algorithmus 1) vor. Dieser Ansatz unterteilt das Problem in zwei Fälle:
- Strenge Ungleichungen: Es wird Real Root Isolation (RRI) verwendet, um Intervalle zu finden, in denen das Vorzeichen von Polynomen invariant ist. Durch das Abtasten rationaler Punkte innerhalb dieser Intervalle (unter Ausnutzung der Dichte der rationalen Zahlen in den reellen Zahlen) werden Lösungen für strenge Einschränkungen gefunden.
- Nicht-strenge Ungleichungen: Für Lösungen, die auf dem Rand liegen (wo nicht-strenge Ungleichungen zu Gleichungen werden), verwendet der Algorithmus den Rational Root Theorem (RRT). Dies ermöglicht die Enumeration einer endlichen Menge von Kandidaten für rationale Nullstellen der aus den Randbedingungen abgeleiteten Polynomgleichungen.
  Der Algorithmus kombiniert diese mit Quantorenelimination (unter Verwendung von QEPCAD), um die schwächsten Vorbedingungen für das Vorhandensein von Lösungen zu bestimmen.
Korrekter, aber unvollständiger Algorithmus für den allgemeinen Fall ( $|Y|>1$ ): Für mehrere Ausgabeparameter schlagen die Autoren Algorithmus 2 vor (implementiert im Tool NQSynth). Dies ist ein korrektes, aber unvollständiges Verfahren, das das Problem mit mehreren Ausgaben iterativ in Teilprobleme mit einzelnen Ausgaben zerlegt:
- Es fragt einen NRA-Oracle (Z3) nach einer rationalen erfüllenden Belegung (Modell) ab.
- Es fixiert alle außer einer Ausgabeparameter basierend auf diesem Modell, wodurch das Problem auf eine Instanz der Synthese mit einer einzigen Ausgabe reduziert wird, die durch den oben beschriebenen vollständigen Algorithmus lösbar ist.
- Es konstruiert eine Entscheidungsliste (eine Reihe von if-then-else-Zweigen), wobei jeder Zweig einer spezifischen Vorbedingung entspricht, die durch Quantorenelimination abgeleitet wurde.
- Der Prozess wiederholt sich, indem die Spezifikation durch Negation der Vorbedingungen der gefundenen Lösungen verfeinert wird, bis die Spezifikation unerfüllbar wird oder ein Timeout eintritt.

Implementierung und experimentelle Ergebnisse
Die Autoren implementierten ihren Ansatz in einem Prototyp-Tool namens NQSynth. Sie bewerteten es gegen zwei konkurrierende Ansätze:

QEPCAD+CVC5: Eine modifizierte SyGuS-Pipeline, die zuerst die schwächste Vorbedingung über reellen Zahlen berechnet und dann ein Programm synthetisiert.
ModEnum: Ein auf Modellen basierender Enumerationsansatz, inspiriert von Monniauxs Arbeit zur linearen Arithmetik.

Die Bewertung verwendete zwei Benchmark-Sets:

NRA-Benchmarks: 83 angepasste Benchmarks aus dem SMT-LIB 2024-Repository (Families meti-tarski/Arthan, asin, zankl).
Geometrische Benchmarks: 51 Spezifikationen, die 2D- und 3D-geometrische Beziehungen modellieren (Kreise, ringförmige Bereiche, Hyperbeln).

Hauptergebnisse:

NQSynth löste 59 von 83 NRA-Benchmarks und 33 von 51 geometrischen Benchmarks innerhalb eines 120-Sekunden-Timeouts.
Im Gegensatz dazu löste QEPCAD+CVC5 26 NRA- und 16 geometrische Benchmarks, während ModEnum 23 NRA- und 11 geometrische Benchmarks löste.
Bemerkenswerterweise synthetisierte NQSynth erfolgreich Programme für viele Spezifikationen, die nicht realisierbar waren (oder bei denen die Berechnung der schwächsten Vorbedingung schwierig war), ein Szenario, in dem SyGuS-Tools vollständig versagen.
Die Experimente zeigten, dass die Hauptengpassstelle für NQSynth der Schritt der Quantorenelimination (QEPCAD) war, insbesondere bei größeren Eingaben, und nicht die Syntheselogik selbst.

Bedeutung und Behauptungen
Der Beitrag behauptet, eine neue Technik zum Repertoire der Programmsynthese aus NRA-Spezifikationen hinzuzufügen. Seine primäre Bedeutung liegt in:

Umgang mit Nicht-Realisierbarkeit: Es bietet eine praktische Methode, um Programme zu synthetisieren, die Eingaben, für die keine Lösung existiert, elegant handhaben, eine Fähigkeit, die aktuellen SyGuS-Tools des State-of-the-Art fehlt.
Rationale Präzision: Durch die Zielsetzung rationaler Eingaben und Ausgaben werden Rundungsfehler vermieden, die mit der Gleitkomma-Arithmetik verbunden sind, und mathematische Korrektheit für Anwendungen mit hoher Präzision gewährleistet.
Über SyGuS hinaus: Der Ansatz löst Probleme, die außerhalb der Reichweite bestehender SyGuS-Tools liegen, selbst für realisierbare Spezifikationen, indem er zahlentheoretische Eigenschaften (RRT und RRI) nutzt, anstatt sich ausschließlich auf syntaktische Suche oder Standard-Quantorenelimination zu verlassen.

Die Autoren schließen, dass, obwohl eine allgemeine vollständige Lösung aufgrund der Härte von $HTP_{\mathbb{Q}}$ theoretisch unwahrscheinlich ist, ihr korrektes und unvollständiges Verfahren eine robuste praktische Lösung bietet, die bestehende Methoden bei einer breiten Palette von Benchmarks erheblich übertrifft. Als zukünftige Arbeit wird vorgeschlagen, Bedingungen zu untersuchen, unter denen Schleifen-freie Programme ausreichen, und die Abhängigkeit von schweren Quantoreneliminations-Engines zu reduzieren.