(Lesezeit dieses Artikels: 15 Minuten)
Anmerkung der Redaktion: Obwohl die Fähigkeiten der künstlichen Intelligenz in den letzten Jahren rasant zugenommen haben, gibt es bei komplexen Schlussfolgerungsaufgaben immer noch Defizite. Forscher von Microsoft Research Asia haben dies aus verschiedenen Blickwinkeln untersucht und ständig neue Wege zur Verbesserung der Schlussfolgerungsfähigkeiten großer Modelle erforscht. Von rStar-Math, das die Monte-Carlo-Baumsuche nutzt, um den menschlichen Prozess des „tiefen Denkens“ zu simulieren, über Logic-RL, eine regelbasierte Reinforcement-Learning-Methode, bis hin zu LIPS, das die mathematische Intuition großer Sprachmodelle mit symbolischen Methoden verbindet, und einem neuen Framework zur Verbesserung der Genauigkeit der automatischen Formalisierung. Weiterhin gibt es ein neuro-symbolisches Framework zur automatischen Generierung hochwertiger, überwachter mathematischer Daten sowie die Einführung des einheitlichen Schlussfolgerungs-Frameworks CoR und des Lernens kritischer Planungsphasen CPL – jede Studie bietet eine neue Perspektive und Methode zur Verbesserung der Schlussfolgerungsfähigkeiten großer Modelle.
Die rasante Entwicklung der künstlichen Intelligenz hat ihr in zahlreichen Bereichen leistungsstarke Fähigkeiten verliehen und gleichzeitig immer höhere Erwartungen geweckt, dass die künstliche Intelligenz über tiefgreifende Denk- und Schlussfolgerungsfähigkeiten verfügen möge, um den Menschen bei der Lösung verschiedener „kopflastiger“ komplexer realer Probleme zu helfen.
Um die Schlussfolgerungsfähigkeiten großer Modelle zu verbessern, führen Forscher von Microsoft Research Asia in drei Richtungen Forschung durch: Erstens die Verbesserung der Schlussfolgerungsfähigkeiten durch die Verbesserung der Modelle selbst, sodass auch Modelle kleineren Umfangs eine starke Schlussfolgerungsleistung erzielen können; zweitens das tiefe Erlernen der Regeln des mathematischen Schlussfolgerns, um die Zuverlässigkeit großer Sprachmodelle zu erhöhen; und drittens die Verbesserung der Generalisierungsfähigkeit des Schlussfolgerns, damit das Modell flexibel auf domänenübergreifende Aufgaben angewendet werden kann und so den Fortschritt der allgemeinen künstlichen Intelligenz fördert.
Das Potenzial großer Sprachmodelle freisetzen – Stärkere Schlussfolgerungsfähigkeiten in kleineren Modellen
„Obwohl große, auf Weltwissen trainierte Modelle über riesige Wissensreserven verfügen, haben die bestehenden Modelle ihr volles inhärentes Potenzial nicht ausgeschöpft. Darüber hinaus fehlt den bestehenden Modellen die Fähigkeit zum kontinuierlichen Lernen, was einen starken Kontrast zur menschlichen Fähigkeit darstellt, ständig neues Wissen zu lernen und kognitive Lücken zu schließen“, sagt Dr. Lihong Zhang, Principal Researcher bei Microsoft Research Asia. Hervorragende Schlussfolgerungsfähigkeiten hängen oft von der Unterstützung großer Modelle ab. Daher untersuchen einige Forscher auch, wie ähnliche Schlussfolgerungsfähigkeiten in Modellen kleineren Umfangs erreicht werden können.
Im traditionellen Schlussfolgerungsmodus verwenden große Modelle bei komplexen Problemen oft eine einfache, direkte „intuitive“ Schlussfolgerung, um Antworten zu generieren. Obwohl diese Methode schnell ist, ist sie anfällig für Fehler. Im Gegensatz dazu analysieren Menschen Probleme Schritt für Schritt, versuchen mehrere Ansätze, wägen die Vor- und Nachteile ab und geben dann eine Antwort. Angesichts dessen schlugen die Forscher rStar-Math vor, dessen Kern in der Nutzung der Monte-Carlo-Baumsuche (MCTS) liegt, um den menschlichen Prozess des „tiefen Denkens“ zu simulieren und kleineren Sprachmodellen zu ermöglichen, ein höheres Niveau bei den Schlussfolgerungsfähigkeiten zu erreichen.
rStar-Math erreicht die Selbstentwicklung in drei Schritten: Zuerst werden komplexe mathematische Probleme in mehrere Schlussfolgerungsschritte zerlegt, sodass das Modell allmählich den Beitrag jedes Schrittes erkunden und überprüfen kann, wodurch sichergestellt wird, dass der vom kleinen Modell generierte Schlussfolgerungsweg aus korrekten, qualitativ hochwertigen Zwischenschritten besteht; zweitens wird ein kleines Modell als Prozess-Präferenz-Modell (PPM) trainiert, um Belohnungs-Labels für jeden mathematischen Schlussfolgerungsschritt zuverlässig vorherzusagen, wodurch das gewünschte Prozess-Belohnungs-Modell und eine zuverlässige Annotation erreicht werden; schließlich wird durch ein vierstufiges Selbstentwicklungs-Schema allmählich von Grund auf modernste Politikmodelle und PPMs aufgebaut, wobei in jeder Runde die neuesten Politikmodelle und PPMs für die Monte-Carlo-Baumsuche verwendet werden, um sich schrittweise zu entwickeln und stärkere Politikmodelle und PPMs zu trainieren.
Experimente zeigen, dass rStar-Math seine Wirksamkeit an vier kleinen Sprachmodellen (1,5 Milliarden - 7 Milliarden Parameter) validiert hat. Bei der American Invitational Mathematics Examination (AIME) konnte rStar-Math im Durchschnitt 53,3% (8/15) der Probleme lösen und rangierte damit unter den besten 20% der hervorragendsten Highschool-Mathematikschüler.
rStar-Math: Small LLMs can master math reasoning with self-evolved deep thinking
Paper Link:
https://arxiv.org/pdf/2501.04519
Abbildung 1: Schematische Darstellung von rStar-Math
Die Forscher schlugen auch die regelbasierte Reinforcement-Learning-Methode Logic-RL vor, die die Schlussfolgerungsfähigkeit des Modells bei komplexen Logikproblemen verbessert, indem sie Logikrätsel als Trainingsdaten synthetisiert. Logic-RL führt eine praktische Systemaufforderung und eine strenge Formatbelohnungsfunktion ein, um zu verhindern, dass das Schlussfolgerungsmodell Abkürzungen nimmt. Wenn das Modell beispielsweise Antworten generiert, muss es den Schlussfolgerungsprozess und die Antwort gemäß einem bestimmten Format organisieren, und nur wenn sowohl der Schlussfolgerungsprozess als auch die Antwort die Anforderungen erfüllen, kann es eine höhere Belohnung erhalten, wodurch die Vollständigkeit und Genauigkeit des Schlussfolgerungsprozesses sichergestellt wird.
Nach dem Training mit Logic-RL zeigte das Modell nicht nur eine hervorragende Leistung bei Logikrätseln, sondern auch eine starke Generalisierungsfähigkeit bei mathematischen Wettbewerbs-Benchmarks für kleine Modelle mit 7 Milliarden Parametern (wie AIME und AMC), wobei die Genauigkeit um 125% bzw. 38% verbessert wurde.
Logic-RL: Unleashing LLM reasoning with rule-based reinforcement learning
Paper Link:
https://arxiv.org/pdf/2502.14768
Mathematische Schlussfolgerungsfähigkeiten stärken – Zuverlässigeres Schlussfolgern
Mathematik ist als Eckpfeiler der Wissenschaft von strenger Logik und hoher Präzision geprägt. Für die künstliche Intelligenz wird die Lösung mathematischer Schlussfolgerungsprobleme die Schlussfolgerungsfähigkeiten der KI erheblich verbessern und die breite Anwendung von Modellen in verschiedenen Bereichen fördern. Sich allein auf die Fähigkeiten zur Verarbeitung natürlicher Sprache großer Modelle zu verlassen, reicht jedoch oft nicht aus, um die strengen Standards zu erfüllen, die für mathematische Schlussfolgerungen erforderlich sind. Um dies zu erreichen, verwenden die Forscher formale und symbolische Forschungsmethoden, um den Modellen zu helfen, bestehende menschliche mathematische Methoden und Werkzeuge zu erlernen, mathematische Regeln zu beherrschen und die Effizienz und Genauigkeit der Schlussfolgerungen zu verbessern.
„Natürliche Sprache ist die Sprache der Menschen, nicht die native Sprache von Computern oder großen Modellen, die natürliche Sprache nicht direkt verstehen können. Wir hoffen, die Ausgabe großer Sprachmodelle in Codeform umzuwandeln und sie auf Axiome abzubilden, wie zum Beispiel ‚1+1=2‘, die selbstverständliche Wahrheiten sind, um so die Richtigkeit der Modellausgabe zu überprüfen. Dies ist ähnlich, wie Menschen beim Kommunizieren das Gehörte in ihr eigenes Verständnis umwandeln, während wir es durch einen Formalisierungsprozess in Werkzeuge umwandeln, die Computer verstehen können“, sagt Dr. Xian Zhang, Senior Researcher bei Microsoft Research Asia.
Mathematische Sprache umfasst mathematische Theoreme, Ungleichheitsbeweise usw., die sich signifikant vom Sprachsystem großer Sprachmodelle unterscheiden. Um großen Modellen das Verständnis mathematischer Probleme zu ermöglichen, ist es zunächst notwendig, mathematische Probleme durch formale und symbolische Methoden in Codeform umzuwandeln und sie dann auf computerverständliche Axiome abzubilden. Darauf basierend entwickelten die Forscher den LLM-basierten Ungleichheitsbeweiser mit symbolischem Schlussfolgern (LIPS). Er integriert auf kreative Weise die mathematische Intuition großer Modelle mit domänenspezifischen Erkenntnissen, die durch symbolische Methoden kodiert sind, um zu bestimmen, welche Teile des mathematischen Schlussfolgerns am besten für große Modelle geeignet sind und welche besser von symbolischen Methoden gehandhabt werden.
Durch die Analyse, wie Menschen solche Probleme lösen, extrahiert LIPS zwei Strategien: eine ist das Skalieren (Scaling), das von symbolischen Methoden behandelt wird; die andere ist das Umschreiben (Rewriting), das von großen Modellen behandelt wird. Nach der Evaluierung von LIPS an 161 herausfordernden Ungleichungen aus mehreren Mathematikwettbewerben zeigen die Ergebnisse, dass LIPS die derzeit fortschrittlichste Leistung demonstrierte und vorhandene große Modelle und symbolische Methoden ohne zusätzliche Trainingsdaten erheblich übertraf.
Proving Olympiad inequalities by synergizing LLMs and symbolic reasoning
Paper Link:
https://openreview.net/pdf?id=FiyS0ecSm0
Abbildung 2: LIPS Ungleichheitsbeweiser mit symbolischem Schlussfolgern
Obwohl formale Methoden bei verschiedenen mathematischen Schlussfolgerungsaufgaben großes Potenzial für große Modelle gezeigt haben, ist die Erfolgsquote großer Modelle bei der automatischen Formalisierung von Datenanweisungen immer noch gering. Speziell bei der automatischen Formalisierung großer Modelle gibt es einen signifikanten Unterschied zwischen der One-Pass-Rate (das erste generierte Ergebnis ist korrekt) und der K-Pass-Rate (eines der besten K generierten Ergebnisse ist korrekt).
Um diese Lücke zu schließen, führten die Forscher ein neues Framework ein, das die Selbstkonsistenz für die automatische Formalisierung aus zwei innovativen und komplementären Dimensionen herstellt – symbolische Äquivalenz und semantische Konsistenz. Symbolische Äquivalenz erweitert traditionelle Vergleiche (wie Endergebnisse und Ausführungsverhalten), um die logische Äquivalenz zwischen automatischen Formalisierungskandidaten zu überprüfen. Semantische Konsistenz korrigiert unerwartete Schlussfolgerungsunterschiede, die die symbolische Äquivalenz möglicherweise übersehen könnte, indem sie die Einbettungsähnlichkeit zwischen re-non-formalisierten (umgekehrt übersetzten) Ergebnissen und den ursprünglichen natürlichen Sprachanweisungen misst. Diese Methode stellt sicher, dass der automatische Formalisierungsprozess die beabsichtigte Bedeutung und Kohärenz der ursprünglichen Anweisungen bewahrt. Experimente auf den Datensätzen MATH und miniF2F zeigten, dass diese Methode die Genauigkeit der automatischen Formalisierung erheblich verbesserte und eine relative Verbesserung von bis zu 0,22-1,35 Mal bei verschiedenen großen Sprachmodellen und Baseline-Methoden erzielte.
Autoformalizing mathematical statements by symbolic equivalence and semantic consistency
Paper Link:
https://openreview.net/pdf?id=8ihVBYpMV4
Abbildung 3: Framework zur automatischen Formalisierung
Darüber hinaus sind die Forscher der Meinung, dass die extreme Knappheit hochwertiger mathematischer Datensätze ebenfalls ein Schlüsselfaktor ist, der die Verbesserung der mathematischen Schlussfolgerungsfähigkeiten großer Sprachmodelle begrenzt. Um diese Schwierigkeit zu überwinden, schlugen die Forscher ein neuro-symbolisches Framework vor, das zur automatischen Generierung hochwertiger, überwachter mathematischer Daten dient. Dieses Paradigma kombiniert die Stärken neuronaler und symbolischer Ansätze. Einerseits generiert es vielfältige mathematische Probleme durch systematische Stichproben im symbolischen Raum und nutzt symbolische Löser, um die Gültigkeit der Probleme sicherzustellen; andererseits können große Modelle die Umwandlung vom symbolischen Raum in den natürlichen Sprachraum effektiv unterstützen, um sicherzustellen, dass die neu generierten formalisierten Probleme mit ihren entsprechenden natürlichen Sprachversionen konsistent bleiben.
Neuro-symbolic data generation for math reasoning
Paper Link:
https://openreview.net/pdf?id=CIcMZGLyZW
Abbildung 4: Neuro-symbolisches Framework
Verbesserung der Generalisierungsfähigkeit des Schlussfolgerns großer Sprachmodelle – Schlussfolgern wird nutzbarer
Die Generalisierungsfähigkeit des Schlussfolgerns ist ein wichtiger Indikator dafür, ob künstliche Intelligenz wirklich universell einsetzbar ist. Modelle mit starker Generalisierungsfähigkeit können Wissensgrenzen verschiedener Bereiche überschreiten und „aus einem Fall auf andere schließen“, wodurch der Anwendungsbereich und Wert der künstlichen Intelligenz erweitert wird. Die Forscher haben festgestellt, dass nach dem Training von Modellen mit mathematischen Daten ihre Schlussfolgerungsfähigkeit in mehreren Bereichen wie Wissenschaft und Code signifikant verbessert wird. Diese Erkenntnis liefert eine neue Richtung zur Verbesserung der Generalisierungsfähigkeit des Schlussfolgerns großer Modelle.
Durch die Integration von drei Schlussfolgerungsparadigmen – natürliche Sprache, Code und symbolische Sprache – in denselben Schlussfolgerungspfad schlugen die Forscher das einheitliche Schlussfolgerungs-Framework CoR (Chain-of-Reasoning) vor. Dabei hilft die natürliche Sprache, den Kontext und die Anforderungen des Problems zu verstehen, die Codesprache ist gut für präzise Berechnungen und logische Verarbeitung, und die symbolische Sprache kann mathematische und logische Beziehungen prägnant und streng ausdrücken. CoR ermöglicht es dem Modell, zunächst basierend auf einem Paradigma zu schließen, dann flexibel zwischen Paradigmen je nach den verschiedenen Phasen und Anforderungen des Problems zu wechseln und die kollaborative Schlussfolgerung mit mehreren Paradigmen basierend auf zuvor generiertem Inhalt fortzusetzen, wodurch die Generalisierung des Schlussfolgerns bei allgemeinen mathematischen Aufgaben erreicht wird.
Zusätzlich kann das Modell durch Anpassen von Prompts die Tiefe der Schlussfolgerung und die Anzahl der verwendeten Paradigmen ändern, was seine Anpassungsfähigkeit an verschiedene Aufgaben erheblich verbessert. Bei Tests auf 5 mathematischen Schlussfolgerungs-Datensätzen erzielte CoR signifikante Verbesserungen und zeigte eine überraschende allgemeine mathematische Problemlösungsfähigkeit – es kann sowohl mathematische Berechnungsprobleme als auch mathematische Beweisprobleme lösen.
Chain-of-Reasoning: Towards unified mathematical reasoning in LLMs via a multi-paradigm perspective
Paper Link:
https://arxiv.org/pdf/2501.11110
Abbildung 5: Schlussfolgerungsprozess unter verschiedenen Paradigmen
Darüber hinaus konzentrieren sich bestehende große Modelle hauptsächlich auf die Verbesserung der Schlussfolgerungsfähigkeiten für spezifische Aufgaben oder Domänen (wie Mathematik oder Programmierung) und haben das Problem der Generalisierungsfähigkeit bei verschiedenen Schlussfolgerungsaufgaben nicht vollständig gelöst. Um die Generalisierungsfähigkeit bei Schlussfolgerungsaufgaben zu verbessern, schlagen die Forscher vor, im Aktionsraum abstrakter Pläne auf hoher Ebene zu suchen, anstatt sich auf aufgabenspezifische Aktionsräume zu beschränken, die die Generalisierungsfähigkeit normalerweise einschränken würden.
Durch die Analyse früherer Forschungen, die große Modelle zur Generierung von Schlussfolgerungsplänen und spezifischen Aufgabenlösungen nutzten, um die Schlussfolgerungsfähigkeit zu verbessern, stellten die Forscher fest, dass spezifische Aufgabenlösungen eng mit spezifischen Aufgabenfähigkeiten zusammenhängen. Im Gegensatz dazu stellen Pläne ein abstraktes Denken zur Problemlösung dar, z. B. die Entscheidung, welches Wissen anzuwenden oder wie ein Problem zu zerlegen ist, was dem Modell hilft, breitere, aufgabenunabhängige Fähigkeiten zu entwickeln und so die Generalisierungsfähigkeit zu verbessern.
Dr. Xueting Han, Principal Researcher bei Microsoft Research Asia, erklärt: „Menschen haben einige gemeinsame Strategien, wenn sie über die Problemlösung nachdenken. Zum Beispiel komplexe Probleme in Teilprobleme zerlegen, Schlüsselbereiche aus umfangreichen Informationen extrahieren sowie vorhandenes Wissen basierend auf spezifischen Informationen abrufen und nutzen, wie Theoreme in der Mathematik oder Algorithmen in der Programmierung. Durch das Erlernen dieser Problemlösungsstrategien bilden große Modelle beim Auftreten neuer Probleme ebenfalls einen ähnlichen Denkprozess wie beim menschlichen Problemlösen, wodurch Probleme effektiver gelöst werden.“
Darauf aufbauend schlugen die Forscher die Methode Critical Plan Step Learning (CPL) vor, die aus zwei Schlüsselkomponenten besteht: planbasierte Suche und Lernen kritischer Planschritte durch Step-wise Advantage Preference Optimization (Step-APO). Die planbasierte Suche nutzt die Monte-Carlo-Baumsuche, um verschiedene Planschritte bei mehrstufigen Schlussfolgerungsaufgaben zu erkunden. Durch die Erstellung eines Planbaums hilft sie dem Modell, aufgabenunabhängige Fähigkeiten zu erwerben, wodurch die Generalisierungsfähigkeit des Modells bei verschiedenen Aufgaben verbessert wird. Step-APO integriert die Vorteilsabschätzungen aus schrittweisen Präferenzpaaren, die mit der Monte-Carlo-Baumsuche erhalten wurden, sodass das Modell feinkörnige Präferenzen zwischen Schritten lernen, kritische Planschritte identifizieren und den Einfluss fehlerhafter Schritte abschwächen kann, wodurch die Gesamt-Schlussfolgerungsfähigkeit des Modells verbessert und seine Generalisierungsfähigkeit bei verschiedenen Aufgaben erhöht wird.
CPL: Critical plan step learning boosts LLM generalization in reasoning tasks
Paper Link:
https://arxiv.org/pdf/2409.08642
Abbildung 6: Schematische Darstellung von CPL
Die Grenzen der Schlussfolgerungsfähigkeit kontinuierlich erweitern und Herausforderungen großer Modelle angehen
Vom mathematischen Schlussfolgern bis zur Verbesserung der Generalisierungsfähigkeit der Schlussfolgerungen von Modellen, von intuitiven schnellen Antworten bis hin zu Antworten, die aus tiefem Denken abgeleitet sind, erforschen Forscher von Microsoft Research Asia kontinuierlich die Grenzen der Schlussfolgerungsleistung großer Modelle. Durch die Einführung neuer Perspektiven und Methoden haben sie nicht nur die Spitze dieses Feldes vorangetrieben, sondern auch dazu beigetragen, dass weitere verwandte Forschungsarbeiten neue Fortschritte erzielen. Mit der Verbesserung der Leistung und Zuverlässigkeit großer Sprachmodelle erweitert sich auch der Anwendungsbereich der künstlichen Intelligenz in realen Szenarien kontinuierlich und bietet starke technische Unterstützung für Bereiche wie intelligente Bildung, intelligente Gesundheitsversorgung und intelligente wissenschaftliche Forschung.
Allerdings müssen wir auch anerkennen, dass aktuelle große Modelle noch immer zahlreiche Herausforderungen gegenüberstehen, wie z. B. Halluzinationsprobleme bei der Inhaltserzeugung und unzureichend strenge Schlussfolgerungsprozesse. Diese Probleme können in spezifischen Anwendungsszenarien schwerwiegende Folgen haben. Zum Beispiel können Abweichungen in der Modellspezifischen Forschung zu falschen Forschungsrichtungen führen und erhebliche Ressourcenverschwendung verursachen; im Gesundheitswesen können ungenaue Informationen direkt das Leben der Patienten gefährden.
Zusätzlich zu den oben genannten Forschungen versuchen die Forscher von Microsoft Research Asia auch, die Schlussfolgerungsfähigkeiten der künstlichen Intelligenz aus vielen verschiedenen Blickwinkeln zu verbessern, darunter die Verwendung von LLMs zur automatischen Generierung von Korrektheitsbeweisen für Rust-Code, die Entwicklung von Methoden, die den einzigartigen Merkmalen des Verus-Verifizierungswerkzeugs entsprechen; die Vorschlagung des SAFE-Frameworks zur Behebung des Datenknappheitsproblems bei der formalen Verifizierung von Rust-Code; die Einführung des Alchemy-Frameworks zur Konstruktion formaler Theoreme durch Variation von Symbolen, wodurch das Problem der Datenknappheit beim neuronalen Theorembeweisen (NTP) gelindert wird, und so weiter. Diese Errungenschaften bieten weitere Möglichkeiten zur Verbesserung der Schlussfolgerungsfähigkeiten großer Sprachmodelle und liefern reiche Ideen für zukünftige Forschungsrichtungen.
Weitere verwandte Forschung:
AutoVerus: Automated proof generation for rust code
https://arxiv.org/abs/2409.13082
Automated proof generation for rust code via self-evolution
https://arxiv.org/pdf/2410.15756v1
Alchemy: Amplifying theorem-proving capability through symbolic mutation
https://arxiv.org/pdf/2410.15748
Mutual reasoning makes smaller LLMs stronger problem-solvers
https://arxiv.org/pdf/2408.06195