💻 computer science

Self-Supervised Theorem Discovery in a Formal Axiomatic System

Dieses Paper präsentiert einen selbstüberwachten Agenten, der autonom zehntausende bedeutsame Theoreme entdeckt und Benchmarks für Menschen löst, indem er ausschließlich von Axiomen und Inferenzregeln ausgeht, was demonstriert, dass nützliches mathematisches Wissen ohne menschliche Vorannahmen entstehen kann und das logische Denken von LLMs effektiv verbessern kann.

Ursprüngliche Autoren: Kazuki Ota, Takayuki Osa, Tatsuya Harada

Veröffentlicht 2026-06-30

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Kazuki Ota, Takayuki Osa, Tatsuya Harada

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 bringen einem Roboter das Rechnen bei, aber mit einer sehr strengen Regel: Sie dürfen dem Roboter keine Lehrbücher geben, keine Beispiele gelöster Aufgaben und keine „Spickzettel“ mit bekannten Fakten. Sie dürfen ihm nur das absolute Minimum geben: ein paar grundlegende Logikregeln (wie „Wenn A wahr ist und A impliziert B, dann ist B wahr“) und eine leere Tafel.

Die Frage, die dieses Paper stellt, lautet: Kann dieser Roboter sich selbst beibringen, neue, nützliche mathematische Fakten zu entdecken, indem er einfach nur mit diesen grundlegenden Regeln spielt?

Hier ist, wie die Forscher ihren Roboter aufgebaut haben und was sie erreicht haben, erklärt durch einfache Analogien.

1. Das Spiel: Ein Stapel Blöcke

Die Forscher haben für den Roboter ein Spiel mit einem System namens „Hilbert-Logik“ aufgebaut. Stellen Sie sich dieses System wie ein Spiel mit einem Stapel von Blöcken vor.

Die Regeln: Der Roboter hat drei Arten von speziellen Blöcken (Axiome), die er aufheben und auf den Stapel legen kann. Er hat auch eine Regel zum Kombinieren von Blöcken: Wenn er einen Block sieht, der sagt „Wenn X, dann Y“, und dieser auf einem Block steht, der „X“ sagt, kann er sie gegen einen Block austauschen, der „Y“ sagt.
Das Ziel: Dem Roboter wird ein Ziel-Block (ein Theorem) vorgegeben, und er muss die exakte Abfolge von Zügen finden, um diesen spezifischen Block oben auf den Stapel zu bauen.

2. Die Strategie: „Das probiere ich später mal“

Der Robbot beginnt mit dem Raten zufälliger Züge. Meistens scheitert er daran, das spezifische Ziel zu erreichen, das ihm gegeben wurde. Die Forscher gaben dem Roboter jedoch einen cleveren Trick namens Self-Supervised Learning (selbstüberwachtes Lernen).

Stellen Sie sich vor, der Roboter versucht, einen Turm zu bauen, um eine rote Flagge (das Ziel) zu erreichen. Er scheitert zwar, die rote Flagge zu erreichen, aber im Prozess baut er versehentlich eine sehr stabile blafe Plattform auf halber Höhe.

Der Trick: Anstatt diese blaue Plattform wegzuwerfen, sagt der Roboter: „Hey, ich habe gerade eine blaue Plattform gebaut! Lass uns das für das nächste Mal zu einem neuen Ziel machen.“
Die Schleife: Der Roboter speichert diese blaue Plattform als „Ziel“. Später versucht er, diese blaue Plattform erneut zu bauen. Jedes Mal, wenn er Erfolg hat, lernt er die exakten Schritte, um dies zu tun. Mit der Zeit baut der Roboter eine massive Bibliothek dieser „Plattformen“ (Theoremen), die er selbst entdeckt hat.

3. Die besten Werkzeuge auswählen

Der Roboter entdeckt tausende dieser Plattformen. Aber nicht alle von ihnen sind nützlich. Einige sind zu spezifisch (wie eine Plattform, die nur auf einen winzigen Stein passt), und einige sind einfach nur Wiederholungen von Dingen, die er bereits weiß.

Der Roboter nutzt zwei Filter, um die „Goldenen Werkzeuge“ auszuwählen:

Generalität: Er behält die Plattformen, die vielseitig sind (wie ein flacher Tisch), und wirft die weg, die zu seltsam oder zu spezifisch sind.
Schwierigkeit: Er sucht nach Plattformen, die schwer von Grund auf zu bauen sind. Wenn der Roboter Schwierigkeiten hat, eine bestimmte Plattform aus den Basismethoden zu bauen, ist diese Plattform ein „schwieriges Problem“. Der Roboter entscheidet, dieses schwierige Problem als vorgefertigtes Werkzeug (ein Lemma) zu seiner Werkzeugkiste hinzuzufügen.

4. Das Ergebnis: Eine wachsende Bibliothek

Nachdem der Roboter mehrere „Generationen“ (Runden des Lernens) durchlaufen hat, besitzt er eine Bibliothek von zehntausenden selbst entdeckten mathematischen Fakten.

Die Forscher testeten dies auf zwei Arten:

Kann der Roboter menschliche Probleme lösen? Sie gaben dem Roboter einen Satz von 30 klassischen Logikrätseln, die von Menschen geschrieben wurden (aus einem Lehrbuch). Der Roboter löste unter Verwendung seiner selbst erstellten Bibliothek 30 % dieser Rätsel erfolgreich. Das ist beeindruckend, da er diese Rätsel noch nie gesehen hatte und keine menschliche Hilfe erhielt.
Kann er anderen Robotern helfen? Die Forscher nahmen die „Goldenen Werkzeuge“, die der Roboter entdeckt hatte, und gaben sie einer anderen, sehr intelligenten KI (einem Large Language Model wie GPT) als „Hinweis“. Als diese andere KI die Möglichkeit hatte, diese selbst entdeckten Werkzeuge zu nutzen, wurde sie wesentlich besser darin, die Logikrätsel zu lösen.

Das große Ganze

Das Paper beweist, dass man einer KI nicht als Mensch eine Bibliothek mit mathematischen Fakten in die Hand drücken muss. Wenn man einer KI nur die grundlegenden Regeln des Spiels gibt, kann sie das Spiel spielen, ihre eigenen Abkürzungen entdecken und ihre eigene Bibliothek an nützlichem Wissen aufbauen.

Es ist wie ein Kind, das lernt, mit LEGOs zu bauen. Wenn man ihnen nur ein paar Basisteile und die Anweisung „Stecke sie zusammen“ gibt, werden sie vielleicht irgendwann selbst herausfinden, wie man ein komplexes Schloss baut, und dann feststellen: „Oh, diese spezielle Bogenform, die ich gebaut habe, ist wirklich nützlich, um Türen zu bauen“, und anfangen, diese Bogenform als Standardstück für alle ihre zukünftigen Schlösser zu verwenden.

Was das Paper NICHT behauptet:

Es behauptet nicht, dass der Roboter bereits fortgeschrittene Analysis oder Physik betreiben kann.
Es behauptet nicht, dass dies sofort für alle Arten von Mathematik funktioniert (sie haben es nur für die Aussagenlogik getestet).
Es behauptet nicht, dass dies menschliche Mathematiker ersetzt, sondern zeigt einen Weg auf, wie eine KI ihr eigenes formales Wissen entwickeln kann.

Kurz gesagt: Die KI hat sich selbst Mathematik von Grund auf beigebracht, ihr eigenes Wörterbuch nützlicher Fakten erstellt und bewiesen, dass diese Fakten tatsächlich helfen, reale Probleme zu lösen.

Technisches Resümee: Selbstüberwachtes Entdecken von Theoremen in einem formalen axiomatisches System

Problemstellung

Obwohl jüngste KI-Systeme, insbesondere Large Language Models (LLMs), signifikante Fortschritte im mathematischen Schließen demonstriert haben, verlassen sie sich weitgehend auf vom Menschen bereitgestellte Priors wie mathematische Texte, Code und bestehende Theorem-Bibliotheken. Eine kritische offene Frage bleibt: Kann ein Agent autonom nützliche Theoreme ausgehend rein aus den primitiven Regeln eines formalen axiomatischen Systems entdecken, ohne Zugriff auf menschliches Vorwissen, bestehende Theorem-Bibliotheken oder Trainingsdatensätze für Problemstellungen?

Aktuelle Methoden hängen oft von menschenkonstruiertem Wissen ab, um das Schließen (Reasoning) zu initialisieren. Selbst verbessernde Agenten in axiomatischen Domänen verlassen sich oft auf externe Richter, um die Nützlichkeit entdeckter Theoreme zu bewerten. Diese Arbeit untersucht, ob ein Agent nicht nur Theoreme entdecken, sondern auch „nützliche“ identifizieren und nutzen kann, um seine eigene Beweissuche und die Leistung externer Reasoning-Systeme zu verbessern, wobei er sich ausschließlich auf Axiome und Inferenzregeln stützt.

Methodik

1. Formale Umgebung: Hilbert-System als Stack-Maschine

Die Autoren instanziieren das Problem innerhalb eines Hilbert-Axiomensystems für die Aussagenlogik. Das System ist bewusst minimal gehalten und besteht aus:

Drei Axiomen:
- $Ax1: A \to (B \to A)$ (Schwächung)
- $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distribution)
- $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Kontraposition)
Eine Inferenzregel: Modus Ponens (MP), der $Y$ aus $X$ und $X \to Y$ ableitet.

Um das Lernen zu erleichtern, formulieren die Autoren das Theorembeweisen als einen deterministischen, zielgerichteten Stack-Maschinen-Entscheidungsprozess $(S, A, s_0, P)$ :

Zustand ( $S$ ): Ein endlicher Stack von Formeln.
Aktionen ( $A$ ): Auf den Stack drücken von Instanzen von $Ax1, Ax2, Ax3$ oder Anwendung von Modus Ponens (MP).
Mechanismus: Die MP-Aktion nutzt die Hindley–Milner-Unifikation. Wenn das oberste Stack-Element mit $X \to Y$ und das darunter liegende Element mit $X$ unifiziert, werden beide gepoppt und $Y$ wird auf den Stack gedrückt.
Erfolg: Ein Beweis ist erfolgreich, wenn der Stack eine einzige Formel enthält, die dem Ziel entspricht.

2. Selbstüberwachter Algorithmus zur Entdeckung von Theoremen

Der Kernbeitrag ist ein Algorithmus, der zwischen Beweissuche und der Extraktion nützlicher Theoreme alterniert und so eine Bibliothek von Theoremen aufbaut, die als Lemmata für die zukünftige Suche dienen.

A. Zielgerichtetes Policy-Lernen

Der Agent lernt eine Policy $\pi_\theta(A|S, g)$ , um die nächste Aktion unter Berücksitzung des aktuellen Stacks $S$ und eines Ziel-Formel $g$ vorherzusagen.

Hindsight Learning: Während einer Suchepisode wird jeder Zustand, in dem der Stack eine einzelne Formel $f_t$ enthält, als „erreichtes Theorem“ behandelt, unabhängig davon, ob dies das ursprüngliche Ziel war.
Trainingssignal: Das Aktionspräfix, das zu $f_t$ führt, wird als Beweis für $f_t$ behandelt. Diese Präfixe werden zu einem Trainingsdatensatz $D_{train}$ hinzugefügt, um die Policy mittels Cross-Entropy-Loss zu aktualisieren.
Ziel-Buffer ( $G$ ): Ein Buffer verwaltet die entdeckten Theoreme. Der Agent sampelt Ziele gleichmäßig aus $G$ für nachfolgende Suchepisoden, was effektiv sein eigenes Curriculum bootstrappt.

B. Extraktion nützlicher Theoreme

Um zu verhindern, dass die Bibliothek mit trivialen oder redundanten Theoremen überladen wird, filtert der Algorithmus entdeckte Theoreme basierend auf zwei Kriterien:

Generalität: Dieoreme werden gefiltert, um jene zu entfernen, die lediglich Spezialisierungen anderer Kandidaten sind. Das System behält nur die „minimalen“ Elemente unter einer partiellen Ordnung definiert durch Formelsubstitution (d. h. es behält die allgemeinsten Formen).
Reproduzierbarkeit: Das System schätzt die Wahrscheinlichkeit, mit der die aktuelle Policy ein Theorem erneut beweisen kann. Unter Verwendung eines Bayesianischen Posterior-Mittelwerts (Beta(1,1) Prior) priorisiert es Theoreme, die zwar entdeckt, aber schwer zuverlässig zu reproduzieren sind. Diese „schwer reproduzierbaren“ Theoreme sind wertvoll, da das Hinzufügen von ihnen als Lemmata schwierige Beweispfade komprimiert.

C. Mehrgenerationale Erweiterung der Bibliothek

Der Prozess operiert in Generationen:

Policy-Lernen: Training der Policy auf dem aktuellen Aktionsraum (anfänglich nur Axiome und MP).
Extraktion: Identifizierung nützlicher Theoreme aus dem Ziel-Buffer $G$ basierend auf Generalität und Reproduzierbarkeit.
Erweiterung des Aktionsraums: Hinzufügen der extrahierten Theoreme als neue Library-Aktionen (z. B. $Thm_1, Thm_2$ ). Wenn diese ausgewählt werden, drücken sie das entsprechende Theorem auf den Stack, was als vorverifiziertes Lemma fungiert.
Iteration: Wiederholung des Prozesses, wodurch der Agent lernt, die zuvor entdeckten Theoreme zu nutzen, um neue, komplexere Theoreme zu finden.

Wesentliche Beiträge

Formulierung: Das Beweisen von Aussagenlogik-Theoremen wird als Stack-Maschinen-Entscheidungsprozess formuliert, der direkt auf Hilbert-Axiomen und Inferenzregeln basiert und auf externe Theorem-Korpora verzichtet.
Algorithmus: Ein selbstüberwachter Algorithmus zur Entdeckung von Theoremen wird vorgeschlagen, der eine Theorem-Bibliothek allein aus primitiven Regeln aufbaut. Er nutzt extrahierte Theoreme als Lemmata für die nachfolgende Beweissuche wieder.
Autonome Entdeckung: Der Agent entdeckt zehntausende von Theoremen und findet Beweise für menschengeschriebene Benchmark-Probleme, ohne menschliche Priors für das Training zu verwenden.
Übertragbarkeit: Die extrahierten Theoreme dienen als effektives externes Wissen und verbessern die Beweisleistung externer LLMs, wenn sie als Prompt-Lemmata bereitgestellt werden.

Experimentelle Ergebnisse

1. Theorem-Entdeckung und Abdeckung

Wachstum: Die Anzahl der entdeckten Theoreme steigt über sechs Generationen hinweg an, was die Fähigkeit des Agenten demonstriert, seine Wissensbasis autonom zu erweitern.
Benchmark-Leistung: Der Agent findet erfolgreich Hilbert-System-Beweise für 30 % eines menschengeschriebenen Benchmark-Sets (abgeleitet aus Kleenes Lehrbuch).
Vergleich: Während GPT-5-high (die stärkste Baseline) ohne Unterstützung nur ca. 23 % Genauigkeit auf diesen Benchmarks erreicht, deutet die Fähigkeit des Agenten, Beweise für 30 % zu finden, darauf hin, dass er nicht-triviale Beweise entdeckt, die aus einer menschlichen mathematischen Perspektive sinnvoll sind.

2. Einfluss auf LLM-Reasoning

Prompt-Lemmata: Wenn die extrahierten Theoreme als Prompt-Lemmata an GPT-4o und GPT-5 Varianten übergeben werden, verbessert sich deren Erfolgsrate bei der Beweisführung der Benchmark-Probleme signifikant.
Qualitative Analyse:
- Einige entdeckte Theoreme entsprechen bekannten Prinzipien (z. B. dem Prinzip der Explosion, $\neg A \to (A \to B)$ ), die leicht interpretierbar sind.
- Andere (z. B. komplexes Implikations-Lifting) sind für Menschen nicht unmittelbar offensichtlich, fungieren aber effektiv als unterstützendes Wissen in LLM-Beweisen.
- Dies zeigt, dass der Agent in der Lage ist, nützliche Lemmata hervorzubringen, die Menschen nicht explizit bereitgestellt haben, und dass diese Lemmata über verschiedene Reasoning-Architekturen hinweg (vom Agenten zum LLM) übertragbar sind.

Bedeutung und Ansprüche

Das Paper behauptet, einen Beleg dafür zu liefern, dass nützliche Theoreme durch Beweissuche entdeckt werden können, ohne auf menschenbereitgestellte Theorem-Bibliotheken angewiesen zu sein.

Selbstentwickelnde KI: Die Arbeit deutet auf einen Pfad zu selbstentwickelnden KI-Systemen für die Mathematik hin, die ihr formales Wissen durch Beweissuche autonom erweitern können, während jede Entdeckung formal verifizierbar bleibt.
Formale Verifizierbarkeit: Im Gegensatz zu LLMs, die plausibel klingende, aber falsche Aussagen halluzinieren können, sind die Entdeckungen des Agenten strikt in den Axiomen und Inferenzregeln des Hilbert-Systems begründet.
Bescheidenheit: Die Autoren behaupten nicht, die State-of-the-Art-LLMs im allgemeinen Reasoning übertroffen zu haben. Stattdessen demonstrieren sie, dass ein Agent in einer beschränkten, formalen Umgebung lernen kann, sein eigenes Wissen zu entdecken und zu nutzen, um Probleme zu lösen, die selbst für fortgeschrittene LLMs schwierig sind, und dass dieses selbst entdeckte Wissen externe Systeme verstärken kann.

Die Studie ist auf ein einzelnes Axiomensystem (Hilbert-Aussagenlogik) beschränkt, aber die Autoren postulieren, dass das Framework auf reichere Systeme wie die Prädikatenlogik erster Stufe oder die Mengenlehre verallgemeinerbar ist, was einen Richtungsweiser für zukünftige Arbeiten darstellt.