🤖 machine learning

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

Diese Arbeit zeigt, dass das Auswahlaxiom eine messbare geometrische Signatur in neuronalen Beweis-Embeddings hinterlässt – charakterisiert durch sinkende Anomalie-Scores und Rekonstruktionsverluste, wenn sich Beweise im Abhängigkeitsgraphen vom Axiom entfernen –, was mit der Leistungsdisparität zwischen konstruktivem und klassischem Theorembeweisen in Systemen wie Lean 4 korreliert und diese vorhersagt.

Ursprüngliche Autoren: Rodrigo Mendoza-Smith

Veröffentlicht 2026-06-30✓ Author reviewed ⓘ

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Rodrigo Mendoza-Smith

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. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich eine riesige, antike Bibliothek vor, genannt Mathlib. Diese Bibliothek enthält fast eine halbe Million mathematischer Beweise, die alle in einer strengen, computerlesbaren Sprache namens Lean geschrieben sind. Seit über einem Jahrhundert streiten Mathematiker über zwei verschiedene Wege, diese Beweise zu erstellen:

Konstruktive Beweise: Die „Lego“-Methode. Wenn Sie behaupten, dass ein Gebäude existiert, müssen Sie genau zeigen, wie man es baut, Stein für Stein.
Klassische Beweise: Die „Magie“-Methode. Sie können behaupten, dass ein Gebäude existiert, indem Sie einfach sagen: „Es ist unmöglich, dass es nicht existiert“, ohne zu zeigen, wie man es baut. Dies beruht auf einer Regel namens Auswahlaxiom (Axiom of Choice).

Lange Zeit dachten die Leute, dies seien nur philosophische Unterschiede. Dieses Paper argumentiert, dass es sich tatsächlich um geometrische Unterschiede handelt, die man messen kann, wie die Entfernung zwischen zwei Städten auf einer Landkarte.

So haben die Autoren dies entdeckt, unter Verwendung einfacher Analogien:

1. Das „Echo“ der Magie-Regel

Die Autoren behandelten die Bibliothek wie einen riesigen Echoraum. Sie trainierten ein künstliches Gehirn (eine KI) nur auf den „Lego“- (konstruktiven) Beweisen. Die KI lernte den Rhythmus, den Stil und die Struktur dieser Beweise. Sie wurde zur Expertin darin, zu erkennen, was ein „normaler“ konstruktiver Beweis ist.

Dann fütterten sie die KI mit den „Magie“- (klassischen) Beweisen.

Das Ergebnis: Die KI sagte nicht nur: „Das ist anders.“ Sie maß, wie anders es war.
Die Analogie: Stellen Sie sich vor, Sie sind ein Musiklehrer, der nur klassisches Klavier hört. Wenn Sie ein Jazzstück hören, sagen Sie vielleicht: „Das klingt seltsam.“ Aber wenn Sie ein Jazzstück hören, das vor 100 Jahren geschrieben wurde, klingt es vielleicht weniger seltsam als ein modernes Jazzstück, das ein sehr spezifisches, ungewöhnliches Instrument verwendet.

2. Das „Tiefe“-Gesetz

Die Autoren erkannten, dass nicht alle „Magie“-Beweise gleichermaßen magisch sind.

Geringe Tiefe (Entfernung 1-2): Diese Beweise nutzen die „Magie-Regel“ (Auswahlaxiom) direkt. Sie sind wie ein Jazzsong, der dieses seltsame Instrument gleich zu Beginn verwendet. Für die KI klingen sie sehr seltsam und „fehl am Platz“.
Große Tiefe (Entfernung 9+): Diese Beweise nutzen die „Magie-Regel“ schon viel früher, tief vergraben in einer Kette anderer Lemmata. Der Beweis selbst sieht sehr nach einem „Lego“-Beweis aus. Für die KI klingen sie fast normal.

Die Entdeckung: Es gibt einen glatten Gradienten. Je weiter man sich von der direkten Nutzung der „Magie-Regel“ entfernt, desto mehr beginnt der Beweis wie ein standardmäßiger „Lego“-Beweis auszusehen und zu klingen. Die „Seltsamkeit“ verblasst. Die Autoren nennen dies das Depth Law (Tiefengesetz).

3. Drei Wege, die „Seltsamkeit“ zu messen

Die Autoren verwendeten drei verschiedene „Lineale“, um diese Distanz zu messen, und alle stimmten überein:

Der Anomalie-Score: Wie weit ist dieser Beweis vom nächsten „Lego“-Beweis entfernt? (Wie die Messung, wie weit eine Jazz-Note von einer Klaviernote entfernt ist).
Der Rekonstruktionsverlust (Reconstruction Loss): Wenn die KI versucht, den nächsten Schritt in einem „Magie“-Beweis zu erraten, macht sie dann häufiger Fehler als bei einem „Lego“-Beweis? (Wie ein Lehrer, der das nächste Wort in einem Satz errät; er hat mehr Schwierigkeiten mit den „Magie“-Sätzen).
Der Dichtencheck: Lebt dieser Beweis in der belebten „Lego“-Nachbarschaft oder ist er in der leeren „Magie“-Wildnis verloren?

Alle drei Lineale zeigten dasselbe Muster: Die „Magie“-Beweise sind sehr markant, wenn sie nah an der Quelle liegen, aber sie verschmelzen mit der Umgebung, wenn man sich weiter entfernt.

4. Der „Roboter-Solver“-Test

Der praktischste Teil des Papers betrifft einen Roboter namens Aesop, der versucht, diese mathematischen Probleme automatisch zu lösen.

Das Problem: Der Roboter ist gut darin, „Lego“-Beweise zu lösen (20 % Erfolgsquote), aber schlecht bei „Magie“-Beweisen (nur 1,5 %). Es ist, als könnte ein Roboter zwar mit Blöcken bauen, aber durch Zaubersprüche verwirrt werden.
Der Clou: Die Autoren versuchten, dem Roboter zu helfen, indem sie ihm einen „neuronalen Führer“ (einen smarten Assistenten, der den ersten Schritt vorschlägt) gaben.
Das Ergebnis: Der Führer half ein wenig, aber er löste das Problem nicht. Der Roboter hatte immer noch massiv Schwierigkeiten mit den „Magie“-Beweisen, selbst wenn diese „tief“ waren und wie „Lego“-Beweise aussah.

Die wichtigste Erkenntnis: Selbst wenn die „Magie“-Beweise immer mehr wie „Lego“-Beweise aussehen, je weiter man sich von der Quelle entfernt, desto mehr Schwierigkeiten bereiten sie dem Roboter-Solver. Dies deutet darauf hin, dass die „Magie-Regel“ eine permanente, unsichtbare Narbe im Beweis hinterlässt, die es heutigen Computern schwer macht, ihn zu lösen, ungeachtet dessen, wie „normal“ der Beweis oberflächlich betrachtet wirkt.

Zusammenfassung

Das Paper beweist, dass das Auswahlaxiom nicht nur eine philosophische Idee ist; es hinterlässt einen messbaren, geometrischen Fingerabdruck auf mathematischen Beweisen.

Direkte Nutzung der Regel lässt Beweise für die KI sehr „fremdartig“ erscheinen.
Indirekte Nutzung lässt sie „normaler“ erscheinen.
Dennoch, selbst wenn sie „normal“ aussehen, haben automatisierte Solver immer noch signifikant mehr Schwierigkeiten mit ihnen als mit rein konstruktiven Beweisen.

Es ist, als würde man feststellen, dass ein Haus, das mit „magischen Ziegeln“ gebaut wurde, von außen zwar exakt wie ein Haus aus „normalen Ziegeln“ aussehen mag, aber wenn man versucht, es mit einem Standard-Werkzeug zu reparieren, verursachen die magischen Ziegel dennoch Probleme.

Technisches Resümee: Geometrische Messungen des Auswahlaxioms in neuronalen Beweis-Embeddings

Problemstellung

Das Auswahlaxiom (Axiom of Choice, AC) hat die mathematischen Grundlagen historisch gesehen in klassische und konstruktive Lager gespalten – eine Unterscheidung, die weitgehend philosophischer und methodischer Natur bleibt. Während klassische Beweise nicht-konstruktive Abkürzungen nutzen, die durch das AC zulässig sind, erfordern konstruktive Beweise explizite Zeugen. Es war jedoch unklar, ob diese beiden Paradigmen strukturelle Unterschiede aufweisen, die über die bloße Axiomabhängigkeit hinaus detektierbar sind. Diese Arbeit untersucht, ob das Auswahlaxiom eine messbare „geometrische Signatur“ innerhalb des Raums formaler Beweise hinterlässt, spezifisch innerhalb der Lean 4 Mathlib-Bibliothek, und ob diese Signatur operationale Konsequenzen für neuronale Theorembeweiser hat.

Methodik

Datenpartitionierung und Abhängigkeitsverfolgung

Die Autoren nutzen die kernbasierte Verfolgung der Axiomabhängigkeit von Lean 4, um die Mathlib-Bibliothek zu partitionieren, die 471.260 maschinell zertifizierte Deklarationen enthält. Durch eine Breitensuche im Abhängigkeitsgraphen klassifizieren sie die Deklarationen in zwei Mengen:

Klassische Beweise: Solche, die transitiv von Classical.choice abhängen.
Konstruktive Beweise: Solche, die dies nicht tun.

Der „Abstand“ eines klassischen Beweises wird als die Länge der kürzesten Abhängigkeitskette von diesem Beweis zu Classical.choice definiert. Dies erzeugt einen stratifizierten Datensatz, in dem Beweise nach ihrer Tiefe von dem Axiom gruppiert sind. Die Studie konzentriert sich auf eine gefilterte Population von 42.355 Theoremen (31.144 klassisch, 11.211 konstruktiv) mit Taktik-Traces zwischen 2 und 200 Schritten.

Label-freies Repräsentationslernen

Um die geometrischen Eigenschaften dieser Beweise ohne Bias zu messen, trainieren die Autoren einen selbstüberwachten Denoising-Autoencoder ausschließlich auf konstruktiven Beweisen.

Input: Beweise werden als Sequenzen von Taktik-Heads (z. B. intro, rw, simp) dargestellt, wobei spezifische Argumente verworfen werden, um den Fokus auf die Beweiskomposition zu legen.
Architektur: Ein 4-schichtiger Transformer-Encoder gepaart mit einem 2-schichtigen Decoder. Das Modell wird darauf trainiert, maskierte Taktik-Token (20 % Korruption) aus der Eingangssequenz zu rekonstruieren.
Embedding: Das Beweis-Embedding ist der Mittelwert der verborgenen Zustände des Encoders (ohne Padding), normiert auf die Einheitssphäre.
Label-freie Beschränkung: Der Encoder sieht während des Trainings weder klassische Beweise noch deren Vokabular oder Hyperparameter-Einstellungen. Klassische Beweise dienen strikt als gehaltene Population zur Messung.

Geometrische Messungen

Drei komplementäre Metriken werden verwendet, um die Divergenz klassischer Beweise von der konstruktiven Trainingsverteilung als Funktion ihrer Abhängigkeitstiefe zu messen:

Anomalie-Score (k-NN): Der euklidische Abstand zu den $k$ -nächsten konstruktiven Nachbarn.
Rekonstruktionsverlust: Der Cross-Entropy-Verlust, der entsteht, wenn das auf konstruktiven Beweisen trainierte Modell versucht, maskierte Token in einem klassischen Beweis vorherzusagen.
Dichte-Superlevel-Containment: Der Anteil der klassischen Beweise, die außerhalb des hochdichten Bereichs (Superlevel Set) der konstruktiven Trainingsverteilung liegen.

Operationale Evaluierung

Die Studie evaluiert den Einfluss dieser geometrischen Befunde auf die Theorembeweis-Leistung unter Verwendung zweier Systeme:

aesop: Ein symbolischer Best-First-Search-Beweiser.
Hybrid (ReProver + aesop): Ein neural gesteuerter Ansatz, bei dem ein neuraler Taktik-Generator den ersten Schritt vorschlägt, gefolgt von aesop.

Zentrale Ergebnisse

Das Tiefengesetz (The Depth Law)

Der primäre Befund ist die Existenz eines „Tiefengesetzes“: Die geometrische Unterscheidung zwischen klassischen und konstruktiven Beweisen nimmt vorhersagbar mit der Entfernung von Classical.choice ab.

Scharfe Trennung bei geringen Tiefen: Bei Tiefe 2 (Beweise, die direkt klassische Lemmata aufrufen), ist die Trennung stark. Der k-NN-Anomalie-Score erreicht einen AUC von 0,847, der Rekonstruktionsverlust ist 34,5 % höher als der konstruktive Baseline-Wert, und 43 % der klassischen Beweise liegen außerhalb der konstruktiven 90-%-Dichteregion.
Abbau zur Ununterscheidbarkeit: Mit zunehmender Tiefe konvergieren die Metriken gegen die konstruktive Baseline. Bei Tiefe 9+ nähern sich alle drei Metriken den Zufallswerten an (AUC $\approx$ 0,5, Verlust $\approx$ Baseline, Containment $\approx$ 90 %), wodurch tiefe klassische Beweise geometrisch von konstruktiven ununterscheidbar werden.
Ein-Parameter-Mischungsgesetz: Die Autoren modellieren diesen Gradienten als Mischung aus zwei Verteilungen: einer konstruktiven Verteilung $P$ und einer direkt-klassischen Verteilung $R$ . Die Verteilung der Tiefe $d$ , $Q_d$ , wird als $Q_d = (1 - \lambda_d)P + \lambda_d R$ modelliert, wobei $\lambda_d$ ein Mischgewicht ist, das mit der Tiefe abnimmt. Die drei distinkten Messungen kollabieren auf eine einzige Kurve, wenn sie normalisiert werden, was ein solches Ein-Parameter-Gesetz stützt.

Robustheitskontrollen

Das Signatursignal ist robust gegenüber mehreren potenziellen Störfaktoren (Confounds):

Keywords: Das Entfernen expliziter klassischer Taktik-Marker (z. B. classical, by contra) reduziert den Tiefe-2-AUC nur geringfügig (von 0,847 auf 0,754), was darauf hindeutet, dass das Signal strukturell und nicht bloß lexikalisch ist.
Länge: Die Residualisierung der Embeddings bezüglich der Beweislänge eliminiert den Gradienten nicht.
Autor/Datei/Thema: Mixed-Effects-Modelle, die Autor, Datei und mathematisches Subgebiet kontrollieren, bestätigen, dass das Signal innerhalb spezifischer Kontexte bestehen bleibt.
Aussage vs. Beweis: Theorem-Aussagen zeigen einen wesentlich schwächeren Tiefengradienten (aggregierter AUC 0,604) im Vergleich zu Beweisen (aggregierter AUC 0,675), was bestätigt, dass das Signal primär kompositionell (Beweisstruktur) und nicht topikal (Theoreminhalt) ist.
Axiom-Spezifität: Während auch propext und Quot.sound Tiefengradienten aufweisen, erzeugt Classical.choice den steilsten Gradienten, was auf eine einzigartige operationale Kopplung mit klassischer Argumentation hindeutet.

Operationale Konsequenzen

Die geometrische Signatur korreliert mit der Leistung der Beweiser:

aesop Fehlgeschlagen: aesop löst 20,0 % der konstruktiven Theoreme, aber nur 1,5 % der klassischen (ein 13-facher Unterschied). Im Gegensatz zum geometrischen Signal glättet sich dieser operationale Abstand nicht mit der Tiefe; klassische Beweise bleiben für aesop unabhängig von ihrer Entfernung zum Axiom schwierig.
Neurale Steuerung: Das Hinzufügen eines neuralen Taktik-Generators (ReProver) komprimiert die Lücke auf etwa das Fünffache (22,0 % vs. 4,5 %), schließt sie jedoch nicht.
Prädiktive Kraft: Der geometrische Anomalie-Score sagt das Scheitern von aesop signifikant besser voraus als die reine Beweislänge allein (der AUC steigt von 0,766 auf 0,841, wenn man den Anomalie-Score hinzufügt).

Bedeutung und Behauptungen

Das Paper behauptet, den ersten empirischen Beleg dafür zu liefern, dass das Auswahlaxiom eine messbare geometrische Korrelation im Beweisraum besitzt. Die Autoren argumentieren:

Strukturelle Unterscheidung: Die klassisch-konstruktive Spaltung ist nicht nur eine philosophische Haltung, sondern eine strukturelle Eigenschaft der Beweiskomposition, die in neuronalen Embeddings sichtbar ist.
Operationale Relevanz: Diese geometrische Signatur ist keine abstrakte Kuriosität; sie sagt die Leistung automatisierter Theorembeweiser voraus. Das „Tiefengesetz“ legt nahe, dass Beweise mit zunehmender Tiefe strukturell ähnlicher zu konstruktiven Beweisen werden, die operationale Barriere für symbolische Beweiser wie aesop jedoch spezifisch für das Vorhandensein von Classical.choice bleibt.
Methodischer Beitrag: Die Arbeit zeigt, dass label-freies, selbstüberwachtes Lernen auf einer einzelnen Klasse (konstruktive Beweise) die strukturellen Grenzen einer gehaltenen Klasse (klassische Beweise) aufzeigen kann, die durch logische Abhängigkeit definiert ist, und bietet somit ein neues Werkzeug für die metamathematische Analyse an.

Die Autoren bleiben hinsichtlich kausaler Mechanismen zurückhaltend und merken an, dass zwar die geometrische Signatur und die operationale Lücke stark assoziiert sind, die spezifische Ursache der Schwierigkeit für den Beweiser (strukturelle Barriere vs. Regelwerk-Konfiguration) jedoch weiterer Untersuchung bedarf. Die Arbeit ist als Einladung an die Community formuliert, ähnliche strukturelle Achsen in formalen Bibliotheken zu identifizieren.