ProofOfThought: LLM-basiertes Reasoning mit Z3-Theorembeweisen

• ProofOfThought kombiniert Large Language Models (LLMs) mit dem Z3-Theorembeweiser, um leistungsstarkes und interpretierbares Reasoning zu ermöglichen
• Das Projekt liefert für natürlichsprachliche Anfragen präzise und verlässliche Reasoning-Ergebnisse
• Über eine hochstufige Python-API können Entwickler komplexe Reasoning-Aufgaben einfach implementieren und erproben
• Mit Z3DSL wird auch ein JSON-basiertes Low-Level-DSL bereitgestellt, das flexible Anpassungen ermöglicht
• Die Veröffentlichung beim Sys2Reasoning Workshop NeurIPS 2024 zeigt die Vorteile der praktischen Nutzbarmachung aktueller Forschungsergebnisse

---

Vorstellung des Open-Source-Projekts ProofOfThought

ProofOfThought ist eine Open-Source-Reasoning-Bibliothek, die einen neurosymbolischen Programmsynthese-Ansatz einsetzt und dabei Large Language Models (LLMs) mit dem Z3-Theorembeweiser kombiniert. Dass sie für komplexe reale Probleme robuste und interpretierbare Reasoning-Ergebnisse liefert, ist sowohl für den praktischen Einsatz als auch für die Forschung von großer Bedeutung.

Als Open-Source-Projekt kann es von allen frei für Forschung, Services und Entwicklung genutzt werden. Gegenüber herkömmlichen, rein LLM-basierten Reasoning-Systemen bietet es den Vorteil, dass sich der Reasoning-Prozess leichter verifizieren und Fehler leichter interpretieren lassen. Im Vergleich zu anderen Reasoning-Systemen ist besonders die strukturelle Transparenz des Ablaufs natürlichsprachliche Eingabe → automatische Umwandlung in ein Logikprogramm → Z3-basiertes Reasoning hervorzuheben.

Systemarchitektur und Hauptbestandteile

• High-Level-API (z3dsl.reasoning) :

  • Ausführung von Reasoning-Anfragen auf Basis natürlicher Sprache
  • Bereitstellung einer Python-Schnittstelle, die auch für Einsteiger leicht nutzbar ist

• Low-Level-DSL (z3dsl) :

  • JSON-basierter Zugriff auf den Z3-Theorembeweiser
  • Vorteilhaft für komplexe Anpassungen und den Aufbau automatisierter Pipelines

Beispiele für zentrale Funktionen

• Das LLM wandelt die eingegebene Anfrage in logische Ausdrücke (symbolische Programme) um

• Über den Z3-Beweiser werden Wahr/Falsch-Ergebnisse (yes/no) oder bedingungsbasierte Interpretationen erzeugt

• Beispiel:

  • Anfrage: "Würde Nancy Pelosi Abtreibung öffentlich verurteilen?"
  • Ergebnis: False (nein)

• Bereitstellung einer Evaluierungspipeline (EvaluationPipeline):

  • Batch-Auswertung großer Datensätze möglich
  • Automatisches Reporting, etwa zur Genauigkeit

Einsatz- und Anwendungsszenarien

• Automatisierung von Reasoning-Benchmarks für Forschungszwecke
• Services zum automatischen Beweisen von LLM-basierten Wissensgraphen oder Problemen höherer Logik
• Potenzial für den Einsatz in verschiedensten AI-Services wie komplexen Policy-Anfragen oder der automatischen Beurteilung natürlichsprachlicher Debatten

Wissenschaftliche Bedeutung und Merkmale

• Präsentiert beim Sys2Reasoning-Workshop der NeurIPS 2024
• Symbolisch interpretierbare Verlässlichkeit, die bestehende LLM-Grenzen (Unsicherheit im Reasoning) ergänzt
• Transparenz und Interpretierbarkeit von Reasoning-Ergebnissen und ihrer Begründung sind große Stärken für die Entwicklung realer Services

Fazit

ProofOfThought bietet Entwicklern und Forschern, die eine robuste und interpretierbare AI-Reasoning-Infrastruktur aufbauen möchten, einen konkreten praktischen Mehrwert, indem es die Stärken von LLMs und dem Z3-Theorembeweiser kombiniert. Lizenz und Struktur des Projekts sind passend für das Open-Source-Ökosystem gestaltet und machen es sowohl für akademische Forschung als auch für industrielle Nutzung attraktiv.

[GN⁺]

Hacker-News-Kommentare

• Es wird von einer interessanten Erfahrung mit Gemini 2.5 Pro berichtet. Beim Versuch, ein lineares Gleichungssystem in einem Online-CAS zu lösen, funktionierte das CAS nicht wie erwartet, also wurde Gemini um Hilfe gebeten, und Gemini präsentierte direkt die Lösung. Es erklärte, dass dafür das Python-Paket sympy verwendet wurde. Es wird der Eindruck geteilt, dass die Kombination aus einem unscharfen LLM und einem strengen Tool sehr wirkungsvoll sein kann
  • Fühlt sich ähnlich wie beim Menschen an. Wir sind schlecht in komplexen Berechnungen, bauen aber großartige Computer, die das gut erledigen. Und nach enormem Aufwand bauen wir Programme, die auf Zahlenberechnung basierend mehr oder weniger Text vorhersagen, aber in schwierigen Berechnungen ungeschickt sind. Am Ende können diese Programme vorhersagen, wie man Programme erstellt und nutzt, die stark in Zahlenberechnung sind
  • Die Kombination aus LLM und sympy für Mathematik gefällt mir wirklich gut. Wenn man das LLM sympy-Code schreiben lässt, kann man darauf vertrauen, dass symbolische Operationen korrekt ausgeführt wurden. Der Code selbst bleibt als Artefakt erhalten und kann schrittweise von Menschen oder LLMs überarbeitet und verbessert werden, außerdem per Git-Historie verwaltet werden. Durch bestandene Tests und Verifikation bleibt das Vertrauen in die mathematische Korrektheit erhalten. Ich nutze auch Hilfsfunktionen, die sympy-Code leicht nach LaTeX konvertieren. Kürzlich habe ich mathematische Arbeiten zum Quantum-Eraser-Experiment auf diese Weise durchgeführt. github-Link
  • Ich verstehe, dass es ein brauchbarer Ansatz ist, den Problemlösungsprozess gemeinsam mit einem LLM und Tools nachzuverfolgen. In der Praxis funktionierte das sogar besser als erwartet. Aber statt ein CAS zu verwenden, das LLM zur Bearbeitung von Mathematik zu bewegen, ist wie ein Wohnungsumzug, bei dem man statt eines Lastwagens mehrfach mit dem Bus hin- und herfährt. So die Analogie, nur weil man bereits eine Busfahrkarte hat
• Es wird betont, dass ein LLM letztlich ein statistisches Sprachmodell ist. Aus Erfahrung funktioniert die Generierung von Logikprogrammen, insbesondere Prolog-Quellcode, besser als erwartet. Vermutlich liegt das daran, dass Prolog in die symbolische Verarbeitung natürlicher Sprache eingeführt wurde und im Trainingsdatensatz auch reichlich Übersetzungsbeispiele vorhanden sind. Es könnte sich lohnen, in Z3 statt der SMTLib-Syntax die Datalog-Syntax von Z3 zu verwenden. Empfohlen werden die zugehörige Demo und die Z3-Datalog-Syntax
  • Die Datalog-Syntax in Z3 ist ziemlich gut. Wir haben im Grammars-Paper SMT verwendet, weil die Kompatibilität mit verschiedenen Solvern am höchsten war. Aber wir haben im NeurIPS-Begutachtungsprozess getestet, dass der Ansatz auch mit PROLOG gut funktioniert. Ich erwarte, dass es auch mit Datalog funktioniert. Paper-Link, Datalog-Beispiel
• Das wirkt wie ein interessanter Ansatz. Unser Team hat in ähnlicher Weise einen Prototyp gebaut, der Geschäftsrichtlinien in LEAN kodiert. Das LLM wandelt die Wissensbasis aus internen Wikis oder Google Docs zunächst in LEAN-Code um. Danach wird ein Solver zur Konsistenzprüfung ausgeführt. Wenn das Wiki geändert wird, läuft der gesamte Prozess erneut und dient so als eine Art Prozess-Linter. Allerdings blieb es beim Prototypen, weil die LEAN-Transformation selbst noch Prüfung durch Ingenieure erfordert. Für Domänen mit rechtlichen oder finanziellen Compliance-Anforderungen scheint das aber vielversprechend
  • Es wird erwähnt, dass die Hürde der automatischen Formalisierung wirklich hoch ist. Aus unserem NeurIPS-2025-Paper teilen wir die Erfahrung, dass wir die Unsicherheit automatischer Formalisierung für klar definierte Grammatiken quantifiziert und analysiert haben. Paper-Link Wenn jemand eine ausführlichere Diskussion möchte, kann er sich jederzeit melden
  • Für alle, die sich fragen, was LEAN ist: Es ist der von Microsoft entwickelte Lean Theorem Prover. Projektlink
  • Mich interessieren konkrete Beispiele. Ich würde gern hören, welche Art von Richtlinien in der Praxis so präzise beschrieben sind, dass man sie in LEAN definieren kann
  • Es scheint sehr nützlich zu sein, dass sich mit diesem Ansatz widersprüchliche Richtlinien systematisch identifizieren lassen
• Ein sehr interessantes Forschungsfeld. Vor einigen Jahren habe ich mit logik- und wahrscheinlichkeitbasierten Reasoning-Engines überprüft, ob Prämissen sauber zu Schlussfolgerungen führen. Außerdem habe ich Agents eingesetzt, um Domänenwissen zu synthetisieren, zu formalisieren und zu kritisieren. Es ist keine Wunderwaffe, aber ein gewisses Maß an Genauigkeit ließ sich absichern. Ich denke, dass ein gewisser Grad an Symbolik und das Konzept agent-as-a-judge für die Zukunft vielversprechend sind. Referenz-Paper
  • Ich habe die Arbeit gelesen. Ziemlich cool. Ich habe kürzlich ebenfalls bei AWS ARChecks einen Autoformalization-Agenten gebaut. Das ist noch nicht öffentlich, aber es gibt bereits allgemein verfügbare Produkte, die als Referenz dienen können AWS-Blog
  • Agent/LLM als Richter zu verwenden, ist meiner Ansicht nach verzerrt und nur fürs Bootstrapping geeignet. Wenn die Leistung hoch genug wird, wird der LLM-Richter künstlich zum Engpass, daher muss man letztlich zu menschlichen Expertenrichtern oder deterministischen Orakeln übergehen
• Es wird erwähnt, dass der knife-edge rolling kernel von RHEL für den Proof of Concept verwendet wurde
• Ich hatte das Gefühl, dass dem Repository eine ausführlichere Erklärung fehlt, was daran liegen könnte, dass es als Begleitmaterial zum Paper dient. Im Kern scheint es eine API zu sein, mit der man ein LLM Z3-Programme erzeugen lässt. Es soll reale Anfragen logisch ausdrücken und dabei Fakten, Inferenzregeln und Ziele erfassen. Die Aufsichtsfunktion besteht darin, logische Beschreibungen direkt lesen und den Solver ausführen zu können, um wahr/falsch zu überprüfen. Meine Zweifel sind: Wer soll all diese SMT-Regeln einzeln lesen und mit der Realität abgleichen? Wer prüft die Konstantenwerte? Und könnte das LLM nicht versehentlich oder zur Zielerreichung logisch oder realitätsfern falsche Regeln hinzufügen? Das Paper meldet 51 % False Positives auf einem Logik-Benchmark, was überraschend hoch ist und als Signal dafür gedeutet wird, dass LLMs im logischen Modellieren schwach sind oder unvollständige Regeln erzeugen. Die Evaluation ist dürftig und erklärt nicht klar, warum das passiert
  • Es wird behauptet, dass dieses Paper letztes Jahr mit GPT-4o geschrieben wurde und sich die Lage mit neueren Modellen stark verbessert hat. Zum Beispiel vergleicht ein aktuelles Paper in Tab 1 textbasiertes und SMT-basiertes Abschneiden. o3-mini bringt Text-Reasoning und Ergebnisse auf SMT gut in Einklang. Im kommerziellen Produkt AWS Automated Reasoning Checks wird ein Domänenmodell erstellt und verifiziert, und in der Phase der Antwortgenerierung werden die Q/A-Paare des LLMs durch strikte Solver-Verifikation darauf geprüft, ob sie die Richtlinien einhalten. Dadurch könne die politikbezogene Gültigkeit von Q/A-Paaren mit über 99 % abgesichert werden AWS-Blog
• Es ist eine Frage, ob die eigene Interpretation stimmt. Wenn die probabilistische Ausgabe eines LLM in ein logisches Modell überführt wird, ist das dann nicht einfach nur „garbage in, garbage out“?
  • Formale Logik dient als Filter. Also eher: „garbage in, filtered garbage out“. Die Analogie lautet, dass auch die Evolution zufälligen „Müll“ in Form von Mutationen hervorbringt, der dann von der natürlichen Umgebung herausgefiltert wird
  • Es kommt nicht immer „Müll“ heraus. Ziemlich oft entsteht nützliche Ausgabe, und genau das macht es sinnvoll
  • Das ist eine subjektive Bewertung. Man könnte schließlich auch alles, was die Menschheit in den letzten Jahrtausenden hervorgebracht hat, als Müll ansehen. Streng genommen war ein Leben in Höhlen vielleicht einfacher
• Es ist sehr faszinierend, dass KI nicht nur „denkt“, sondern auch ein überprüfbares Tagebuch hinterlässt. Das wirkt, als würde ein Philosoph mit einem kryptografischen Notar leben. Wirklich erstaunliche Arbeit
• Die Kernidee ist, dass das LLM den Reasoning-Prozess zunächst strukturiert in einem JSON-DSL entwirft und dieser dann deterministisch in Logik erster Ordnung übersetzt wird, um in Z3 einen Theorembeweis zu versuchen. Dadurch besteht die finale Ausgabe aus beweisbaren Schlussfolgerungen (oder Gegenbeispielen) und unterscheidet sich somit von bloß überzeugend klingenden Textketten
• Interessante Forschung. Ich habe ins Repo geschaut, weil mich DSL-Beispiele interessiert haben, aber es war schwer, klare Beispiele zu finden. Ein Beispiel-Code-Snippet im README wäre hilfreich
  • Danke für das Interesse, wir werden das bald ergänzen. Bis dahin gibt es ab Seite 11 des Papers mehrere Szenarien zur Erklärung Paper-PDF