Gödel's Poetry: Automatisiertes Theorembeweisen mit KI

Forscher haben ein neues System vorgestellt, das die Grenzen des automatisierten Beweisens mit künstlicher Intelligenz verschiebt. Durch den Einsatz spezialisierter Sprachmodelle für die Lean4-Umgebung erzeugt das System Beweise und zerlegt schwierige Sätze in einfachere, logisch zusammenhängende Propositionen.

Ein mehragentenbasiertes Orchestrierungsframework koordiniert dabei die Schritte Autoformalisation, Beweisgenerierung, Zerlegung und rekursive Beweisführung. Ohne Zerlegung erreichte das System bereits 90,4 % Erfolgsquote auf dem miniF2F‑Benchmark – mit der zusätzlichen Zerlegung steigt die Leistung deutlich an.

Ein wesentlicher technischer Fortschritt ist die Erweiterung des Kimina Lean Servers um AST‑Parsing-Funktionen, die eine automatisierte, rekursive Zerlegung von Theoremen ermöglichen und die Effizienz des gesamten Prozesses steigern.

Das Tool ist als Open‑Source‑Projekt unter dem Namen goedels-poetry auf PyPI verfügbar und steht auf GitHub zur Verfügung. Entwickler können die Architektur leicht an andere Sprachmodelle anpassen und zusätzliche Funktionen integrieren.