Zur Entwicklung von Artificial Intelligence

[TomS]

Das ist definitiv eine Entwicklung der Fähigkeiten, die viele überrascht haben dürfte:

https://openai.com/de-DE/index/model-disproves-discrete-geometry-conjecture/

 

[antaris]

Ich finde das nun nicht gerade überraschend. Es ist ja nun nicht das erste Mal, dass ChatGPT ein Erdös-Problem gelöst hat. Wenn das bemerkenswerte ist, dass Methoden der algebraischen Zahlentheorie auf ein Problem der diskreten Geometrie übertragen wurden und so ein unerwartetes Ergebnis erhalten wurde, dann kann ich nur sagen, dass CNNA eine viel längere Kette von Disziplinen ableitet.

Beim Erdös Problem ist das mit einer klaren Aufgabe verbunden: konkretes offenes Einzelproblem -> Beweis oder Gegenbeispiel
Bei CNNA ist das zuerst nicht so gegeben, denn man hat einen großen Suchraum, der erstmal eingeschränkt werden muss. Daraus folgt dann der Rahmen (z.B. der DAG -> Importgraph) mit konkreter Konstruktion vieler Einzelprobleme, woraus man dann schrittweise/nacheinander versuchen kann -> Beweis oder Gegenbeispiel des jeweiligen Einzelproblems in steigender Abhängigkeit zu den Importen im DAG.

Man muss sich das mit der AI wie ein Art Brennglas vorstellen. Wenn ein großer Rahmen untersucht wird, dann kann der Fokus nicht auf einzelne Punkte gelegt werden und das Ergebnis bleibt eher allgemein. Hat man aber den Rahmen soweit fertig, dann können einzelne Aspekte fokussiert und speziell untersucht werden.
Der Beweis von OpenAI ist nun aber auch erst bemerkenswert, nachdem er intern und extern geprüft und bestätigt wurde. Bei letzteren wurde er dann sogar noch vereinfacht und verbessert.

 

[TomS]

Ich finde das nun nicht gerade überraschend.

Nun, die Mathematiker hat es teilweise überrascht.

 

[TomS]

auch interessant:

AI-led solutions of Erdős problems spark debate over the future of mathematics – Physics World

Problems that defeated human mathematicians for decades are now solved, but for whose benefit?

physicsworld.com

The fall of the theorem economy

How AI could destroy mathematics and barely touch it

davidbessis.substack.com

https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-remarks.pdf

The solution of the problem by the internal model of Open AI is, in my opinion, an outstanding
achievement, settling a long-standing open problem. The fact that the correct answer is not n1+o(1)
is surprising, and the construction and its analysis apply fairly sophisticated tools from algebraic
number theory in an elegant and clever way. As explained by the remarks of some of my colleagues
here there are several reasons that explain why AI tools can be better than humans in finding such
a construction. With or without a full agreement with these reasons, the fact is that the AI was
able to do here what lots of excellent human researchers tried and failed to do.

AI Broke an 80-Year-Old Math Conjecture, Then Humans Rewrote the Proof

An OpenAI model disproved the Erdős unit distance conjecture. But what nine mathematicians verified was not the raw output — it was 'edited reasoning.' Where does trust in AI-made knowledge come from?

blog.pebblous.ai

The quality of the result was no small thing. Fields Medalist Tim Gowers said he would recommend it for publication in Annals of Mathematics, the most prestigious journal in the field, without hesitation. Yet what nine outside mathematicians verified was not the model's raw output but a human-polished version, an "edited reasoning," and they had to rewrite that proof back into human language.

 

[antaris]

Nun, die Mathematiker hat es teilweise überrascht.

Was genau hat sie überrascht: dass eine jahrzehntelang für plausibel gehaltene Vermutung falsch war, oder dass eine AI die entscheidende Widerlegung gegen genau diese Vermutung gefunden hat?
Ersteres kann ich unmittelbar nachvollziehen. Wenn zudem zuvor niemand ernsthaft erwartet hatte, dass sich Methoden der algebraischen Zahlentheorie und der diskreten Geometrie bei diesem Problem gerade auf diese Weise komplementär ergänzen, dann ist natürlich auch der gefundene Lösungsweg mathematisch überraschend.

Dass eine hinreichend leistungsfähige AI solche disziplinübergreifenden Zusammenhänge finden kann, überrascht mich dagegen weniger. Genau das war schon vor Monaten meine Frage: Kann eine AI Beziehungen zwischen etablierten, aber disziplinär getrennt entwickelten mathematischen oder physikalischen Modellen erkennen, die Menschen übersehen haben — möglicherweise schlicht deshalb, weil niemand systematisch in dieser Richtung gesucht hat?

Das Ergebnis zeigt zumindest für ein konkretes, klar formuliertes Einzelproblem: Ja, offenbar kann sie das. Das Problem und das Erfolgskriterium waren vorgegeben, aber kein Lösungsweg. Die AI musste also nicht nur eine bekannte Methode ausführen, sondern selbst eine unerwartete Verbindung zwischen verschiedenen mathematischen Gebieten finden und daraus eine widerlegende Konstruktion entwickeln.

 

[TomS]

Was genau hat sie überrascht: dass eine jahrzehntelang für plausibel gehaltene Vermutung falsch war, oder dass eine AI die entscheidende Widerlegung gegen genau diese Vermutung gefunden hat?

Beides.

Dass eine hinreichend leistungsfähige AI solche disziplinübergreifenden Zusammenhänge finden kann, überrascht mich dagegen weniger. Genau das war schon vor Monaten meine Frage: Kann eine AI Beziehungen zwischen etablierten, aber disziplinär getrennt entwickelten mathematischen oder physikalischen Modellen erkennen, die Menschen übersehen haben — möglicherweise schlicht deshalb, weil niemand systematisch in dieser Richtung gesucht hat?

Im vorliegenden Fall ist es wohl weniger, dass man keinen Bezug zwischen den Fachgebieten vermutet hätte, als vielmehr, dass man an die Korrektheit der Vermutung geglaubt und deswegen in keiner Richtung nach einem Gegenbeispiel gesucht hat. Einige meinen, es wäre also eher Fleiß denn Genie gewesen, aber wir sollten evtl. davon ausgehen, dass da noch mehr kommt ...

Die AI musste also nicht nur eine bekannte Methode ausführen, sondern selbst eine unerwartete Verbindung zwischen verschiedenen mathematischen Gebieten finden und daraus eine widerlegende Konstruktion entwickeln.

Die KI muss nur genügend viele Wege durchprobieren. Sie probiert dabei häufiger wahrscheinliche Wege, d.h. wie du oben sagst, es gibt Zusammenhänge, die bisher unbeachtet geblieben sind, die die KI jedoch "sieht".

Die Frage ist eher, ob es möglich ist, die KI mittels sehr vieler Runs bestimmte Wege durchtesten zu lassen - egal ob letztlich erfolgreich oder nicht - und unabhängig davon die Gewichte derartiger Verbindungen bzw. Wege zu erkennen, also SELBST aus den Trainingsdaten zu ermitteln, nicht mittels KI.

Was zählt denn für den Mathematiker als Verbindung:

• eine explizit bewiesene Verbindung
• ein Hinweis bzw. eine Vermutung in der Literatur
• ...
• eine strukturelle Ähnlichkeit, die nirgendwo wirklich manifest ist sondern sich eher über viele Texte erstreckt

Beispiele:

• würde die KI bei der Pfadintegral-Quantisierung selbstständig den Nutzen der Grassmann-Variablen erkennen, wenn dies nicht bereits in sämtlichen Trainingsdaten vorhanden wäre?
• würde die KI die Taniyama–Shimura–Weil-Vermutung aufstellen (die Verwandtschaft der L-Funktionen sieht man, wenn man weiß, wo man hinschauen muss)
• würde die monstrous moonshine vermuten? (wenn man die Arbeiten nebeneinanderliegt, sieht man die Verwandtschaft der Zahlen)

Letztlich interessieren mich eher strukturelle Zusammenhänge, die man nicht so leicht sieht, also Fälle, in denen nicht einfach nur bisher übersehene jedoch recht offensichtliche Zusammenhänge entdeckt wurden (in den letzten Beispiel ist nicht die Entsprechung der Zahlen das spannende, sondern die Kühnheit der Vermutung, dass dies etwas bedeutet).)

 

[antaris]

Deine Unterscheidung trifft für mich den eigentlichen Punkt: Es ist etwas anderes, eine bereits explizit bekannte oder in der Literatur vermutete Verbindung wiederzufinden, als aus verstreuten strukturellen Ähnlichkeiten eine neue, tragfähige Beziehung zu vermuten.

Beim Erdös-Problem könnte tatsächlich entscheidend gewesen sein, dass man die Vermutung für richtig hielt und deshalb den Raum möglicher Gegenbeispiele nicht systematisch genug untersucht hat. Dann wäre die Stärke der AI zunächst vor allem Suchbreite, Ausdauer und die Fähigkeit, auch wenig wahrscheinliche Pfade konsequent weiterzuverfolgen.

Aber selbst "genügend viele Wege durchprobieren" setzt voraus, dass die AI mögliche Wege überhaupt erzeugen, bewerten, kombinieren und über viele Schritte konsistent halten kann. Der Suchraum liegt ja nicht als fertige endliche Liste vor.

Für mich ist deshalb die weitergehende Frage dieselbe wie deine: Erkennt die AI nur explizite oder latent nahegelegte Beziehungen aus den Trainingsdaten, oder kann sie eine strukturelle Verwandtschaft postulieren, die nirgends als solche formuliert wurde?

Genau hier ist CNNA für mich interessant. Die einzelnen mathematischen Bausteine sind natürlich überwiegend etabliert. Nicht etabliert ist aber die konkrete Kette, die im Suchprozess entstanden ist: von sequentieller Baumprovenienz über gerichtete Response- und Schur-/DtN-Strukturen bis zu schiefsymmetrischer Kopplung, komplexer Struktur und späteren operatoralgebraischen Fragen.

Dabei war nicht nur ein Lösungsweg offen. Zunächst war auch nicht bekannt, welche Teilprobleme, Disziplinen und Abhängigkeiten überhaupt relevant werden. Der Python-Suchpfad hat mögliche Verbindungen und Obstruktionen hervorgebracht und der jetzige DAG zerlegt diese erst nachträglich in überprüfbare Teil-/ bzw. Einzelprobleme.

Ob diese Verbindungen wirklich neu und mathematisch tragfähig sind, entscheidet sich natürlich nicht an ihrer Plausibilität, sondern an den formalen Beweisen, den dokumentierten Obstruktionen und später der unabhängigen Prüfung. Dabei ist jedoch auch zu berücksichtigen, dass selbst beim Erdös-Problem der ursprüngliche Suchraum nicht von der AI selbst erzeugt wurde, sondern bereits vor Jahrzehnten durch menschliche Fragestellung und mathematische Formulierung festgelegt war. Jede AI arbeitet somit immer innerhalb eines ihr vorgegebenen Rahmens aus Definitionen, Axiomen und Zielsetzungen. Die entscheidende offene Frage ist daher weniger, ob eine AI innerhalb eines solchen Rahmens neue Strukturen finden kann, sondern ob sie auch in der Lage ist, diesen Rahmen selbstständig zu erweitern oder neu zu definieren – oder ob dafür weiterhin menschliche Impulse, Intuitionen oder Leitideen notwendig bleiben. Die Einschätzung der Korrektheit des Erdös-Problem hat ja auch nicht die AI getroffen, sondern unabhängige Experten. Selbst wenn die AI oft richtig liegen sollte, ist es keine Garantie für 100%. Bei der Lösung eines Einzelproblems ist das auch alles überschaubar aber bei einer Verkettung von Beweise über viele Disziplinen hinweg ist die Möglichkeit eines frühen Fehlers, der immer weitergetragen/vererbt wird, nicht auszuschließen.

Die Trainingsdaten selbst sind m.E. auch nicht wirklich entscheidend, denn darauf kann die AI ja nicht mehr direkt zugreifen, zumal die Trainingsdaten auch veraltet sein können. Ohne Eingrenzung der Quellen und des Suchraums geht es m.E. (noch) nicht allein nur durch die AI.

 

[antaris]

Deine Unterscheidung trifft für mich den eigentlichen Punkt: Es ist etwas anderes, eine bereits explizit bekannte oder in der Literatur vermutete Verbindung wiederzufinden, als aus verstreuten strukturellen Ähnlichkeiten eine neue, tragfähige Beziehung zu vermuten.

Ein konkretes Beispiel aus CNNA ist die strukturelle Ähnlichkeit zwischen der von-Neumann-Konstruktion der natürlichen Zahlen und dem auf b=1 eingeschränkten Provenienzbaum. Bei b=1 existiert auf jeder Tiefe genau ein Knoten und diese bilden damit eine eindeutige Nachfolgerkette, deren Tiefe mit 0,1,2,... identifiziert werden kann. Das ist keine wörtliche Gleichsetzung des Baums mit den von-Neumann-Ordinalen, wohl aber eine klare strukturelle Entsprechung.

Die weitergehende, zunächst nicht vorgegebene Frage lautet dann: Was wird aus dieser Nachfolgerstruktur, wenn man nicht bei b=1 bleibt, sondern b>1 zulässt? Der lineare Nachfolgerpfad verzweigt sich zu endlichen Adressen. Dadurch entsteht die Möglichkeit, nicht mehr nur aufeinanderfolgende natürliche Zahlen, sondern feinere Zwischenstrukturen, Stellenentwicklungen, rationale Netze und über geeignete Grenz- oder Vervollständigungsverfahren möglicherweise reelle Strukturen zu untersuchen. Dafür wird nicht mal der asymmetrisch wachsende Baum benötigt, der ist nur zur Erweiterung zur schiefsymmetrischen Kopplungsstruktur notwendig.

Die einzelnen Bausteine – von-Neumann-Zahlen, b-äre Bäume, Stellenwertdarstellungen und metrische Vervollständigungen – sind selbstverständlich bekannt. Nicht bereits gegeben ist aber ihre konkrete Verkettung als Provenienzpfad:

Ob diese Kette tatsächlich kanonisch aus CNNA folgt, ist damit noch nicht bewiesen. Insbesondere müsste gezeigt werden, dass Stellengewichte, Ordnung, Rechenoperationen und Vervollständigung aus der internen Wachstums- und Response-Struktur hervorgehen und nicht nachträglich eingesetzt werden. Aber genau darin besteht der Unterschied zwischen einer bloßen Analogie und einer tragfähigen strukturellen Vermutung: Die Analogie erzeugt zunächst ein neues Forschungsprogramm, dessen einzelne Übergänge anschließend formal geprüft oder durch Obstruktionen verworfen werden. Dabei gilt der reguläre b-äre Baum eigentlich als wissenschaftlich voll erschlossen.

 

[TomS]

Für mich ist deshalb die weitergehende Frage dieselbe wie deine: Erkennt die AI nur explizite oder latent nahegelegte Beziehungen aus den Trainingsdaten, oder kann sie eine strukturelle Verwandtschaft postulieren, die nirgends als solche formuliert wurde?

Die Trainingsdaten selbst sind m.E. auch nicht wirklich entscheidend, denn darauf kann die AI ja nicht mehr direkt zugreifen, zumal die Trainingsdaten auch veraltet sein können. Ohne Eingrenzung der Quellen und des Suchraums geht es m.E. (noch) nicht allein nur durch die AI.

Alles, was die KI kann oder weiß, basiert letztlich auf Trainingsdaten.

Beispiel:

monstrous moonshine … is the unexpected connection between the monster group M and modular functions, in particular the j function. The initial numerical observation was made by John McKay in 1978 … In the mid-1970s, Jean-Pierre Serre, Andrew Ogg and John G. Thompson studied the quotient of the hyperbolic plane by subgroups of SL2(R), particularly, the normalizer Γ0(p)+ of the Hecke congruence subgroup Γ0(p) in SL(2,R). They found that the Riemann surface resulting from taking the quotient of the hyperbolic plane by Γ0(p)+ has genus zero exactly for p = 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 41, 47, 59 or 71. When Ogg attended a lecture by Jacques Tits in which the conjectural order of the monster group was presented, he noticed that these were precisely the prime factors of the group's size … In 1978, John McKay found that the first few terms in the Fourier expansion of the normalized J-invariant … could be expressed in terms of linear combinations of the dimensions of the irreducible representations of the monster group M with small non-negative coefficients. Specifically, McKay noticed that the coefficient 196884 was precisely one more than 196883, the degree of the smallest faithful complex representation of the monster group.

Damit könnte man nun einen Test machen: man eliminiert aus einem Satz ausgewählter Trainingsdaten alle Ergebnisse zu Moonshine nach 1978, und insbs. die offensichtlichen Hinweise wie die Zahlen. Damit – d.h. mit darüberhinaus üblichen Daten bis einschließlich 1978 – trainiert man LLMs. Wieviel muss man hinzufügen, bis das LLM zumindest die Vermutung aufstellt? Wievie, bis der Beweis gelingt?

 

[antaris]

Alles, was die KI kann oder weiß, basiert letztlich auf Trainingsdaten.

Das greift zu kurz.

antaris zu Claude: lass uns eine komplexe Struktur mittels b-ären Baum herleiten, claude zu antaris: du Idiot...setze i (wie alle anderen auch, denn das IST was in den Trainingsdaten gespeichert ist)

antaris zu ChatGPT: lass uns eine komplexe Struktur b-ären Baum herleiten, ChatGPT zu antaris: ok lass es uns versuchen, denn das nicht setzen von i (wie es alle anderen auch machen, denn das IST was in den Trainingsdaten gespeichert ist), könnte neue Erkenntnisse bringen.

Weder claude, noch ChatGPT hatten irgendeine wachsende Struktur auf einem b-ären Baum in den Trainingsdaten, die auf eine komplexe Struktur führt und dennoch konnten wir sie finden. Ich habe sehr intensiv nach solche Quellen gesucht aber exakt das nicht gefunden. wenn du sowas finden kannst, dann können wir darüber diskutieren, ob das in den Trainingsdaten enthalten war oder nicht. Daraus folgt, dass auf dieser gefundenen Struktur das "Moonshine-Problem" neu untersucht und dabei neue Erkenntnisse gefunden werden könnten, die über das etablierte Wissen und damit auch sämtlichen Trainingsdaten aller AI's hinausgehen.

Das nachträgliche Gedankenexperiment "was wäre, wenn wir so tun als wären die Trainingsdaten nicht da", hatten wir m.E. hier im Form schon mal als unsinnig verworfen. Wenn dann muss man jetzt tatsächlich neue Strukturen finden und mit der Literatur abgleichen. Wenn die Literatur keine Quellen liefert, dann kann sie schlecht als Träger für Trainigsdaten gedient haben.

Wieviel muss man hinzufügen, bis das LLM zumindest die Vermutung aufstellt? Wievie, bis der Beweis gelingt?

Es geht doch auch gar nicht darum, ob die AI wirklich alleine etwas finden kann. Die Anfrage was sie finden soll kommt immer vom Mensch und damit implizit auch der Suchraum in menschengemachter Literatur bzw. Trainingsdaten.
Der "Ausbruch" bei OpenAI und der darauf folgende Einbruch bei Huggingface von letztens hat sehr schön gezeigt, dass die AI eher spicken will, anstelle selber "derived-only" Antworten zu generieren. Selbst wenn also die Trainingsdaten nicht verfügbar sind, dann sucht die AI sich ggf. passende Informationen an zugänglichen Stellen.

 

[TomS]

Das greift zu kurz.

Nein.

Nochmal:

Alles, was die KI kann oder weiß, basiert letztlich auf Trainingsdaten. Auf was sonst?

 

[antaris]

Nein.

Nochmal:

Alles, was die KI kann oder weiß, basiert letztlich auf Trainingsdaten. Auf was sonst?

Nicht alles was es kann oder weiß. Ich glaube das ist zu sehr entweder/oder.

Die Trainingsdaten liefern keine fertige Liste aller späteren Antworten, die nur richtig kombiniert werden müssen. Bei der konkreten Aufgabe werden neue Hypothesen und Zwischenkonstruktionen erzeugt, gegeneinander geprüft und teilweise verworfen. Dass zusätzlicher Rechenaufwand während der Bearbeitung die Leistung von Reasoning-Modellen erhöht, spricht ebenfalls dagegen, ihre Funktion auf bloßen Abruf von Trainingspassagen zu reduzieren.

Das ist bei einem Menschen nicht wesentlich anders: Seine mathematische Fähigkeit basiert auf Ausbildung und Literatur. Trotzdem würde man einen neuen Beweis nicht dadurch erklären, dass er „letztlich auf Lehrbüchern basiert“. Die Lehrbücher erklären die Voraussetzungen seiner Fähigkeit, aber nicht die konkrete Entdeckung.

Hinzu kommt in unserem Fall eine externe formale Ebene. Mathlib ist eine Bibliothek formalisierten mathematischen Wissens in Lean. Falls Mathlib-Code zum Training gehörte, ist er dort natürlich Trainingsmaterial. Im aktuellen Arbeitsprozess ist Mathlib aber zugleich eine tatsächlich verwendete formale Bibliothek, und Lean prüft konkrete neue Beweisterme im Kernel. Das ist kein bloßes Erinnern aus Trainingsdaten, sondern eine laufende logische Verifikation.

Der nächste Formalisierungsschritt wird bei mir gerade nicht durch die Trainingsdaten, sondern durch die Rückkopplung lean/mathlib/python/Vergleich mit Primärliteratur ausgelöst. Ich will sogar größtmöglich den Zugriff auf Trainingsdaten verhindern. Darum gebe ich Literatur vor.
Also im Prinzip stimme ich dir zu aber rein methodisch und für meinen speziellen workflow halt nicht.
Bei dem Erdös-Gegenbeweis wurde aber wohl gerade nix vorgegeben und damit wohl wirklich rein auf Basis der Trainingsdaten das Ergebnis erzielt.

Zumal "das Hineinkippen von allem verfügbaren Wissen in ein einziges tiefes Loch" m.E. gar nichts bringt, weil dann eben auch sämtliche Ebenen miteinander vermischt werden, welche die AI erst mühsam auseinanderziehen muss und wo so oft schon nicht wirklich klar ist, wo genau die Ebenen überhaupt zu trennen sind.

 

[antaris]

Das beste Gegenbeispiel gegen eine reine Trainingsdaten-Erklärung ist für mich gerade die Suche nach der komplexen Struktur im CNNA-Modell.


ChatGPT, Claude und ich haben über viele Tage versucht, im statischen symmetrischen b-ären Baum eine Tür durch die Obstruktionswand zu finden. Die Kanten waren durch die Symmetrie nicht kanonisch unterscheidbar, eine Orientierung fehlte, und damit ließ sich auch keine komplexe Struktur ohne zusätzliche Wahl ableiten.
Wenn die konkrete Lösung als bekannte Struktur einfach in den Trainingsdaten vorgelegen hätte, stellt sich die naheliegende Frage: Warum hat weder ChatGPT noch Claude sie direkt vorgeschlagen?

Claude bestand vielmehr wiederholt darauf, i beziehungsweise eine komplexe Struktur einfach zu setzen und dann damit weiterzuarbeiten. Genau das entspricht auch der etablierten Literatur, welche als Trainingsdaten gefüttert wurden: Die komplexen Zahlen oder ein Operator J mit J^2=-I werden normalerweise vorausgesetzt. Dass ihre Provenienz selbst das Problem sein könnte, ist gerade nicht der übliche Ausgangspunkt und somit sehr wahrscheinlich nie in den Trainingsdaten enthalten gewesen.

Der entscheidende Schritt entstand erst durch die Obstruktionen und den Wechsel vom gesetzten symmetrischen Baum zum sequentiellen asymmetrischen Wachstum. Mit der ersten Geburt entstand eine ausgezeichnete longitudinale Rolle F_1; mit der ersten seitlichen Geschwistergeburt eine transversale Rolle F_2. Die Knoten selbst "wissen" davon nichts — diese Rollen entstehen global aus ihrer Geburtsprovenienz. Der gerichtete Response koppelt beide schiefsymmetrisch, und daraus ergibt sich erst der Pfad zur komplexen Struktur.

Natürlich waren einzelne mathematische Bausteine wie symmetrische und antisymmetrische Moden, Schur-Komplemente oder komplexe Strukturen vermutlich in den Trainingsdaten enthalten. Aber die konkrete CNNA-Kette

lag offenbar gerade nicht als fertige Lösung bereit.

Streng beweisen kann ich wegen der unbekannten Trainingskorpora nicht, dass nirgends etwas Ähnliches enthalten war. Ich könnte aber die Suche nach solchen Strukturen beweisen, da alle Chats noch verfügbar sind. Der teils hier im Forum dokumentierte Suchverlauf ist starke Evidenz dafür, dass die Lösung nicht abgerufen, sondern erst z.B. auch durch Mitwirkung der Teilnehmer hier im Forum durch aufstellen von Leitplanken, wiederholte Obstruktionen/Falsifikationen und die Neuformulierung des Problems konstruiert wurde.

Gerade der Umstand, dass die Modelle zunächst immer wieder zur konventionellen Setzung von i zurückkehrten, zeigt den Unterschied zwischen einem aus Trainingsdaten gelernten Standardpfad und einer innerhalb eines neuen Problemrahmens entstehenden Lösung besonders deutlich.

 

[TomS]

Nicht alles was es kann oder weiß.

Doch, alles. Worauf soll es sonst basieren?

Die Trainingsdaten liefern keine fertige Liste aller späteren Antworten, die nur richtig kombiniert werden müssen.

Das habe ich auch nicht behauptet.

Bei der konkreten Aufgabe werden neue Hypothesen und Zwischenkonstruktionen erzeugt, gegeneinander geprüft und teilweise verworfen. Dass zusätzlicher Rechenaufwand während der Bearbeitung die Leistung von Reasoning-Modellen erhöht, spricht ebenfalls dagegen, ihre Funktion auf bloßen Abruf von Trainingspassagen zu reduzieren.

Das habe ich ebenfalls nicht behauptet.

Hinzu kommt in unserem Fall eine externe formale Ebene. Mathlib ist eine Bibliothek formalisierten mathematischen Wissens in Lean. Falls Mathlib-Code zum Training gehörte, ist er dort natürlich Trainingsmaterial. Im aktuellen Arbeitsprozess ist Mathlib aber zugleich eine tatsächlich verwendete formale Bibliothek, und Lean prüft konkrete neue Beweisterme im Kernel. Das ist kein bloßes Erinnern aus Trainingsdaten, sondern eine laufende logische Verifikation.

Wie gesagt, das habe ich nicht behauptet.

Bei dem Erdös-Gegenbeweis wurde aber wohl gerade nix vorgegeben und damit wohl wirklich rein auf Basis der Trainingsdaten das Ergebnis erzielt.

Den Prompt kann man nachlesen.

Also bis auf die stochastische Komponente bei der Antwort ist ein LLM ein Algorithmus bzw. eine berechenbare Funktion f, die deterministisch von den Trainingsdaten t und dem Prompt x abhängt, und daraus einen Output Y erzeugt:

y = f(x, t)

Etwas allgemeiner betrachtet hängt es noch vom Parametern p und Zufallsvariablen r ab, also

y = f(x, t, p, r)

Aber daneben gibt es nichts. Dass r irgendeine zusätzliche Fähigkeit bedeuten würde, sehe ich nicht.

Stattest du das Modell noch mit Lean o.a. aus, entspricht das nur "Unterfunktionen" g, die anders als ein LLM funktionieren, aber letztlich landest du wieder bei

y = f(g, x, t, p, r)

Wenn das LLM also ein Theorem beweist, dann bedeutet das, dass y eine Zeichenfolge beinhaltet, die Mathematiker als Theorem interpretieren. In Wirklichkeit hat das LLM aber nichts anderes gemacht als z.B. beim Malen eines Comic.

 

[antaris]

Doch, alles. Worauf soll es sonst basieren?

Ich glaube, wir reden aneinander vorbei, weil wir "basiert auf" unterschiedlich verwenden.
Du meinst offenbar die kausale Herkunft der Modellfähigkeit: Ohne Training und die daraus entstandenen Parameter könnte das Modell weder Mathematik noch Sprache. In diesem Sinn stimme ich dir zu.

Mich interessiert dagegen die methodische Frage, wodurch ein konkretes neues Resultat im aktuellen Forschungsprozess entsteht und wodurch es geprüft wird. Dafür ist "basiert letztlich auf Trainingsdaten" zwar richtig, aber nicht hinreichend erklärend, da nur Trainingsdaten eben bei mir mehrfach gerade nicht zum Ziel geführt haben. Wir sehen das aus verschiedenen Perspektiven und meine ist ja nicht nur "füge lean und Python hinzu", sondern nutze diesen Rahmen, diese Inputs, verbiete dies, mache jenes oder nutze diese Primärquelle. Die Beweise, welche ein LLM beweist müssen nicht zwangsläufig richtig sein, auch wenn lean ohne sorry und Axiome baut. Insofern "versteht" das LLM natürlich nicht oder "denkt" auch nicht logisch.
Ich habe in CNNA auch nirgends vollkommen neue Mathematik etablieren müssen, welche die AI hätte irgendwie erst finden müssen. Ja, insofern basiert das alles auf Trainingsdaten, da eben die genutzten Methoden quasi alle aus den entsprechenden Lehrbüchern stammen und dennoch hat die AI (weder ChatGPT, noch Claude -> das Wachstum habe ich selber vorgeschlagen) nicht einfach auf dieser Basis die Kombination gefunden, welche die Obstruktion durchbrochen hat. Danach ist es eine iterative Mustererkennung über Testscripte gewesen, woraus der jetzige DAG abgeleitet wurde. Die echte Beweislast mit lean fängt jetzt eigentlich erst an.

Im Nachhinein ist es eh schwierig zu sagen, "was wäre, wenn..." und eigentlich ist es auch egal. Die fortschreitende Entwicklung der AI's wird die Landschaft so oder so weiter verändern.

 

[ralfkannenberg]

Wenn zudem zuvor niemand ernsthaft erwartet hatte, dass sich Methoden der algebraischen Zahlentheorie und der diskreten Geometrie bei diesem Problem gerade auf diese Weise komplementär ergänzen

Hallo Antaris,

wieso schreibst Du, dass sich die Methoden der algebraischen Zahlentheorie und der diskreten Geometrie "komplementär" ergänzen ?

Ja, sie ergänzen sich, aber wieso "komplementär" ?


Freundliche Grüsse, Ralf

 

[antaris]

wieso schreibst Du, dass sich die Methoden der algebraischen Zahlentheorie und der diskreten Geometrie „komplementär“ ergänzen?

Ja, sie ergänzen sich, aber wieso „komplementär“?

Hallo Ralf,

ich verwende "komplementär" hier nicht als technischen mathematischen Begriff, sondern im Sinn zweier verschiedener, jeweils unentbehrlicher Beiträge zur Provenienz des Gegenbeweises.
Die diskrete Geometrie formuliert das eigentliche Extremalproblem: Wie viele Punktpaare einer endlichen Punktmenge in der euklidischen Ebene können genau den Abstand 1 besitzen?
Die entscheidende Brücke zur algebraischen Zahlentheorie liegt darin, dass der euklidische Abstand selbst über eine algebraische Norm ausgedrückt werden kann. Für gaußsche ganze Zahlen gilt beispielsweise

Die geometrische Bedingung, dass zwei Punkte den Abstand 1 besitzen, wird damit zu einer algebraischen Bedingung an ihre Differenz:

Die algebraische Zahlentheorie liefert nun ungewöhnlich reiche Zahlkörper mit sehr vielen solchen Norm-eins-Differenzen. Über Einbettungs- und Auswahlargumente werden diese algebraischen Strukturen anschließend wieder in eine endliche Punktkonfiguration der euklidischen Ebene übersetzt.

Der Beweis besitzt daher vereinfacht die Schleife

Keine der beiden Disziplinen liefert den Gegenbeweis in dieser Form für sich allein: Die diskrete Geometrie gibt Problem, Zielgröße und geometrische Rückübersetzung vor; die algebraische Zahlentheorie erzeugt die bisher fehlende große Familie geeigneter Differenzen.
Mit komplementär meinte ich daher, dass beide methodischen Beiträge unterschiedliche Rollen erfüllen und der Gegenbeweis gerade aus ihrer geschlossenen Übersetzung ineinander entsteht, also gewissermaßen eine komplementäre Provenienz des Beweises aus zwei Disziplinen.

 

[TomS]

Ich glaube, wir reden aneinander vorbei, weil wir "basiert auf" unterschiedlich verwenden.
Du meinst offenbar die kausale Herkunft der Modellfähigkeit: Ohne Training und die daraus entstandenen Parameter könnte das Modell weder Mathematik noch Sprache. In diesem Sinn stimme ich dir zu.

Mich interessiert dagegen die methodische Frage, wodurch ein konkretes neues Resultat im aktuellen Forschungsprozess entsteht und wodurch es geprüft wird. Dafür ist "basiert letztlich auf Trainingsdaten" zwar richtig, aber nicht hinreichend erklärend, da nur Trainingsdaten eben bei mir mehrfach gerade nicht zum Ziel geführt haben.

Mich interessiert aber zunächst nicht, wie Forschung funktioniert – wobei man unter anderem LLMs als Werkzeug nutzt – sondern mich interessiert, wie ein LLM für sich betrachtet funktioniert (bekannt) und wozu es für sich betrachtet in der Lage ist bzw. wo seine Grenzen sind. Forscher diskutieren hier im Wesentlichen drei Methoden: Induktion, Deduktion und Abduktion.

• Induktion ist im wesentlichen Mustererkennung, das tun und können LLMs, so sind sie konstruiert.
• Deduktion ist logisches Beweisen, das können sie tatsächlich im Kern nicht, ihre Mustererkennung imitiert jedoch bei genügend guten Trainingsdaten Deduktion, d.h. ihre Ausgaben sehen so aus, als ob sie logisch schlussfolgern würden.
• Abduktion, also kreatives Erfinden neuer Methoden, die dann im Zuge der Deduktion verwendet werden, können sie nicht – so die heutige Lehrmeinung. Ein Beispiel wären algebraische Körpererweiterungen und Galois-Gruppen zur Kategorisierung der Lösbarkeit von Polynomgleichungen mittels Radikalen.

Im Nachhinein ist es eh schwierig zu sagen, "was wäre, wenn..." und eigentlich ist es auch egal.

Ganz im Gegenteil.

Wenn ich wissen möchte, wozu LLMs fähig sind, dann möchte ich insbs. ihre Grenzen kennen (das macht jeder Ingenieur und jeder Wissenschaftler bei der Untersuchung neuer Methoden). Dass es im Nachhinein schwierig sein soll, bedeutet ja nicht, dass es uninteressant ist.

Außerdem ist es nicht schwierig. Man trainiere ein LLM mit der Mathematik, die bis bis 30. Mai 1832 bekannt war, und fordere es auf, den Satz von Galois zu beweisen. Das ist schon alles.

 

[antaris]

Mich interessiert aber zunächst nicht, wie Forschung funktioniert – wobei man unter anderem LLMs als Werkzeug nutzt – sondern mich interessiert, wie ein LLM für sich betrachtet funktioniert (bekannt) und wozu es für sich betrachtet in der Lage ist bzw. wo seine Grenzen sind.

Ok, verstanden. Dann weiß ich nun genau worin unser "Aneinandervorbeireden" begründet war. Ich habe diese Grenzen ehrlich gesagt schon vor Monaten zwangsläufig ausgelotet und das nicht zuletzt gerade mit/wegen dem negativen Feedback hier im Forum. Meine eigenen Unzulänglichkeiten und die der AI zielen exakt auf die Dreiteilung, denn weder ich, noch die AI können alleine alle 3 vollständig und kohärent abdecken.
Deine Fragestellung habe ich also intern schon beantwortet und genau daraus ist die Frage zum Workflow eines kohärenten Forschungsweges entstanden und davon schreibe ich hier die ganze Zeit.
Für mich ist die Frage nach dem Workflow zentral, denn ohne institutionellen Hintergrund und ohne Zugriff auf Spezialisten der Disziplinen muss ich selbst einen selbstorganisierenden Workflow etablieren, den ein Wissenschaftler nicht in der Form braucht, da er andere Möglichkeiten hat.

Ich habe ChatGPT mal die Rollenverteilungen gegen deine Dreiteilung mappen lassen und da kannst du dann auch erkennen, wo die Grenzen der Dreiteilung auf Seite der AI's schon verschwimmen/verschmelzen bzw. verschieden sind. Wichtig ist, dass eine Aussage über ChatGPT nicht zwingend auch für Claude gilt. Die beiden AI's arbeiten unterschiedlich und sind auch "charakterlich" anders eingestellt. ChatGPT ist z.B. eher sehr explorativ und offen, Claude aber eher sehr konservativ und zurückhaltender eingestellt. Bei ChatGPT ist die Erinnerungsfunktion mittlerweile sehr gut, bei Claude eher sehr schlecht. Claude "vergisst" schnell den Kontext und das selbst innerhalb eines Chats.

Wichtig ist dabei auch festzuhalten, dass insbesondere ChatGPT das Arbeitstier ist, welches nach meinen Vorgaben sämtliche Python-Scripte und auch den lean-code schreibt. Den Weg der Ausführung innerhalb des durch Leitplanken begrenzten Rahmens überlasse ich vollkommen der AI. Inwiefern man diesen Prozess, innerhalb der gesetzten Wahlfreiheit, als (effektiv) kreativ bezeichnen kann, das sei dahingestellt. Wobei ich Python lokal nur ausführe, wenn schwere Läufe anstehen, die den Timeout der AI überschreiten. Die schnellen Python-Smoketests macht die AI vollständig selber, inkl. folgender Auswertung und das ist sehr schnell/effektiv. Bei lean ist es nach wie vor so, dass ich es lokal ausführe, da ChatGPT bisher nicht die native Möglichkeit bietet.

Rollenmapping: https://chatgpt.com/s/t_6a72e9913f348191ad4c99c134a222df

 

[TomS]

Wenn es da etwas verschmilzt oder verschmilzt, ldann wohl eher, weil das alles unglaublich ist.

Ich möchte davon weg und einen Punkt wirklich verstehen. Dass man mittels vieler Tools und der Adaption der Pipeline alles mögliche lösen kann, ist irgendwie klar.