DeepMinds AlphaProof-System l\u00f6ste vier von sechs Problemen bei der Internationalen Mathematikolympiade 2024 und erzeugte formal verifizierte Beweise durch Verst\u00e4rkungslernen, das an Millionen automatisch formalisierten Problemen trainiert wurde. Dieses Ergebnis, in einer aktuellen Nature-Studie berichtet, signalisiert eine breitere Verschiebung. K\u00fcnstliche Intelligenz unterst\u00fctzt Mathematiker nicht nur, sie ver\u00e4ndert aktiv die Mechanik, wie Beweise geschrieben, gepr\u00fcft und entdeckt werden.<\/p>\n\n\n\n\n\n\n\n\n\n
AlphaProof orientiert sich an AlphaZero, dem Spielagenten, der im Schach und Go Meisterschaftsniveau erreichte. Statt Brettstellungen durchsucht es jedoch formale Beweiszust\u00e4nde im Lean-Beweisassistenten. Das System lernt, formale Beweise durch Verst\u00e4rkungslernen zu finden, indem es an Millionen von Problemen trainiert wird, die automatisch in formale mathematische Sprache \u00fcbersetzt wurden. Jeder Kandidatenbeweis wird von einer Verifikations-Engine gepr\u00fcft, wodurch ein Feedback-Loop entsteht, in dem das Modell dadurch besser wird, dass best\u00e4tigt wird, welche Schlussfolgerungsschritte tats\u00e4chlich standhalten.<\/p>\n
Die Leistung bei der IMO 2024 ist bemerkenswert, weil Wettbewerbsaufgaben an der Grenze dessen liegen, was trainierte menschliche Teilnehmer unter Zeitdruck leisten k\u00f6nnen. AlphaProof arbeitete in einem formalen Rahmen, das hei\u00dft jeder von ihm produzierte Schritt war maschinenpr\u00fcfbar, statt sich auf die Art intuitiver Spr\u00fcnge zu verlassen, die handschriftliche Beweise kennzeichnen. Diese Unterscheidung ist wichtig. Ein formal verifizierter Beweis l\u00e4sst keine L\u00fccken f\u00fcr versteckte Fehler, genau der Standard, den skeptische Mathematiker verlangen, bevor sie maschinell erzeugter Argumentation vertrauen.<\/p>\n
AlphaProofs Trainingspipeline deutet auch an, wie zuk\u00fcnftige Systeme gebaut werden k\u00f6nnten. Indem gro\u00dfe Mengen von Problemen automatisch formalisiert und dann Verst\u00e4rkungslernen eingesetzt wurde, um den entstehenden Suchraum zu durchqueren, umgingen die Entwickler die Knappheit handgeschriebener formaler Beweise. Das System lernte effektiv eine Strategie zur Beweiskonstruktion, nicht geleitet durch menschliche Demonstrationen, sondern durch die strengen Zw\u00e4nge eines Beweispr\u00fcfers. In diesem Sinne ist der IMO-Auftritt weniger ein Gimmick und mehr ein Beleg daf\u00fcr, dass formale Beweissuche auf wirklich herausfordernde Mathematik skalieren kann.<\/p>\n\n\n\n\n\n\n\n
AlphaProof ist nicht das einzige System, das diese Grenzen verschiebt. AlphaGeometry, ver\u00f6ffentlicht als peer-reviewed Studie in Nature, stellte einen neuro-symbolischen Rahmen<\/a> vor, der ein auf synthetischen Daten trainiertes neuronales Sprachmodell mit einer symbolischen Deduktionsmaschine koppelt. Die neuronale Komponente schl\u00e4gt geometrische Konstruktionen und Zwischenschritte vor, w\u00e4hrend die symbolische Engine logische Konsistenz durch Pr\u00fcfung jedes deduktiven Schrittes durchsetzt. Diese Arbeitsteilung erlaubt dem Modell, kreative geometrische Ideen zu erkunden, ohne die Strenge formalen Schlussfolgerns zu opfern.<\/p>\n Der Nachfolger, AlphaGeometry2, erweiterte diesen Ansatz und wurde an historischen Olympiadengeometrie-Aufgabens\u00e4tzen evaluiert. Laut einem arXiv-Preprint<\/a> erreichte das System die Leistung der besten menschlichen Goldmedaillengewinner und l\u00f6ste einen vergleichbaren Anteil an Aufgaben unter \u00e4hnlichen Bedingungen, und das ohne sich w\u00e4hrend des Trainings auf menschliche L\u00f6sungsspuren zu st\u00fctzen. Dieses Ergebnis legt nahe, dass KI zumindest in strukturierten Dom\u00e4nen wie der euklidischen Geometrie Probleml\u00f6seheuristiken internalisieren kann, die fr\u00fcher als das Ergebnis jahrelanger spezialisierter menschlicher Praxis galten.<\/p>\n Im Bereich der Kombinatorik ging FunSearch einen anderen Weg. Statt Theoreme direkt zu beweisen, nutzte es ein gro\u00dfes Sprachmodell innerhalb einer evolution\u00e4ren Suchschleife, um Kandidatenprogramme zu generieren, die anschlie\u00dfend auf ihre mathematische Qualit\u00e4t bewertet wurden. Dieser Ansatz, beschrieben in einem Nature-Aufsatz \u00fcber neue kombinatorische Konstruktionen<\/a>, produzierte neuartige Cap-Set-Beispiele und verbesserte Heuristiken f\u00fcr das Bin-Packing-Problem. Der entscheidende Punkt ist, dass das System mathematische Objekte und Algorithmen entdeckte, die zuvor nicht von Menschen katalogisiert worden waren, was unterstreicht, dass generative Modelle wirklich neue Ideen beitragen k\u00f6nnen und nicht nur bestehendes Material remixen.<\/p>\n\n\n\n\n\n\n\n Trotz dieser Fortschritte bleibt eine best\u00e4ndige Herausforderung die L\u00fccke zwischen der Art, wie Mathematiker denken, und wie Beweisassistenten arbeiten. Von Menschen verfasste L\u00f6sungen, insbesondere auf Olympiadeniveau, st\u00fctzen sich oft auf Einsichten auf hohem Abstraktionsniveau, geschickte Substitutionen und informelle Diagramme. Solche \u00dcberlegungen in einen maschinenpr\u00fcfbaren Beweis zu \u00fcberf\u00fchren, erfordert in der Regel die Zerlegung des Arguments in viele kleine Lemmata, die jeweils in der starren Syntax eines Beweisassistenten ausgedr\u00fcckt sind. Eine k\u00fcrzlich ver\u00f6ffentlichte arXiv-Analyse von Olympiadeaufgaben<\/a> fand, dass sich eine einzelne Wettbewerbsfrage beim \u00dcbersetzen in Lean in Dutzende formaler Schritte aufbl\u00e4hen kann, was veranschaulicht, wie schnell die Komplexit\u00e4t explodiert.<\/p>\n Dieser Dekonstruktionsprozess ist arbeitsintensiv, und der Mangel an gro\u00dfen, hochwertigen formalen Korpora hat eingeschr\u00e4nkt, wie schnell neuronale Beweiser sich verbessern k\u00f6nnen. DeepSeek-Prover, ein System mit Fokus auf Autoformalisation f\u00fcr formale Mathematik, zielt direkt auf diesen Engpass ab, indem es informelle mathematische Aussagen in gro\u00dfem Ma\u00dfstab in formale \u00fcbersetzt. Durch das Erzeugen ausgerichteter Paare aus informellem und formalem Text sollen die Trainingsdaten geschaffen werden, die moderne Sprachmodelle ben\u00f6tigen, um robuste Beweisstrategien zu erlernen.<\/p>\n Gleichzeitig verfolgt Lean-STaR einen anderen Ansatz: Anstatt von Anfang an auf rein formales Schlie\u00dfen zu bestehen, erzeugt sein Modell informelle Kommentare, die mit Lean-Beweisschritten vermischt sind. Dieser gemischte Stil hat auf dem miniF2F-Benchmark, der Aufgaben aus Wettbewerben wie AMC, AIME und IMO \u00fcber mehrere Beweisassistenten hinweg zusammenfasst, zu besseren Ergebnissen gef\u00fchrt. Die Idee ist, dass es das Modell durch „laut denkende“ nat\u00fcrliche Sprache zu besseren formalen Schritten f\u00fchren kann, \u00e4hnlich wie menschliche Mathematiker Ideen in Prosa skizzieren, bevor sie sie vollst\u00e4ndig formal ausarbeiten.<\/p>\n\n\n\n\n\n\n\nDer Formatisierungsengpass<\/h2>\n\n\n
Mathematiker sind aus gutem Grund vorsichtig<\/h2>\n\n\n