KI-Mathematiker von Tsinghua University ist da: Er verfolgt Ideen konsequent bis zu mathematischen Theoremen und ist an der Fertigstellung einer 84-seitigen Arbeit über Quantenalgorithmen beteiligt.
Der KI-Mathematiker ist dieses Mal nicht nur zum Lösen von Übungsaufgaben gekommen.
Zuvor hat das Team von Professor Liu Yang, dem Direktor des Instituts für Intelligente Industrie (AIR) der Tsinghua-Universität, ein Agentensystem für die mathematische Forschung vorgestellt –
AIM.
Im Gegensatz zu vielen früheren Agenten, die sich auf das Lösen von Aufgaben konzentrieren, beantwortet AIM nicht nur mathematische Fragen, sondern versucht auch, an einem früheren Punkt der wissenschaftlichen Arbeit mitzuwirken:
Es kann Forscher dabei unterstützen, Ideen zu entwickeln, Theoreme zu strukturieren und Beweisentwürfe zu erstellen, die dann von Menschen weiter überprüft werden.
Kürzlich haben Wang Yanqiao, ein gemeinsam ausgebildeter Student von AIR und der Qiuzhen-Hochschule, sowie Assistenzprofessor Liu Jinpeng von der Qiuzhen-Hochschule eine bahnbrechende Forschung zu Quantenalgorithmen abgeschlossen, bei der KI tief eingebunden ist –
Sign Embedding Quantum Algorithms for Matrix Equations and Matrix Functions.
Diese Forschung begann mit einer vagen Intuition: Kann die rationale Approximation ein Gestaltungsprinzip für Quantenalgorithmen werden?
Im Forschungsprozess half die KI zuerst den menschlichen Forschern, die möglichen Wege auszulegen, bevor die Menschen die Richtungen auswählten, die Annahmen prüften und die Ableitungen korrigierten. AIM beteiligte sich in späteren Phasen an der Strukturierung von Theoremen, der Erstellung von Beweisentwürfen und der Komplexitätsanalyse.
Schließlich stellte das Forschungsteam Sign-Embedding-Quantenalgorithmen vor und erstellte eine 84-seitige Arbeit zu Quantenalgorithmen.
Man kann sagen, dass AIM im Vergleich zu früheren Fällen, bei denen hauptsächlich von Forschern vorgegebene offene mathematische Probleme gelöst wurden, dieses Mal an der Formulierung von Forschungsproblemen und der Erkundung von Richtungen beteiligt ist.
Wie wurde das erreicht?
Die mathematischen Fähigkeiten der KI entwickeln sich vom „Lösen von Aufgaben“ zur „Forschung“
In den letzten Jahren hat die KI kontinuierliche Fortschritte in Bereichen wie mathematisches Schlussfolgern, Algorithmensuche, Vermutungsprüfung und Beweisunterstützung erzielt.
Viele vorhandene Fälle richten sich hauptsächlich an relativ klare Aufgaben: Ein Satz, der bewiesen oder widerlegt werden muss, eine Zielfunktion, die optimiert werden soll, oder ein Suchraum, der von einem Programm ausgeführt und bewertet werden kann.
In der tatsächlichen fortgeschrittenen mathematischen Forschung finden wichtige Fortschritte jedoch oft statt, bevor Theoreme offiziell formuliert werden.
Forscher haben möglicherweise zuerst eine vage Intuition, einen domänenübergreifenden Analogieschluss oder eine noch nicht ausgeformte technische Vorliebe, bevor sie allmählich bestimmen, in welches Problem sie umgewandelt werden soll, welche Annahmen verwendet werden, auf welchem Weg fortgeführt wird und welche Familie von Theoremen schließlich entsteht.
Diese Phase ist oft schwer mit Standardantworten oder einzelnen numerischen Indikatoren zu bewerten, beeinflusst aber direkt den Wert und die Richtung der Forschung.
Zu der Frage „Kann KI bei der Formulierung von Problemen helfen?“ liefert die Forschung ein relativ vollständiges Beobachtungsbeispiel:
KI und AIM werden in einen Forschungszyklus eingebunden, der von menschlichen Forschern überwacht wird, und beteiligen sich sowohl an der Erkundung und Ableitung als auch an der fortlaufenden Prüfung, Überarbeitung und Integration.
Voneiner Meta-Idee zu einer prüfbaren Familie von Theoremen
Es ist erwähnenswert, dass die Forschung nicht mit einem bereits genau definierten Theorem zu Quantenalgorithmen begann, sondern aus einer umfassenden Intuition eines menschlichen Forschers stammte:
Die rationale Approximation hat Vorteile bei der Behandlung von stufenförmigen Funktionen, insbesondere der Sign-Funktion – kann diese Idee als Gestaltungsprinzip für Quantenalgorithmen dienen?
In der frühen Erkundung erweiterten die Forscher diese Intuition durch die Interaktion mit einem allgemeinen KI-Modell zu einer Gruppe von möglichen Forschungsrichtungen und Vergleichsdimensionen.
Anschließend wählten die menschlichen Forscher anhand mathematischer Vorlieben, technischer Machbarkeit und potenzieller Beiträge aus und konzentrierten sich allmählich auf den Weg des „Sign-Embedding“.
AIM diente in späteren Phasen als Teil des Mensch-KI-Kooperationssystems und half, den ausgewählten Weg in prüfbare Theoremziele und Ableitungsmaterialien zu strukturieren.
Die daraus resultierende Arbeit zu Quantenalgorithmen umfasst insgesamt 84 Seiten. Die folgende Abbildung zeigt die Rolle, die KI/AIM bei der Entstehung dieser Arbeit gespielt hat.
Es ist zu beachten, dass die Funktionen der Wegverbreiterung, der Strukturierung möglicher Richtungen und des Vergleichs, die frühzeitig durch allgemeine KI-Konversationen erledigt wurden, in der späteren Version AIM v2 weiter zu systematischen Fähigkeiten ausgebaut wurden.
Das heißt, dieses Beispiel zeigt nicht nur einen konkreten Forschungsprozess, sondern spiegelt auch die Entwicklung von AIM wider – von der interaktiven Unterstützung hin zur umfassenderen Unterstützung des gesamten wissenschaftlichen Arbeitsablaufs.
Mensch-KI-Arbeitsablauf: Hochdurchsatz-Erkundung durch KI unter der Kontrolle menschlicher Wertvorstellungen
Aus der Perspektive der KI-Forschung liegt der Schwerpunkt dieser Arbeit nicht darin, „vollautomatische mathematische Entdeckungen“ zu demonstrieren, sondern einen nachverfolgbaren, prüfbaren und wiederverwendbaren Mensch-KI-Kooperationsprozess vorzustellen.
Der gesamte Prozess kann in fünf Schritte zusammengefasst werden.
Divergente Wegverbreiterung: Menschliche Forscher liefern eine zentrale Meta-Idee oder eine umfassende wissenschaftliche Intuition, und die KI erweitert sie zu mehreren möglichen Problemen, technischen Wegen und domänenübergreifenden Verbindungen, sodass die Forscher den umliegenden Forschungsraum schneller erfassen können.
Menschliche Wertkontrolle: Angesichts der von der KI generierten möglichen Zweige wählen und konzentrieren sich menschliche Forscher anhand akademischer Urteile, des Problemwerts und der technischen Machbarkeit und entscheiden, welche Richtungen weitere Investitionen wert sind.
Theoremformulierung und Ableitung: Nachdem der Hauptweg festgelegt wurde, hilft AIM, die übergeordneten Ideen in prüfbare Materialien wie Theorembeschreibungen, Zerlegungen von Lemmata, Beweisentwürfe und Komplexitätsausdrücke umzuwandeln.
Komplexitätsprüfung und -korrektur: In der Forschung zu Quantenalgorithmen bedeutet ein korrekter Beweis nicht automatisch, dass der Beitrag des Algorithmus ausreichend ist; ob die Annahmen natürlich sind, das Zugriffsmodell angemessen ist und die Komplexität zu locker ist, muss wiederholt überprüft werden. Der Prozess der Korrektur, Optimierung oder Neustrukturierung kann weiterhin mithilfe der Schlussfolgerungs-, Vergleichs- und Neuschreibfähigkeiten von KI/AIM abgeschlossen werden, aber die wichtigen Urteile und die endgültige Bestätigung müssen von menschlichen Forschern übernommen werden.
Validierung und Integration: Alle mathematischen Aussagen, Beweise, Annahmen, Komplexitätsschätzungen und Beitragsbeschreibungen müssen schließlich von menschlichen Forschern überprüft, ausgewählt, umgeschrieben und integriert werden, bevor sie in die öffentliche Arbeit aufgenommen werden.
Verknüpfung von Entdeckung, Ableitungsgenerierung und sorgfältiger Prüfung
Im Allgemeinen besteht die Bedeutung von AIM nicht darin, menschliche Mathematiker zu ersetzen, um Forschung unabhängig durchzuführen, sondern die Erkundungsdichte und die Effizienz der Ableitung in einem von Menschen überwachten Zyklus zu erhöhen.
KI/AIM kann schnell mögliche Wege erweitern, die Verbindungen zwischen verwandten Konzepten strukturieren und prüfbare Beweis- und Komplexitätsentwürfe generieren;
Menschliche Forscher entscheiden dagegen, welche Wege Forschungswert haben, welche Annahmen akzeptabel sind und welche Ableitungen korrigiert werden müssen.
Dieses Kooperationsmodell macht den Forschungsprozess eher zu „Hochdurchsatz-Generierung von Möglichkeiten + menschliche Wertkontrolle + KI-unterstützte Prüfung und Korrektur + menschliche endgültige Integration“.
Sein Vorteil liegt nicht darin, dass die von der KI ausgegebenen Ergebnisse direkt zu endgültigen Schlussfolgerungen werden, sondern darin, dass die ursprünglich kaum erschöpfende Wegerkundung, Verbindungsstrukturierung und lokale Ableitung in prüfbare, vergleichbare und schrittweise überarbeitbare Zwischenmaterialien umgewandelt werden.
Für die Forschung an AI4Math und KI-Wissenschaftlern ergibt sich daraus auch eine Erkenntnis: Die Rückkopplungssignale in der theoretischen Forschung sind oft keine experimentellen Punktzahlen, sondern mathematische Urteile.
Das System muss Langzeitgedächtnis, Wegverwaltung, Aufzeichnung von Annahmen, Komplexitätsprüfung und Widerlegungsprüfung unterstützen, sodass menschliche Forscher die Richtung effektiver steuern, Fehler entdecken und die endgültigen Ergebnisse stabilisieren können.
Sign-Embedding-Quantenalgorithmen
Als technisches Ergebnis dieses Kooperationsprozesses richten sich die von Wang Yanqiao und Liu Jinpeng vorgestellten „Sign-Embedding-Quantenalgorithmen“ an eine Klasse von Problemen mit Matrixgleichungen und Matrixfunktionen, einschließlich der Gleichungen von Sylvester, Lyapunov und Riccati sowie Objekten wie Matrix-Quadratwurzeln, inversen Quadratwurzeln und geometrischen Mitteln von Matrizen.
Diese Probleme haben eine grundlegende Bedeutung in der numerischen linearen Algebra, der Steuerungstheorie, dynamischen Systemen und dem wissenschaftlichen Rechnen.
Für Leser ohne Hintergrund im Quantenbereich kann die Kernidee dieser Arbeit so verstanden werden: Zuerst werden mehrere Arten strukturierter Matrixprobleme in die Sign-Funktion oder die Sign-Projektion einer erweiterten Matrix eingebettet,
Anschließend werden die entsprechenden Objekte durch Quantenalgorithmus-Primitive wie rationale Approximation und verschobene Inverse realisiert. Dieser Weg „zuerst einbetten, dann approximieren“ bietet eine einheitliche Strukturierung für mehrere scheinbar unterschiedliche Probleme.
Die technischen Beiträge dieser Quantenarbeit umfassen: Die Herstellung brauchbarer Annahmen und Komplexitätsformulierungen unter allgemeineren Eingabebedingungen wie nicht normalen, nicht diagonalisierbaren Matrizen;
Die Erweiterung der Ausgabe von einzelnen Vektorzuständen zu blockweisen Matrixkodierungen, die von nachgeschalteten Quantenkreisen aufgerufen werden können; und die Bildung eines systematischen Quanten-linearen-Algebra-Frameworks für Operatorausgaben durch Skalierung, Neugewichtung und Komplexitätsprüfung der Implementierungsebene von verschobenen Inversen.
Menschliche Urteile und KI-Produktivität in der theoretischen Forschung
Im Allgemeinen stellt die Forschung eine relativ realistische Art dar, wie KI an der mathematischen Forschung beteiligt ist:
KI kann Forschern helfen, Wege schneller zu erweitern, Zusammenhänge zu ordnen, Beweise zu entwerfen und erste Komplexitätsanalysen durchzuführen, wodurch die expliziten Kosten einiger grundlegender Ableitungen und lokaler Erkundungen in der theoretischen Forschung gesenkt werden.
Gleichzeitig hängen jedoch die Frage, ob eine Forschungsrichtung vertieft werden soll, ob die Annahmen natürlich und angemessen sind und ob die Ergebnisse ausreichenden theoretischen Wert haben, weiterhin von den fachlichen Urteilen und der fortlaufenden Prüfung der Forscher ab.
Da Agenten schnell eine große Anzahl möglicher Wege, Beweisentwürfe und technische Beschreibungen generieren können, kann sich der Arbeitsschwerpunkt theoretischer Wissenschaftler ebenfalls verändern.
Nachdem ein Teil der Kosten für mühsame Ableitungen gesenkt wurde, können Forscher mehr Energie in die Richtungsauswahl, die Problemformulierung, die Kontrolle von Annahmen und die Prüfung von Ergebnissen investieren.
Mit anderen Worten: Die Fähigkeit, zu beurteilen, „welche Probleme wirklich erforschenswert sind“, und Wege zu erkennen, die oberflächlich angemessen erscheinen, aber verborgene Bedingungen, technische Mängel oder unzureichende Beiträge aufweisen, wird zu einer noch wichtigeren Fähigkeit.
Dies liefert auch wichtige Erkenntnisse für die zukünftige Entwicklung von AIM. Es lohnt sich, nicht nur die Fähigkeiten zum punktuellen Beweis oder zur lokalen Ableitung weiter zu stärken, sondern auch die systemischen Fähigkeiten zu unterstützen, die den gesamten wissenschaftlichen Prozess begleiten:
Zum Beispiel das Aufzeichnen und Vergleichen verschiedener Forschungswege, das explizite Verwalten wichtiger Annahmen, das Speichern nachverfolgbarer Ableitungsspuren, das Entdecken verborgener Bedingungen und Komplexitätsmängel sowie das Unterstützen von Forschern bei der anschließenden Korrektur, Optimierung und Neustrukturierung mit KI-Hilfe.
Dieses Beispiel zeigt, dass sich der Wert von KI in der fortgeschrittenen theoretischen Forschung schrittweise von der Unterstützung lokaler Aufgaben auf den umfassenderen Forschungsprozess aus