In einer aktuellen, die Mathematikwelt aufregenden Nachricht haben ehemalige Studenten der Tsinghua-Universität mithilfe von KI 162 zuvor ungelöste mathematische Theoreme bewiesen. Noch beeindruckender ist, dass dieses LeanAgent genannte System sogar die formale Herausforderung von Terence Tao an die polynomiale Freiman-Ruzsa-Vermutung gemeistert hat! Dies lässt uns die Forschungsmethoden in den Grundlagenwissenschaften als durch KI grundlegend verändert betrachten.
Bekanntlich sind aktuelle Sprachmodelle (LLMs), obwohl beeindruckend, meist statisch und können keine neuen Kenntnisse online lernen; den Beweis höherer mathematischer Theoreme zu führen, ist für sie schier unmöglich. LeanAgent, gemeinsam entwickelt von Teams am California Institute of Technology, der Stanford University und der University of Washington, ist jedoch ein KI-Assistent mit lebenslangem Lernvermögen, der kontinuierlich lernen und Theoreme beweisen kann.
LeanAgent bewältigt verschiedene Schwierigkeitsgrade in der Mathematik durch einen sorgfältig entwickelten Lernpfad. Eine dynamische Datenbank verwaltet den stetigen Zustrom mathematischen Wissens und stellt sicher, dass es beim Erlernen neuer Kenntnisse bereits erworbenes Wissen nicht vergisst. Experimente zeigen, dass es aus 23 verschiedenen Lean-Code-Repositories 162 zuvor ungelöste mathematische Theoreme bewiesen hat – eine Leistung, die um das Elfache besser ist als bei traditionellen großen Modellen!
Diese Theoreme umfassen viele Bereiche der höheren Mathematik, darunter knifflige Probleme der abstrakten Algebra und der algebraischen Topologie. LeanAgent kann nicht nur von einfachen Konzepten ausgehend komplexe Themen bewältigen, sondern zeigt auch eine hervorragende Leistung in Bezug auf Stabilität und Rückwärtsübertragung.
Tao's Herausforderung stellt die KI jedoch weiterhin vor Probleme. Obwohl interaktive Theorembeweiser (ITPs) wie Lean eine wichtige Rolle bei der Formalisierung und Verifizierung mathematischer Beweise spielen, ist die Erstellung solcher Beweisprozesse oft komplex und zeitaufwendig und erfordert detaillierte Schritte und umfangreiche mathematische Code-Bibliotheken. Moderne große Modelle wie o1 und Claude neigen bei nicht-formalisierten Beweisen zu Fehlern, was die Schwächen von LLMs in Bezug auf Genauigkeit und Zuverlässigkeit bei mathematischen Beweisen aufzeigt.
Frühere Forschungsarbeiten versuchten, LLMs zur Generierung vollständiger Beweisschritte einzusetzen. LeanDojo beispielsweise ist ein Theorembeweiser, der durch Training eines großen Modells auf einem spezifischen Datensatz erstellt wurde. Die Daten für formalisierte Theorembeweise sind jedoch extrem selten, was die breite Anwendbarkeit dieser Methode einschränkt. Ein weiteres Projekt, ReProver, ist ein für die Lean-Theorembeweis-Codebibliothek mathlib4 optimiertes Modell. Obwohl es über 100.000 formalisierte mathematische Theoreme und Definitionen umfasst, beschränkt es sich auf Mathematik auf Bachelor-Niveau und schneidet daher bei komplexeren Problemen schlecht ab.
Die Dynamik der mathematischen Forschung stellt die KI vor eine zusätzliche Herausforderung. Mathematiker bearbeiten oft mehrere Projekte gleichzeitig oder abwechselnd. Terence Tao beispielsweise arbeitet gleichzeitig an verschiedenen Forschungsbereichen, darunter die PFR-Vermutung und die symmetrischen Mittelwerte reeller Zahlen. Diese Beispiele zeigen eine wichtige Schwäche aktueller KI-Theorembeweismethoden: das Fehlen eines KI-Systems, das in verschiedenen mathematischen Bereichen adaptiv lernen und sich verbessern kann, insbesondere bei begrenzten Lean-Daten.
Daher hat das LeanDojo-Team LeanAgent entwickelt, ein neuartiges Framework für lebenslanges Lernen, das die oben genannten Probleme lösen soll. Der Arbeitsablauf von LeanAgent umfasst die Ableitung der Komplexität von Theoremen zur Erstellung von Lernplänen, das Gleichgewicht zwischen Stabilität und Flexibilität während des Lernprozesses durch schrittweises Training und die Verwendung der Best-First-Search zur Suche nach noch nicht bewiesenen Theoremen.
LeanAgent wird mit jedem großen Modell kombiniert und verwendet "Retrieval", um seine Generalisierungsfähigkeit zu verbessern. Seine Innovation liegt in der Verwendung einer benutzerdefinierten dynamischen Datenbank zur Verwaltung des ständig wachsenden mathematischen Wissens und einer auf der Lean-Beweisstruktur basierenden Lernstrategie, die das Lernen komplexerer mathematischer Inhalte unterstützt.
Um das Problem des katastrophalen Vergessens bei KI zu lösen, verwenden die Forscher ein schrittweises Training, das es LeanAgent ermöglicht, sich kontinuierlich an neues mathematisches Wissen anzupassen, ohne zuvor Gelerntes zu vergessen. Dieser Prozess beinhaltet ein inkrementelles Training auf jedem neuen Datensatz, um ein optimales Gleichgewicht zwischen Stabilität und Flexibilität zu gewährleisten.
Durch dieses schrittweise Training zeigt LeanAgent eine hervorragende Leistung beim Beweisen von Theoremen und hat erfolgreich 162 bisher ungelöste Probleme bewiesen, insbesondere herausfordernde Theoreme der abstrakten Algebra und der algebraischen Topologie. Seine Fähigkeit, neue Theoreme zu beweisen, ist elfmal höher als die des statischen ReProver, wobei gleichzeitig die Fähigkeit, bekannte Theoreme zu beweisen, erhalten bleibt.
LeanAgent zeigt im Prozess des Beweisens von Theoremen Merkmale des schrittweisen Lernens, wobei es von einfachen zu komplexeren Theoremen übergeht und sein tiefes Verständnis mathematischen Wissens beweist. Es bewies beispielsweise grundlegende algebraische Struktursätze im Zusammenhang mit der Gruppentheorie und der Ringtheorie und zeigt damit ein tiefes Verständnis der Mathematik. Insgesamt bietet LeanAgent mit seiner starken Fähigkeit zum kontinuierlichen Lernen und zur Verbesserung aufregende Perspektiven für die Mathematik!
论文地址：https://arxiv.org/pdf/2410.06209
