DeepMinds KI löst Aufgaben der Internationalen Mathematik-Olympiade auf Silbermedaillen-Niveau

(deepmind.google)

3 Punkte von GN⁺ 2024-07-26 | 3 Kommentare | Auf WhatsApp teilen

Beim IMO 2024, einem der wichtigsten Prüfsteine für anspruchsvolles mathematisches Schließen, lösten AlphaProof und AlphaGeometry 2 von Google DeepMind 4 von 6 Aufgaben und erreichten damit als erste KI eine Leistung im Bereich einer Silbermedaille
Sie erzielten 28 Punkte von insgesamt 42; alle gelösten Aufgaben wurden mit voller Punktzahl bewertet, nur 1 Punkt unter der Goldmedaillen-Grenze von 29 Punkten im Jahr 2024
Die Bewertung erfolgte nach den IMO-Bewertungsregeln durch Mathematiker; AlphaProof übernahm Algebra und Zahlentheorie, AlphaGeometry 2 die Geometrie, wodurch unterschiedliche Schlussfolgerungsmethoden kombiniert wurden
Die Aufgaben wurden zunächst manuell in eine formale mathematische Sprache übersetzt; während Schüler im Wettbewerb zwei Sitzungen zu je 4,5 Stunden haben, brauchte das System für eine Aufgabe einige Minuten und für andere bis zu 3 Tage
Das Ergebnis zeigt, dass Mathematik-KI über bloßes Rechnen hinaus zur Suche und Verifikation von Beweisen vorgedrungen ist; formalisierte Eingaben und lange Lösungszeiten bleiben jedoch weiterhin wichtige Einschränkungen

Silbermedaillen-Leistung beim IMO 2024

Google DeepMind stellte das mathematische Schlussfolgerungssystem AlphaProof und AlphaGeometry 2, eine verbesserte Version seines Systems zum Lösen von Geometrieaufgaben, vor
Die beiden Systeme lösten 4 der 6 Aufgaben der International Mathematical Olympiad 2024
- AlphaProof: löste 2 Algebra-Aufgaben und 1 Zahlentheorie-Aufgabe
- AlphaGeometry 2: bewies 1 Geometrieaufgabe
- 2 Kombinatorik-Aufgaben wurden nicht gelöst
Jede Aufgabe ist maximal 7 Punkte wert, die Gesamtpunktzahl beträgt 42
- Das System erhielt für alle 4 gelösten Aufgaben die volle Punktzahl und erzielte 28 Punkte
- Das entspricht dem oberen Bereich der Silbermedaille beim IMO 2024
- Die Goldmedaillen-Grenze 2024 lag bei 29 Punkten; im offiziellen Wettbewerb erreichten 58 von 609 Teilnehmenden den Goldmedaillen-Bereich
Dies ist der erste Fall, in dem ein KI-System bei der IMO eine Leistung auf Silbermedaillisten-Niveau erzielte

Bewertungsmethode und Lösungsbedingungen

Verwendet wurden die vom IMO-Veranstalter bereitgestellten Wettbewerbsaufgaben
Die Antworten wurden nach den Bewertungsregeln der IMO beurteilt
- Die Gutachter waren Prof Sir Timothy Gowers, IMO-Goldmedaillist und Fields-Medal-Träger, sowie Dr Joseph Myers, zweifacher IMO-Goldmedaillist und Vorsitzender des IMO 2024 Problem Selection Committee
Damit das System die Aufgaben verstehen konnte, wurden alle Aufgaben zunächst manuell in eine formale mathematische Sprache übersetzt
Im offiziellen Wettbewerb reichen Schüler ihre Antworten in zwei Sitzungen zu je 4,5 Stunden ein
- Das KI-System löste eine Aufgabe innerhalb weniger Minuten, für andere Aufgaben brauchte es bis zu 3 Tage
Unter den von AlphaProof gelösten Aufgaben befand sich auch die schwierigste Aufgabe der IMO 2024, die nur 5 Teilnehmende lösen konnten

AlphaProof: formales Schließen auf Basis von Lean

AlphaProof ist ein System, das lernt, mathematische Aussagen in der formalen Sprache Lean zu beweisen
Es kombiniert ein vortrainiertes Sprachmodell mit dem Reinforcement-Learning-Algorithmus AlphaZero
- AlphaZero ist der Algorithmus, der verwendet wurde, um sich Schach, Shogi und Go selbst beizubringen
Durch die Verwendung einer formalen Sprache lässt sich die Korrektheit von Beweisen mit mathematischem Schließen überprüfen
Bisher gab es nur sehr wenige von Menschen erstellte formale Beweisdaten, weshalb die Nutzung formaler Sprachen im Machine Learning eingeschränkt war
Ansätze auf Basis natürlicher Sprache können auf deutlich mehr Daten zugreifen, können aber plausibel wirkende, dennoch falsche Zwischenschritte oder Lösungen erzeugen
DeepMind feinjustierte das Gemini-Modell, um Aufgaben in natürlicher Sprache automatisch in formale Aussagen zu übersetzen, und erstellte eine Bibliothek formaler Aufgaben mit unterschiedlichen Schwierigkeitsgraden
Wenn AlphaProof eine Aufgabe erhält, erzeugt es Lösungskandidaten und durchsucht anschließend in Lean mögliche Beweisschritte, um sie zu beweisen oder zu widerlegen
- Gefundene und verifizierte Beweise werden verwendet, um das Sprachmodell von AlphaProof zu verstärken
- Dieser iterative Prozess dient dazu, die Fähigkeit zum Lösen schwierigerer Aufgaben zu verbessern
In der Vorbereitung auf die IMO trainierte es über mehrere Wochen, indem es Millionen von Aufgaben bewies oder widerlegte
- Auch während des Wettbewerbs wurde eine Lernschleife eingesetzt, die Beweise für selbst erzeugte Varianten der Aufgaben verstärkte, während das System nach einer vollständigen Lösung suchte

AlphaGeometry 2: Erweiterung auf schwierigere Geometrieaufgaben

AlphaGeometry 2 ist eine stark verbesserte Version des bisherigen AlphaGeometry
Das System hat eine neuro-symbolische Hybridstruktur, die neuronale Netze und symbolisches Schließen kombiniert
- Das Sprachmodell basiert auf Gemini
- Es wurde von Grund auf mit einer Größenordnung mehr synthetischen Daten trainiert als die Vorgängerversion
Dank mehr Daten und eines verbesserten Modells kann es schwierigere Geometrieaufgaben bearbeiten, die Bewegungen von Objekten sowie Gleichungen zu Winkeln, Verhältnissen und Abständen enthalten
Die symbolische Engine von AlphaGeometry 2 ist um einen zweistelligen Faktor schneller als die Vorgängerversion
Bei einer neuen Aufgabe nutzt es einen neuen Mechanismus zum Wissensaustausch, um fortgeschrittene Kombinationen verschiedener Suchbäume einzusetzen und komplexere Aufgaben zu bewältigen
Lösungsrate für IMO-Geometrieaufgaben der letzten 25 Jahre: {b:83,53}
- Nach dem Stand vor dem Wettbewerb 2024 konnte AlphaGeometry 2 83 % der IMO-Geometrieaufgaben der letzten 25 Jahre lösen
- Die Lösungsrate des vorherigen AlphaGeometry lag bei 53 %
Beim IMO 2024 löste es Problem 4 nach formalisierter Eingabe innerhalb von 19 Sekunden

Schlussfolgern in natürlicher Sprache und künftige Nutzung

Im Rahmen der IMO-Arbeit experimentierte DeepMind auch mit einem System für Schlussfolgern in natürlicher Sprache, das auf Gemini und aktueller Forschung basiert
Dieses System muss Aufgaben nicht in eine formale Sprache übersetzen und kann mit anderen KI-Systemen kombiniert werden
Auch an den IMO-Aufgaben 2024 wurde dieser Ansatz getestet; die Ergebnisse wurden als vielversprechend bewertet
Die technischere Methodik von AlphaProof wurde als Nature-Paper veröffentlicht
DeepMind strebt eine Zukunft an, in der Mathematiker gemeinsam mit KI-Tools Hypothesen erkunden, neue Ansätze für alte Probleme ausprobieren und zeitaufwendige Teile von Beweisen schneller abschließen

3 Kommentare

chabulhwi 2024-07-26

Je mehr Mathematiker zur Entwicklung formaler Mathematikbibliotheken beitragen, desto leichter wird es sein, leistungsfähige Mathematik-KI zu entwickeln. Soweit ich weiß, gibt es derzeit in Korea drei Personen, die mathematische Theorien, die sie selbst in der Sprache des Beweisassistenten Lean formalisiert haben, in Leans Mathematikbibliothek Mathlib übertragen.

Ich habe mich im vergangenen Jahr ein wenig an der Portierung von Mathlib von Lean 3 auf Lean 4 beteiligt und in diesem Jahr einen bislang unbewiesenen Satz in der Lean-4-Batteries-Bibliothek bewiesen.

GN⁺ 2024-07-26

Meinungen auf Hacker News

Ich bin wirklich sehr gespannt auf diese Ankündigung, aber es ist unklar, wie viel Arbeit in dem Satz steckt, dass „zunächst ein Mensch die Aufgaben in eine formale mathematische Sprache übersetzt hat, damit das System sie verstehen kann“
Alle nicht-geometrischen Aufgaben hatten die Form „Finde alle X, für die ... gilt“, und die Theoremsätze hatten die Form „Zeige, dass die Menge aller X {foo} ist“
Allein anhand der herunterladbaren Lösungen unter https://storage.googleapis.com/deepmind-media/DeepMind.com/B... lässt sich schwer erkennen, ob {foo} in der Übersetzungsphase von einem Menschen festgelegt oder vom Computer gefunden wurde. Ich würde gern glauben, dass der Computer es gefunden hat, aber ich finde keinen Beleg dafür
- Der Computer hat die Antworten selbst gefunden. Konkret fand er in P1 die geraden ganzen Zahlen, in P2 {1,1} und in P6 2, und lieferte jeweils auch einen Lean-Beweis dazu
- Allgemein gesagt ist diese Übersetzungsphase deutlich einfacher als die Beweisphase. Das Problem bei automatischer Übersetzung ist, dass das Übersetzungsergebnis falsch sein kann
  Auch Menschen passiert das häufig, wenn sie direkt mit formalen Methoden arbeiten; daher dürften die Forschenden zu dem Schluss gekommen sein, dass letztlich jede Übersetzung geprüft werden muss, ob mit LLMs oder anderen Tools
- Auf der verlinkten Seite steht: „Die Aufgabenstellung wurde von Menschen in Lean formalisiert, aber die Antwort innerhalb der Aufgabenstellung wurde vom Agenten erzeugt und formalisiert“
  Unklar bleibt allerdings, welche Anfangsform dem Agenten gegeben wurde, damit dieser Schritt möglich war
- Interessant ist, dass es ein Formalisierungswerkzeug gab, das zur Erstellung der Trainingsdaten verwendet wurde, hier aber nicht zum Einsatz kam. Vielleicht war es noch nicht zuverlässig genug
- Es klingt nach der Beschreibung: „Wenn eine Aufgabe gegeben ist, erzeugt AlphaProof Lösungskandidaten und durchsucht dann in Lean mögliche Beweisschritte, um sie zu beweisen oder zu widerlegen“
  Das heißt: Welche Form von „Aufgabe“ AlphaProof auch erhält und wie auch immer „Finde alle X, für die ... gilt“ formalisiert wurde, vermutlich erzeugt es Kandidatentheoreme in Lean. Zum Beispiel könnte es die Aussage sein, dass eine Menge für eine bestimmte Formel P die Form {n: P(n)} hat. Danach sucht es nach einem Beweis
  Wenn AlphaProof {foo} nicht selbst gefunden hat, sondern es vorgegeben war, wäre die Behauptung, es habe die Aufgabe gelöst, ziemlich absurd. Trotzdem bin ich von diesem Ergebnis sehr angetan
Das ist definitiv beeindruckend, aber wenn die IMO erwähnt wird, braucht es eine Einschränkung. Medaillen werden an 50 % der Teilnehmenden vergeben, also an Schülerinnen und Schüler, und das Verhältnis von Gold, Silber und Bronze beträgt 1:2:3; damit gehören Gold- und Silbermedaillengewinner zu den besten 25 % aller Teilnehmenden
Man könnte also sagen: „Die KI hat IMO-Aufgaben besser gelöst als 75 % der Schülerinnen und Schüler“ – und eigentlich ist schon das vielleicht noch beeindruckender
Aber die Bedingungen „eine Aufgabe in wenigen Minuten, jede der übrigen Aufgaben in bis zu 3 Tagen“ unterscheiden sich von den 9 Stunden, die die Schülerinnen und Schüler bekommen, daher ist es kein echter Vergleich. Wenn die Schülerinnen und Schüler statt 9 Stunden bis zu 15 Tage bekommen hätten, hätten wohl mehr von ihnen diese Punktzahl erreicht oder übertroffen
Tatsächlich hat die KI innerhalb der 9 Stunden, die den Schülerinnen und Schülern zur Verfügung standen, im Grunde nur eine Aufgabe gelöst und wäre damit vermutlich weit von einem Medaillenrang entfernt gewesen. Ich frage mich, ob man ein so beeindruckendes Ergebnis wirklich durch einen Äpfel-mit-Birnen-Vergleich verwässern muss
Objektiver wäre es, zu berichten, dass sie zwar länger gebraucht hat, aber X % aller Aufgaben gelöst oder X von N Punkten erreicht hat
- Ich habe schon IMO-Teilnehmende getroffen, und sie sind wirklich absurd intelligent. Bevor ich mit so einer Gruppe in Kontakt kam, hätte ich mir nicht vorstellen können, dass Menschen so klug sein können. Man sollte sie also eher als die besten 25 % der obersten 0,01 % aller Schülerinnen und Schüler betrachten
  Zeit ist hier keine besonders interessante Achse. Menschen verwenden schließlich keine CPU, die einem riesigen GPU-Cluster entspricht. Interessanter ist die binäre Frage: „Kann man mit genügend Ressourcen zu einer Lösung gelangen?“ Bei GPT/Claude war die Antwort eindeutig nein
- Die Aussage „50 % der teilnehmenden Schülerinnen und Schüler erhalten eine Medaille“ kann missverständlich sein: Mit diesen Schülerinnen und Schülern ist keine Stichprobe normaler Gymnasiastinnen und Gymnasiasten gemeint. Soweit ich weiß, besteht das Team jedes Landes aus etwa sechs der stärksten Wettbewerbsaufgaben-Löser des Landes
- Persönlich, und das ist nicht die Position von Google, glaube ich, dass der einzige Grund, warum es dieses Jahr keine Goldmedaille gab, Pech bei der Aufgabenauswahl war und dass man bei P3/P5 nicht auf Teilpunkte gezielt hat
  Sie waren sehr nah am Cutoff, und normalerweise bekommt man schon für kleine Fortschritte 1 Punkt. Aus technischen Gründen wäre eine Berichterstattung, die behauptet, sie hätten eine Goldmedaille gewonnen, wohl nicht gut gewesen; daher scheint man sich mit einer unumstrittenen Silbermedaille zufriedengegeben zu haben
- Der entscheidende Unterschied zwischen mehr Zeit für Menschen und mehr Zeit für ein Computerprogramm ist, dass wir historisch viel erfolgreicher darin waren, Letzteres schneller auszuführen
- Der Großteil der DeepMind-Forschung ist aus Unternehmenssicht ein Cost Center. Solche Pressemitteilungen helfen, gegenüber Investoren und Öffentlichkeit weitere Investitionen zu rechtfertigen
Das ist wirklich der Fall. AlphaGeometry löste mit viel Brute-Force-Suche eine sehr begrenzte Menge von Problemen.
Die neue Methode ist viel breiter angelegt, und ich denke, sie wird großen Einfluss darauf haben, wie Mathematik betrieben wird. Sie führt von Mathematik in natürlicher Sprache zu formalisierter Mathematik und implementiert dort tatsächlich eine selbstversorgende Pipeline, in der sowohl Formalisierung als auch Beweise trainiert werden können.
Im Prinzip kann diese Pipeline auch grundlegenden Theorieaufbau lernen, etwa das Erzeugen von Hilfsdefinitionen und Lemmata. Das kommt dem Heiligen Gral der Beweisassistenz nahe, und ich glaube, es wird uns ermöglichen, den Großteil der Mathematik, die wir auf natürliche Weise entwickeln, zu formalisieren. Menschen werden nachträglich präzisieren, und Maschinen werden dabei helfen, die Details auszufüllen.
- Stimme zu. Das ist ein großer Fortschritt. Geometrieprobleme gehören in eine andere Kategorie, weil man sie in Systeme polynomialer Gleichungen übersetzen und dann mit bekannten Computeralgebra-Algorithmen lösen kann.
  Diese Art offener Formalisierung war dagegen ein Bereich, in dem der Fortschritt sehr langsam und schrittweise verlief. Ich habe vor fünf Jahren in einem angrenzenden Gebiet gearbeitet, und dieses Ergebnis kann man als etwas ansehen, das mit traditionellen Verfahren des automatischen Schließens unerreichbar gewesen wäre.
  Echte automatische Theorembeweise sind weit über die reine Mathematik hinaus nützlich. Man könnte zum Beispiel die axiomatische Semantik einer kleinen Programmiersprache in Lean niederschreiben und Fragen stellen wie: „Zeige, dass ein Programm existiert, das diese Spezifikation erfüllt.“
  Wenn dieser Ansatz skaliert, wird er wichtiger sein als jede Machine-Learning-Anwendung der letzten Jahre.
- Man sollte Suche nicht geringschätzen. Sie kann wie Brute Force wirken, aber Suche hat beim Go menschliches Niveau übertroffen und ist bis auf IMO-Silbermedaillen-Niveau gekommen.
  Auch die Evolution, die uns hervorgebracht hat, ist eine Suche, die mit enorm vielen Brute-Force-Versuchen funktioniert hat, und Forschung nach der wissenschaftlichen Methode ist im Kern ebenfalls Suche.
- Es gibt bereits Leute, die in diesem Bereich arbeiten.
  https://leandojo.org/
  https://machine-learning-for-theorem-proving.github.io/
  https://www.youtube.com/watch?v=P5ew0BrRm_I
  https://paperswithcode.com/task/automated-theorem-proving
  https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
  https://github.com/RiccardoBiosas/LeanGPT
- Solche Systeme dürften außerhalb der mathematischen Forschung noch viel nützlicher sein.
  Um nützliche Dinge zu tun, muss man keine extrem schwierigen Probleme beweisen. Oft reicht es, einfache Dinge zu beweisen. Wenn man ein Sprachmodell Aufgaben erledigen, Einträge organisieren, Termine koordinieren oder Code schreiben lässt, der X tut, kann man dem Ergebnis nicht ohne Weiteres vertrauen. Wenn das System aber einen Teil des Problems in Logik übersetzen und eine Lösung finden kann, wird es deutlich vertrauenswürdiger.
- Nein. Es ist nur so ähnlich, als hätte man ihnen erlaubt, eine Suchmaschine zu verwenden, um eine Lösung zu finden; mehr nicht.
Der Kernpunkt geht etwas unter: Sie verwenden Lean.
Das ist über mathematische Probleme hinaus wichtig. Machine-Learning-Modelle mit einem Beweissystem ringen zu lassen, ist eine gute Methode, allgemeines Geschwätz zu vermeiden.
Ich hoffe, dass künftig mehr Menschen Typen in Lean oder ähnlichen Systemen schreiben und das als eine viel bessere Art nutzen, Prompts zu formulieren.
- AlphaProof ist eindeutig beeindruckend, aber bei der IMO bekommt der Computer auch Vorteile, die Menschen nicht haben. Niemand wird im Kopf eine Gröbner-Basis konstruieren, aber polyrith braucht nur acht Zeichen. Ich habe auch gesehen, dass AlphaProof nlinarith verwendet.
- Erstaunlich. Ich wollte gerade kommentieren, dass es der Hammer wäre, wenn man das direkt an Lean anschließt. Höhere Mathematik sollte künftig wohl in diese Richtung gehen. Die wichtigsten Beweise sind so komplex geworden, dass fast niemand mehr alle Teile vollständig versteht.
  1. https://lean-lang.org/
- Damit werden sie wohl auch die Riemannsche Vermutung angehen, hehe.
Es gibt eine gute kurze Übersicht von Tim Gowers, die die wichtigsten Vorbehalte erklärt und das Ganze einordnet. Er ist Fields-Medaillist und war auch an dieser Arbeit beteiligt: https://x.com/wtgowers/status/1816509803407040909
Das stimmt, aber schon in die Nationalmannschaft eines Landes zu kommen, ist ein extrem harter Prozess. Bei regionalen Mathematik-Olympiaden, nationalen Mathematik-Olympiaden und so weiter wird in jeder Stufe brutal ausgesiebt.
Danach folgt zusätzliches Training für diese Elitegruppe, und je nach Fall kann es auch weitere Auswahlrunden geben.
Kurz gesagt: In das IMO-Team eines Landes berufen zu werden, ist an sich schon eine große Sache, und darin eine Gold- oder Silbermedaille zu gewinnen, ist einfach eine enorme Leistung.
- Manche Länder nehmen diese Kinder das ganze Jahr über aus der Schule, damit sie sich auf das IMO-Training konzentrieren, und garantieren ihnen außerdem die Zulassung zu den besten Universitäten des Landes.
  Quelle: ein Freund, der eine IMO-Silbermedaille gewonnen hat.
Ich beneide die Leute wirklich, die dafür bezahlt werden, an so etwas zu arbeiten. Das sieht unglaublich spannend aus, und es muss sehr befriedigend sein, auf diese Weise den Stand der Technik voranzutreiben.
- Das muss nicht unbedingt so sein. Es gab schon viele Dinge, die eigentlich sehr erfüllend hätten sein sollen, die dann furchtbar langweilig oder sogar schädlich wurden – und umgekehrt gab es äußerlich ganz gewöhnliche Aufgaben, die wirklich interessant waren.
  Bei der Arbeitszufriedenheit ist meiner Ansicht nach die Arbeitsumgebung wichtiger als das Thema. Selbst wenn man an einem weltverändernden Thema arbeitet, hat man eine harte Zeit, wenn das Team schlecht ist. Manche Menschen haben ein Talent dafür, allem den Spaß zu entziehen, und Büropolitik gibt es überall – besonders bei Themen, die die Welt verändern sollen.
  Umgekehrt kann man selbst bei einem Thema, das so langweilig wirkt wie Kundendaten in eine Datenbank zu schreiben, eine großartige Zeit haben, wenn das Team freundlich ist, die Architektur gut entworfen wurde und es Zeit für Experimente und Wissensaustausch gibt. Ich schätze die Schönheit einfacher Dinge, die einfach gut funktionieren, immer mehr. So etwas kann sogar seltener sein als ein wissenschaftlicher Durchbruch.
  Natürlich können eine großartige Arbeitsumgebung und ein großartiges Thema auch zusammenkommen, und das ist fast wie ein Jackpot und durchaus beneidenswert.
- Ich arbeite in diesem Bereich, konkret an LLM-Pretraining. Es ist nicht so glamourös, wie es von außen aussieht. Dazu gehört, riesige YAML-Dateien zu bearbeiten und Regex in großem Maßstab einzusetzen. Natürlich ist das etwas vereinfacht gesagt.
  Man sollte begeistert und dankbar sein, so etwas machen zu können, aber die groben Werkzeuge nehmen einem viel von der Freude an der Arbeit.
- Wahrscheinlich sollte es nicht „jealous“, sondern „envious“ heißen.
- Das Beste, was wir tun können, ist, weiter auf dem Laufenden zu bleiben und es zu unterstützen.
- Ist jetzt nicht die Zeit, die 3.292.329 Zeilen lange YML für K8s wieder neu zu konfigurieren?
  (/s)
Maschinen spielen seit Jahrzehnten besser Schach als Menschen.
Trotzdem interessiert das niemanden. Alle sind damit beschäftigt, Magnus Carlsen zuzusehen.
Weil wir Menschen sind, interessieren wir uns dafür, was andere Menschen tun. Für Maschinen interessieren wir uns nur, soweit sie uns nützlich sind.
Dieses Prinzip lässt sich breit auf Arbeit und Kunst ausweiten. Solange es Menschen gibt, wird es in solchen Bereichen immer einen Platz für Menschen geben.
- Egal wie viel besser KI in Schach und Kunst wird, Menschen werden weiter Freude daran haben. Genauso wird es vermutlich weiterhin Menschen geben, die Mathematik als Hobby betreiben.
  Ich bezweifle aber stark, dass es in naher Zukunft noch Mathematiker geben wird, die neue mathematische Fortschritte veröffentlichen, die nicht größtenteils oder vollständig von KI entdeckt wurden. Menschen könnten die Anerkennung für einen Beweis bekommen, weil sie die ursprüngliche Frage gestellt haben, aber es gibt kaum eine Welt, in der man darauf besteht, dass Menschen sinnvolle mathematische Probleme langsamer und teurer lösen, wenn Computer das leicht können.
- Stimmt, aber wenn eine KI zum Beispiel die Goldbachsche Vermutung beweist, wäre das eine gewaltige Sache.
- Aus Sicht der Verbraucher macht es keinen Unterschied, ob eine Fleischverarbeitungsfabrik oder ein Amazon-Logistikzentrum 5000 Menschen beschäftigt oder 5.
  Auf Kunst trifft dieses Prinzip sicher zu, auf Arbeit aber nur teilweise oder in den meisten Fällen.
- Es gibt Menschen, die glauben, dass Mathematik im Gegensatz zu Schach oder Kunst tatsächlich nützlich ist. Die meisten Mathematiker werden das wohl nicht so sehen, aber wenn wir diesen verrückten Gedanken kurz akzeptieren, dann ist ein Beweis lediglich ein Werkzeug, das sagt: „Dieses Stück Mathematik wurde korrekt angewendet.“
  Dann muss man den Beweis nicht verstehen, und niemanden interessiert, ob irgendein Mathematiker irgendwo ihn vollständig versteht. Dass Maschinen besser darin sind als wir, Beweise zu finden und zu überprüfen, ist in Ordnung und sogar erwartbar.
- Ich glaube nicht, dass sich dieses Prinzip gut auf mathematische Beweise übertragen lässt. Einen Beweis zu verifizieren ist sehr, sehr viel einfacher, als ihn zu erstellen, und ein zweiter Beweis wird nur noch zu einer Fußnote.
  Viele Mathematiker werden sich damit nicht beschäftigen wollen. Allerdings liegt zwischen der IMO und der vordersten Front der Forschungsmathematik noch eine große Distanz.
Ich habe immer gedacht, dass Theorem Proving ein Einpersonenspiel mit einem absurd großen Suchraum ist und daher lange vor AGI gelöst werden würde.
Meiner Meinung nach sind die größten Beitragenden zu AlphaProof die Leute hinter Lean und Mathlib, weil sie die gewaltige Aufgabe übernommen haben, die gesamte Mathematik zu formalisieren.
Der Mangel an Formalisierung in mathematischen Arbeiten hat Automatisierungsversuche immer wieder scheitern lassen, weil KI-Forscher mit menschlichen Faktoren wie autorenspezifischer Notation, implizitem Wissen und ausgelassenen Beweisschritten kämpfen mussten.
- Die Aussage „Theorem Proving ist ein Einpersonenspiel mit einem enorm großen Suchraum und wird daher lange vor AGI gelöst werden“ klingt seltsam.
  Ich denke, dass der Begriff AGI selbst nicht definiert ist, aber ich weiß nicht, warum man erwarten sollte, dass es viel schwieriger ist, „etwas allgemein Intelligentes“, also Intelligenz auf dem Niveau des Medianmenschen, zu schaffen, als „besser in Mathematik zu sein als Terence Tao“.
- Sie haben nicht die gesamte Mathematik formalisiert. Zum Glück braucht man für die IMO nicht die gesamte Mathematik. Aber sie haben nicht einmal genug für die IMO formalisiert. Vermutlich konnten sie deshalb das Kombinatorikproblem nicht lösen.
Die beste Diskussion gibt es hier: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...