Belegung

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Neuer Weisheitsbericht

Herausgeber: Redaktion

[Einführung in die neue Weisheit] Gerade hat das neueste mathematische Modell von Google DeepMind die Silbermedaille der IMO Mathematical Olympiad gewonnen! Es löste nicht nur 4 der 6 Fragen mit perfekter Punktzahl, nur 1 Punkt von der Goldmedaille entfernt, sondern es dauerte auch nur 19 Sekunden, um die vierte Frage zu lösen. Die Qualität und Geschwindigkeit der Lösung des Problems verblüffte die menschlichen Richter, die punkteten .

AI hat die Silbermedaille der IMO Mathematical Olympiad gewonnen!

Google DeepMind gab gerade bekannt, dass die eigentlichen Fragen der diesjährigen Internationalen Mathematikolympiade von seinem eigenen KI-System erstellt wurden.

Darunter hat AI nicht nur 4 der 6 Fragen erfolgreich beantwortet, sondern auch für jede Frage die volle Punktzahl erhalten, was der höchsten Punktzahl einer Silbermedaille entspricht – 28 Punkte.

Dieses Ergebnis ist nur noch 1 Punkt von der Goldmedaille entfernt!

Von den 609 Teilnehmern gewannen nur 58 Goldmedaillen

Im offiziellen Wettbewerb geben menschliche Teilnehmer ihre Antworten in zwei Sitzungen mit einem Zeitlimit von jeweils 4,5 Stunden ab.

Interessanterweise brauchte die KI nur wenige Minuten, um eine der Fragen zu beantworten, aber die restlichen Fragen dauerten drei volle Tage, was als ernsthafte Auszeit bezeichnet werden kann.

Was dieses Mal einen großen Beitrag leistete, waren zwei KI-Systeme – AlphaProof und AlphaGeometry 2.

Wichtiger Punkt: 2024 ist meiner Meinung nach nicht in den Trainingsdaten dieser beiden KIs enthalten.

Scott Wu, einer der Gründer des KI-Ingenieurs Devin (ein dreimaliger IOI-Goldmedaillengewinner), beklagte: „Als ich ein Kind war, hatte ich nie gedacht, dass sie zehn Jahre später durch KI ersetzt werden würden . gelöst".

Im diesjährigen IMO-Wettbewerb gibt es sechs Wettbewerbsfragen zu den Themen Algebra, Kombinatorik, Geometrie und Zahlentheorie. Sechs Wege ergeben vier, lassen Sie uns das Niveau der KI spüren –

Die Fähigkeit der KI zum mathematischen Denken schockiert den Professor

Wir alle wissen, dass die bisherige KI aufgrund eingeschränkter Denkfähigkeiten und Trainingsdaten nur begrenzte Möglichkeiten zur Lösung mathematischer Probleme hatte.

Die beiden KI-Spieler, die heute gemeinsam auftraten, haben diese Einschränkung durchbrochen. sie sind jeweils--

- AlphaProof, ein neues System für formales mathematisches Denken, das auf verstärkendem Lernen basiert

- AlphaGeometry 2, das geometrische Problemlösungssystem der zweiten Generation

Die von den beiden KIs gegebenen Antworten wurden nach den Regeln der berühmten Mathematiker Professor Timothy Gowers (IMO-Goldmedaillengewinner und Fields-Medaillengewinner) und Dr. Joseph Myers (zweimaliger IMO-Goldmedaillengewinner und Vorsitzender des IMO 2024 Question Selection Committee) bewertet. .

Am Ende hat AlphaProof zwei algebraische Fragen und eine zahlentheoretische Frage richtig gelöst. Eine der schwierigsten Fragen wurde in der diesjährigen IMO von nur fünf menschlichen Teilnehmern gelöst;

Es gibt nur zwei Probleme der kombinatorischen Mathematik, die nicht gelöst wurden.

Auch Professor Timothy Gowers war während des Bewertungsprozesses zutiefst schockiert –

Dass ein Programm eine solch nicht offensichtliche Lösung finden konnte, ist wirklich beeindruckend und übertrifft bei weitem das, was ich angesichts des aktuellen Stands der Technik erwartet hätte.

AlphaProof

AlphaProof ist ein System, das mathematische Aussagen in der formalen Sprache Lean beweisen kann.

Es kombiniert ein vorab trainiertes großes Sprachmodell mit dem Verstärkungslernalgorithmus AlphaZero, der sich selbst beigebracht hat, Schach, Shogi und Go zu beherrschen.

Ein wesentlicher Vorteil formaler Sprachen besteht darin, dass sie für Beweise, die mathematisches Denken beinhalten, formal verifiziert werden können. Ihre Anwendung beim maschinellen Lernen war jedoch aufgrund der sehr begrenzten Menge relevanter, von Menschen geschriebener Daten begrenzt.

Im Gegensatz dazu können auf natürlicher Sprache basierende Ansätze trotz des Zugriffs auf große Datenmengen plausible, aber falsche Zwischenschritte und Lösungen hervorbringen.

Um dies zu überwinden, haben Google DeepMind-Forscher das Gemini-Modell so optimiert, dass Problemaussagen in natürlicher Sprache automatisch in formale Aussagen übersetzt werden. Dadurch wurde eine große Bibliothek mit formalen Problemen unterschiedlicher Schwierigkeit aufgebaut und so eine Brücke zwischen den beiden komplementären Bereichen geschlagen.

Bei der Lösung eines Problems generiert AlphaProof mögliche Lösungen und beweist oder widerlegt diese, indem es nach möglichen Beweisschritten in Lean sucht.

Jeder gefundene und verifizierte Beweis wird verwendet, um das Sprachmodell von AlphaProof zu stärken, damit es in Zukunft schwierigere Probleme lösen kann.

Um AlphaProof zu trainieren, haben Forscher in den Wochen vor und während des Wettbewerbs Millionen von Fragen bewiesen oder widerlegt, die ein breites Spektrum an Schwierigkeitsgraden und mathematischen Themenbereichen abdeckten.

Während des Wettbewerbs wandten sie außerdem eine Trainingsschleife an, indem sie die Beweise an selbst generierten Variationen des Wettbewerbsproblems verstärkten, bis eine vollständige Lösung gefunden wurde.

Infografik zum Ablauf der AlphaProof-Lerntrainingsschleife: Ungefähr eine Million informelle mathematische Probleme werden vom formalen Netzwerk in eine formale mathematische Sprache übersetzt und das Lösernetzwerk trainiert sich dann nach und nach mithilfe des AlphaZero-Algorithmus, indem es nach Beweisen oder Widerlegungen dieser Probleme sucht , um anspruchsvollere Probleme zu lösen

AlphaGeometry 2

AlphaGeometry 2, die aktualisierte Version von AlphaGeometry, ist ein neural-symbolisches Hybridsystem, das von Grund auf auf der Grundlage des Gemini-Sprachmodells trainiert wurde.

Basierend auf einer Größenordnung mehr synthetischen Daten als die vorherige Generation kann es schwierigere geometrische Probleme lösen, einschließlich Gleichungen, die Objektbewegungen, Winkel, Proportionen, Abstände usw. betreffen.

Darüber hinaus verfügt es über eine symbolische Engine, die zwei Größenordnungen schneller ist als sein Vorgänger. Wenn neue Probleme auftreten, nutzt es einen neuartigen Wissensaustauschmechanismus, der erweiterte Kombinationen verschiedener Suchbäume ermöglicht, um komplexere Probleme zu lösen.

Bevor AlphaGeometry 2 dieses Jahr an der IMO teilnahm, hatte es bereits große Erfolge erzielt: Es konnte 83 % der IMO-Geometrieprobleme der letzten 25 Jahre lösen, während die erste Generation nur 53 % lösen konnte.

Meiner Meinung nach hat die Geschwindigkeit von AlphaGeometry 2 alle schockiert – innerhalb von 19 Sekunden nach Erhalt der formellen Frage wurde Frage 4 gelöst!

Frage 4 erfordert den Nachweis, dass die Summe von ∠KIL und ∠XPY gleich 180° ist. AlphaGeometry 2 empfiehlt, einen Punkt E auf der BI-Linie so zu konstruieren, dass ∠AEB=90°.Punkt E hilft dabei, den Mittelpunkt L von AB zu bestimmen, indem er viele ähnliche Dreieckspaare wie ABE ~ YBI und ALE ~ IPC bildet und so die Schlussfolgerung beweist

KI-Problemlösungsprozess

Es ist erwähnenswert, dass diese Fragen zunächst manuell in eine formale mathematische Sprache übersetzt werden, bevor sie an die KI übermittelt werden.
Platz 1

Im Allgemeinen ist die erste Frage (P1) in jedem IMO-Test relativ einfach.

Netizens sagten: „P1 erfordert nur Mathematikkenntnisse der Oberstufe und menschliche Spieler schaffen es normalerweise innerhalb von 60 Minuten.“

Die erste Frage von IMO 2024 untersucht hauptsächlich die Eigenschaften der reellen Zahl α und erfordert die Suche nach einer reellen Zahl α, die bestimmte Bedingungen erfüllt.

AI hat die richtige Antwort gegeben: α ist eine gerade ganze Zahl. Wie genau wird die Frage beantwortet?

Im ersten Schritt zur Lösung des Problems stellte die KI zunächst einen Satz auf, dass die linken und rechten Mengen gleich sind.

Die Menge auf der linken Seite stellt dar, dass alle reellen Zahlen α, die die Bedingungen erfüllen, für jede positive ganze Zahl n, n ⌊i*α⌋ von 1 bis n teilen können; die Menge auf der rechten Seite stellt dar, dass es eine ganze Zahl k, k ist eine gerade Zahl und die reelle Zahl α ist gleich k.

Der folgende Beweis ist in zwei Richtungen unterteilt.

Beweisen Sie zunächst, dass die Menge rechts eine Teilmenge (einfache Richtung) der Menge links ist.

Beweisen Sie dann, dass die Menge links eine Teilmenge der Menge rechts ist (schwierige Richtung).

Bis zum Ende des Codes entwickelte die KI eine Schlüsselgleichung ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋) und verwendete die Gleichung, um zu beweisen, dass α ein sein muss gerade Zahl.

Schließlich fasste DeepMind die drei Axiome zusammen, auf die sich KI im Problemlösungsprozess stützt: propext, Classical.choice und Quot.sound.

Das Folgende ist der vollständige Problemlösungsprozess von P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

Platz 2

Die zweite Frage untersucht die Beziehung zwischen dem Paar positiver Ganzzahlen (a, b), die die Eigenschaft des größten gemeinsamen Teilers beinhaltet.

Die von KI gelöste Antwort lautet:

Der Satz besagt, dass die Menge eines Paares positiver Ganzzahlen (a, b), das bestimmte Bedingungen erfüllt, nur (1,1) enthalten kann.

Im folgenden Problemlösungsprozess besteht die Beweisstrategie der KI darin, zunächst zu beweisen, dass (1,1) die gegebenen Bedingungen erfüllt, und dann zu beweisen, dass dies die einzige Lösung ist.

Beweisen Sie, dass (1,1) die endgültige Lösung ist, indem Sie g=2, N=3 verwenden.

Zeigen Sie, dass, wenn (a,b) die Lösung ist, ab+1 g teilen muss.

In diesem Prozess nutzte die KI den Satz von Euler und die Eigenschaften modularer Operationen zur Argumentation.

Beweisen Sie abschließend, dass a=b=1 die einzig mögliche Lösung ist.

Das Folgende ist der vollständige Problemlösungsprozess von P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

Platz 4

P4 ist eine geometrische Beweisfrage, die den Nachweis einer bestimmten geometrischen Winkelbeziehung erfordert.

Wie oben erwähnt, schaffte AlphaGeometry 2 dies in 19 Sekunden und stellte damit einen neuen Rekord auf.

Abhängig von der gegebenen Lösung werden wie bei der AlphaGeometry der ersten Generation Hilfspunkte in allen Lösungen automatisch vom Sprachmodell generiert.

Im Beweis verwendet die gesamte Winkelverfolgung die Gaußsche Eliminierung und d(AB)−d(CD) ist gleich dem Richtungswinkel von AB nach CD (modulo π).

Während des Problemlösungsprozesses markiert die KI manuell Paare ähnlicher Dreiecke und kongruenter Dreiecke (rot markiert).

Als nächstes folgen die Schritte zur Lösung des AlphaGeometry-Problems, das durch die Verwendung der „Widerspruchsmethode“ vervollständigt wird.

Verwenden Sie zunächst Lean, um die zu beweisenden Aussagen zu formalisieren und die geometrische Konstruktion zu visualisieren.

Die wichtigsten Schritte im Beweis sind wie folgt.

Den vollständigen Problemlösungsprozess finden Sie im Bild unten: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

Platz 6

Die sechste IMO-Frage ist die „ultimative Cheffrage“, die die Eigenschaften von Funktionen untersucht und den Nachweis spezifischer Schlussfolgerungen über rationale Zahlen erfordert.

KI löst, c=2.

Schauen wir uns zunächst die Theorem-Anweisung an, die die Eigenschaften der „Aquaesulschen Funktion“ definiert und erklärt, dass für alle derartigen Funktionen die Wertemenge von f(r)+f(-r) höchstens 2 Elemente hat.

Die Beweisstrategie besteht darin, zunächst zu beweisen, dass für jede Aquaesulsche Funktion die Wertemenge von f(r)+f(-r) höchstens 2 Elemente hat. Konstruieren Sie dann eine bestimmte Aquaesulsche Funktion, sodass f(r)+f(-r) genau zwei verschiedene Werte hat.

Beweisen Sie, dass f(x)+f(-x) höchstens zwei verschiedene Werte annimmt, wenn f(0)=0, und beweisen Sie, dass es keine Aquaesulsche Funktion f(0)≠0 gibt.

Konstruieren Sie die Funktion f(x)=-x+2⌈x⌉ und beweisen Sie, dass es sich um eine Aquaesulsche Funktion handelt.

Beweisen Sie abschließend, dass für diese Funktion f(-1)+f(1) =0 und f(1/2)+f(-1/2)=2 zwei verschiedene Werte sind.

Im Folgenden finden Sie den vollständigen Problemlösungsprozess: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Sie können Olympia-Mathefragen beantworten, aber können Sie erkennen, welche größer ist, 9,11 oder 9,9?

Andrew Gao, ein Forscher an der Stanford University und Sequoia, bekräftigte die Bedeutung dieses KI-Durchbruchs –

Das Wichtigste ist, dass die neuesten IMO-Testfragen nicht im Trainingsset enthalten sind. Das ist wichtig, denn es zeigt, dass KI mit neuen, ungesehenen Problemen umgehen kann.

Darüber hinaus galten durch KI erfolgreich gelöste geometrische Probleme aufgrund der Beschaffenheit des Raums (der intuitives Denken und räumliches Vorstellungsvermögen erforderte) schon immer als äußerst herausfordernd.

Jim Fan, ein leitender Wissenschaftler bei Nvidia, veröffentlichte einen langen Artikel, in dem er sagte, dass große Modelle mysteriöse Existenzen seien –

Sie können Silbermedaillen bei Mathematikolympiaden gewinnen und machen häufig Fehler bei Fragen wie „Welche Zahl ist größer, 9,11 oder 9,9?“

Nicht nur Gemini, sondern auch GPT-4o, Claude-3.5 und Llama-3 können nicht 100 % richtig antworten.

Durch das Training von KI-Modellen erforschen wir weite Bereiche, die über unsere eigene Intelligenz hinausgehen.Dabei entdeckten wir ein sehr seltsames Gebiet – einen Exoplaneten, der wie die Erde aussieht, aber voller seltsamer Täler ist

Das scheint unvernünftig, aber wir können es anhand der Trainingsdatenverteilung erklären:

AlphaProof und AlphaGeometry 2 werden auf formale Beweise und domänenspezifische symbolische Engines trainiert. Bis zu einem gewissen Grad sind sie besser darin, spezielle Olympia-Probleme zu lösen, auch wenn sie auf einem allgemeinen LLM basieren. Der Trainingssatz von GPT-4o ist mit einer großen Menge an GitHub-Codedaten gemischt, die die mathematischen Daten weit übersteigen können. Unter den Softwareversionen kann „v9.11 > v9.9“ die Datenverteilung erheblich verzerren. Daher ist dieser Fehler einigermaßen verständlich.

Der Chef der Google-Entwickler sagte, dass Modelle, die schwierige mathematische und physikalische Probleme lösen können, der Schlüsselweg zu AGI seien, und heute haben wir einen weiteren Schritt auf diesem Weg gemacht.

Andere Internetnutzer sagten, dass es diese Woche zu viele Informationen gegeben habe.

Verweise:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181