Euler: menschzentrierte Multi-Agenten-Mathematik

Hintergrund

Die meisten aktuellen Arbeiten zu KI für Mathematik zielen auf eine einzige Größe: die Endantwort. Sprachmodell-Agenten lösen inzwischen anspruchsvolle Aufgaben und verfassen recht lange Beweise. Die Arbeit zu Euler benennt zwei Probleme dieser Ausrichtung. Erstens können Forschende kaum nachvollziehen, wie ein Ergebnis entstanden ist. Sie sehen die Schlussfolgerung, aber nicht die Abwägungen und verworfenen Ideen auf dem Weg dorthin.

Zweitens zerfällt bei langen Forschungsläufen der Kontext. Eine unbelegte Behauptung, die einmal in eine Argumentationskette gelangt, wird in späteren Schritten immer wieder zitiert. Ihre Quelle lässt sich dann nur schwer finden. Euler ist ein menschzentriertes System für mathematische Forschung. Sein Kernbeitrag ist eine gemeinsame, strukturierte Darstellung des Forschungsprozesses selbst, den das System als nachverfolgbares, wiederverwendbares und prüfbares Objekt behandelt.

Die Arbeit stützt sich auf drei mathematische Fallstudien und beschreibt das implementierte System samt Softwareverifikation. Quantitative Benchmark-Ergebnisse nennt die Zusammenfassung nicht. Dieser Beitrag macht deshalb keine Aussagen über Punktzahlen oder Geschwindigkeitsgewinne.

Tiefenanalyse

Das technische Herzstück ist der Forschungsgraph. Er verbindet mathematische Aussagen, Annahmen, Beweisabhängigkeiten, alternative Ideen, gescheiterte Versuche und Verifikationsbelege. Auffällig ist eine Entwurfsentscheidung: Gescheiterte Versuche und Alternativen bleiben Teil des Graphen und verschwinden nicht aus dem fertigen Text. Wer dem Graphen folgt, sieht, wie eine Schlussfolgerung gewachsen ist und auf welchen Prämissen sie ruht. Für die Agenten ist der Graph eine dauerhafte Quelle aufgabenrelevanten Wissens. Bei Planung, Zusammenarbeit und Verifikation holt ein Agent nur den Teil, den die aktuelle Aufgabe braucht. Er muss nicht die gesamte Historie im Kontextfenster mitführen. So bleiben Fäden über Sitzungen hinweg erhalten. Da Abhängigkeiten und Verifikationsbelege an den Knoten hängen, wird die Frage, ob eine Behauptung Rückhalt hat, nachschlagbar. Das richtet sich direkt gegen die Ausbreitung unbelegter Aussagen zwischen Denkschritten.

Hinzu kommt die Interaktion. Forschende wählen einen Knoten, der mit einem gespeicherten Teamzustand verknüpft ist, lesen das frühere Denken der Agenten nach und erkunden durch weitere Interaktion eine andere Richtung, ohne von vorn zu beginnen. So bleibt der Mensch im Entscheidungskreis. Die Auswertung ist beschreibend. Die Fallstudien zeigen, wie der Graph beim Erkunden wächst, wie gescheiterte Pfade erhalten bleiben und wie Forschende ab einem gewählten Knoten fortfahren. Die Softwareverifikation prüft, ob die Systemteile wie entworfen arbeiten. Das belegt die Tragfähigkeit eines Forschungsablaufs, nicht den Rang in einer Bestenliste.

Branchenwirkung

Euler verschiebt den Schwerpunkt von der Frage, ob die Antwort stimmt, hin zur Frage, ob der Prozess verständlich und wiederverwendbar ist. Das passt zur Arbeitsweise der Mathematik. Ein Satz besitzt Wert durch sein Ergebnis, aber auch durch die Struktur des Beweises, die erprobten Sackgassen und die Abhängigkeiten zwischen den Schritten. Werden diese Elemente explizit gespeichert, kann ein KI-System zum Gesprächspartner werden statt zur Black Box.

Für Teams, die Multi-Agenten-Systeme bauen, bietet der Forschungsgraph ein Muster für langlaufende Aufgaben: Ein strukturierter externer Speicher ersetzt einen ständig wachsenden Kontext, und Agenten knüpfen in einer neuen Sitzung an frühere Arbeit an. Die Zusammenfassung beschreibt das System nur im mathematischen Umfeld. Das Muster könnte auch bei formaler Verifikation oder Code-Review passen. Diese Übertragung ist eine Schlussfolgerung und kein Ergebnis der Arbeit.

Ausblick

Die bisherige Evidenz stammt aus Fallstudien und technischer Verifikation. Ob der Graph die Ausbreitung unbelegter Behauptungen tatsächlich bremst und lange Forschungsläufe erleichtert, braucht kontrollierte Vergleiche. Nutzerstudien mit arbeitenden Mathematikerinnen und unabhängige Reproduktionen würden den Befund stützen. Da keine quantitativen Ergebnisse genannt werden, ist der Nutzen als plausibel und an Beispielen gezeigt zu verstehen, nicht als gemessen.

Aus dem Entwurf ergeben sich offene Fragen. Wie lässt sich die Graphstruktur werkzeugübergreifend standardisieren? Wie werden Verifikationsbelege an formale Beweisassistenten angebunden? Wie geht das Zurückspielen gespeicherter Teamzustände mit Meinungsverschiedenheiten um, wenn mehrere Forschende zusammenarbeiten? Die Antworten entscheiden, ob der Forschungsgraph zur gemeinsamen Schnittstelle für Mensch-KI-Mathematik wird oder ein Merkmal eines einzelnen Systems bleibt.