Gespräch mit Sheng Ying: xAI, die Romantik von Infra, SGLang, Open Source, Gleichberechtigung und "Die Legende von Zhen Huan"

Sie war ehemaliger Leiter des Inferenzteams bei xAI.

Die von ihr erforschte und initiierte quelloffene Inferenz-Engine SGLang ist zu einem wichtigen grundlegenden Werkzeug für die Bereitstellung und Inferenz zahlreicher großer Modelle geworden und gehört heute zu den einflussreichsten quelloffenen Inferenz-Frameworks im Bereich der KI-Infrastruktur.

Sie absolvierte ihren Bachelor-Abschluss im ACM-Kurs der Shanghai Jiao Tong University und erwarb anschließend nacheinander einen Master- und einen Doktorgrad in Informatik an der Columbia University und der Stanford University. Ihre Forschungserfahrung erstreckt sich über Algorithmen, formale Verifikation und große Modellsysteme.

Sie ist unser heutiger Interviewgast — Ying Sheng.

Nach dem Aufkommen der Welle großer Modelle beteiligte sich Ying Sheng als Kernmitglied der quelloffenen Gemeinschaft LMSYS an der Förderung einer Reihe von branchenweit einflussreichen Projekten.

Anschließend trat Ying Sheng xAI bei, leitete gemeinsam das Inferenzteam von Grok und brachte die quelloffene Forschung in die weltweit fortschrittlichste Ingenieurspraxis für große Modelle. Heute hat sie aus der quelloffenen Ökologie von SGLang das Startup-Unternehmen RadixArk hervorgebracht. Ihr Ziel ist es, die fortschrittliche KI-Infrastruktur, die bisher nur wenige Technologiegiganten besitzen, zu einer offenen technologischen Grundlage zu machen, die die gesamte Branche nutzen kann.

RadixArk hat bei seiner Gründung eine Seed-Finanzierung von 100 Millionen US-Dollar abgeschlossen, und die Investoren umfassen fast alle Rechenleistunggiganten und technischen Führungspersönlichkeiten im Silicon Valley.

In diesem Gespräch sprechen wir über die Schönheit der Mathematik, wissenschaftliche Arbeiten und Tiefpunkte aus der Perspektive von Ying Sheng, über SGLang, xAI und RadixArk sowie darüber, wie ein Mensch allmählich seine eigene Natur versteht und beschließt, nicht mehr dagegen anzukämpfen.

Ying Sheng sagt, dass es ihr nicht um das „Making Impact“ geht, sondern darum, dass die Dinge, die sie für richtig hält, am Ende tatsächlich stattfinden. Von der Einstellung „Die Welt hat nichts mit mir zu tun“ bis zu dem Wunsch „eine Zukunft aufzubauen, in der Menschen mit starker KI koexistieren und nicht verlieren“. Im Folgenden ist die Geschichte von Ying Sheng.

Vertragsstrafen, New York und die Schönheit der Mathematik — „Die Welt hat nichts mit mir zu tun“

Chen Xi: Vielen Dank, Ying Sheng, willkommen bei „Silicon Valley 101“.

Ying Sheng: Vielen Dank für dieses Interview.

Chen Xi: Ich sehe, dass Sie gerade erst in dieses neue Büro eingezogen sind. Wie viele Mitarbeiter haben Sie derzeit?

Ying Sheng: Ja, wir sind erst am 1. Juni eingezogen, derzeit haben wir über 40 Mitarbeiter.

Chen Xi: Wird die Expansion sehr schnell voranschreiten?

Ying Sheng: Die Größe unserer Expansion wächst schneller als erwartet. Überall fehlen Mitarbeiter, und es gibt mehr geeignete Bewerber, die wir einstellen können, als ich gedacht habe. Deshalb sind wir etwas unter Druck, aber wir kontrollieren das Wachstum bereits.

Chen Xi: Heute sprechen wir über Ihre gesamte Studienzeit, Ihre spätere Forschungsphase, Ihre Zeit bei xAI und Ihr heutiges Startup-Unternehmen.

Sie haben an der Shanghai Jiao Tong University den Ehrenkurs von ACM belegt und sind bereits 2017 an die Columbia University in den USA gegangen, um einen Master-Abschluss zu machen. Sind Sie damals ins Ausland gegangen, weil alle anderen das auch taten? Warum haben Sie diesen Weg gewählt?

Ying Sheng: Tatsächlich haben damals viele Leute vor, ins Ausland zu gehen, aber ich habe das Konzept des Auslandsaufenthalts sehr spät verstanden. Als ich von Jiangsu nach Shanghai kam, um meinen Bachelor zu absolvieren, erlebte ich einen starken Kulturschock. Die Menschen um mich herum verstanden die berufliche und persönliche Entwicklung besser, sie hatten mehr Pläne, während ich in einem Zustand der Unwissenheit war.

Ich erinnere mich, dass ich direkt nach dem Bachelor-Abschluss zunächst überhaupt keine Zulassung für eine Universität bekommen habe. Ich habe mich an Universitäten in den USA beworben, aber lange Zeit keine Zulassungsmitteilung erhalten. Damals habe ich eine Zulassung zum Doktoratsstudium an der Chinese University of Hong Kong erhalten und diese sogar bereits angenommen. Aber für Bewerbungen gab es eine ungeschriebene Vereinbarung, die bis zum 15. April galt.

Am Tag nach Ablauf dieser Vereinbarung erhielt ich plötzlich eine sehr gewöhnliche Zulassung zum Master-Studium von der Columbia University. Es war eine ganz normale Zulassung, die viele Leute bekommen konnten. Aber damals dachte ich, ich möchte etwas Neues kennenlernen, denn zu dieser Zeit lag das akademische Zentrum noch in den USA. Auch wenn das Master-Programm an der Columbia University kein besonders herausragendes Programm war, wollte ich trotzdem ins Ausland gehen und es mir ansehen. Ich habe meinen Vater angerufen und gefragt, ob ich die vorherige Zulassung zum Doktoratsstudium brechen kann, und dass ich eine Vertragsstrafe zahlen muss. Ich habe kurz gezögert, aber mein Vater hat sehr schnell geantwortet, nach weniger als einer Minute Überlegung sagte er: „Gut, geh hin.“

Chen Xi: Sie sagten, dass Sie von Jiangxi nach Shanghai einen Kulturschock erlebt haben. Haben Sie dann auch einen Kulturschock erlebt, als Sie von Shanghai in die USA gegangen sind?

Ying Sheng: Das war auch der Fall. In meinen frühen Erfahrungen wurde mein Komfortbereich in jeder Phase durchbrochen. Aber meine Gefühle in New York waren anders. New York ist eine sehr tolerante Stadt. Der Schock, den ich in New York erlebt habe, fühlte sich nicht wie ein echter Schock an. Ich spürte Unterschiede, aber ich fühlte mich sehr stark akzeptiert.

Chen Xi: Worin zeigt sich das konkret?

Ying Sheng: Die Kultur in New York ließ mich spüren, dass niemand auf mich schaut, niemand sich darum kümmert, was ich trage, was ich denke, was ich tue oder was ich will. Der Schock, den ich in New York erlebt habe, war eher der Schock, nicht beurteilt zu werden und auch keine anderen beurteilen zu müssen. Dieser Schock führte von einem eingeschränkten Zustand zu einem völlig freien Zustand. Obwohl es ein Schock war, war es eigentlich ein entspannenderer Prozess.

Chen Xi: Ich sehe, dass die Arbeiten, die Sie in Ihrer Master-Phase an der Columbia University veröffentlicht haben, eher theoretisch ausgerichtet sind und sich hauptsächlich auf die mathematischen Eigenschaften von Testfunktionen und linearer Regression konzentrieren. Später, als Sie an der Stanford University promoviert haben, haben Sie den Bereich der formalen Verifikation gewählt. Können Sie uns zunächst sagen, ob diese Forschungen, die Sie an der Columbia University betrieben haben, Auswirkungen auf Ihre späteren Forschungen hatten?

Ying Sheng: Als ich gerade mit dem Master-Studium angefangen habe, wollte ich gar nicht forschen. Aber im ersten Semester habe ich einen Kurs über Komplexitätstheorie besucht, der mir sehr interessant erschien. (Anmerkung: Die Theorie der Berechnungskomplexität ist ein Teilgebiet der theoretischen Informatik und der Mathematik, das berechenbare Probleme nach ihrer eigenen Komplexität klassifiziert und diese Kategorien miteinander verknüpft.) Ich habe zufällig einige Doktorandenfreunde kennengelernt, die alle in der Theorie forschten. Ich fand dieses Gebiet sehr interessant, also habe ich Professoren und diese Mitschüler gefragt, ob es Probleme gibt, an denen ich forschen kann. Nach einer Weile der Forschung fand ich es sehr spannend und erzielte Ergebnisse, also bin ich ganz natürlich zur Stanford University gekommen.

Chen Xi: Haben Sie nach dem Abschluss des Master-Studiums überlegt, zu arbeiten oder sich für ein Doktoratsstudium zu bewerben?

Ying Sheng: Anfangs wollte ich mich nicht für ein Doktoratsstudium bewerben, oder genauer gesagt, ich war nicht der Meinung, dass ich mich nicht bewerben würde, aber ich habe dieses Ziel nicht fest im Blick gehabt. Ich fand die Situation offen, also habe ich diese Option behalten und ein bisschen erkundet. Später fand ich die theoretischen Probleme sehr interessant und habe sie sehr genossen. Damals dachte ich, dass ich nicht einmal viel Geld verdienen muss, ich möchte arm bleiben (stay poor) und einen Ort finden, an dem niemand ist. Einmal bin ich zu einem Workshop in Princeton gegangen und war direkt von dieser Umgebung umgeben. Als ich den Campus von Princeton betrat, spürte ich plötzlich, dass ich von der Welt abgetrennt bin und keine Sorgen habe.

Chen Xi: Sehr akademisch, anders als an der Columbia University.

Ying Sheng: Es ist nicht nur akademisch, es ist einfach so, dass man von der Welt abgetrennt ist und keine Sorgen hat. Das Gefühl, wenn man dort hineingeht, ist, dass viele Dinge, die die Menschen um einen herum schätzen und für die man normalerweise kämpft, völlig bedeutungslos sind — das war mein damaliges Gefühl.

Chen Xi: Haben Sie dieses Gefühl durch die Umgebung der Universität bekommen, oder durch die Atmosphäre der Menschen dort?

Ying Sheng: Es war wahrscheinlich der Workshop selbst, der diese Atmosphäre geschaffen hat: die Umgebung und die Diskussionsatmosphäre der Leute im Workshop. Diese Atmosphäre ließ mich spüren, dass alle Dinge unwichtig sind, die Gedanken und Emotionen der Menschen unwichtig sind, und das erscheint sogar ein bisschen absurd.

Chen Xi: Was ist dann wichtig?

Ying Sheng: Dass nichts wichtig ist, das ist das Wichtige. Das ist eine Art von Nihilismus. Man hat das Gefühl, dass Nichts das Wahre ist, und nur das Wahre ist wichtig.

Unter dieser Umgebung erscheint Mathematik besonders schön und elegant, weil sie deterministisch und absolut ist. Wenn man sich mit ihr befasst, muss man über nichts anderes nachdenken. Sie lässt einen sehr eintauchen und konzentrieren, oder man kann in dieser Umgebung in einen Flow-Zustand geraten. Dieser Flow-Zustand hat nichts mit Menschen zu tun und nichts mit anderen Dingen. Wenn das Gehirn vollständig aktiviert ist, gerät man in einen physiologischen Zustand der Freude, den ich kaum beschreiben kann.

Chen Xi: Ich kann verstehen, was Sie meinen. Dieser Zustand ist sehr rein, ähnlich dem Zustand einer Person, die Mathematiker werden könnte. Warum sind Sie dann später nicht Mathematiker geworden?

Ying Sheng: Damals wollte ich unbedingt Mathematiker werden, ich dachte, ich will nur Mathematik machen. Aber die Entwicklung der Dinge ist nie so einfach, schließlich gab es alle möglichen Störungen im Leben. Im ersten Jahr an der Stanford University hatte ich dieses Gefühl dann nicht mehr.

Chen Xi: Glauben Sie, dass die Stanford University nicht so rein ist wie Princeton?

Ying Sheng: Der Besuch in Princeton war nur eine Reise. Ich war an der Columbia University, aber auch dort konnte ich diese Atmosphäre spüren. Ich habe sogar das Gefühl, dass es zwischen der Westküste und der Ostküste gewisse kulturelle Unterschiede gibt. An der Westküste spürt man allmählich mehr Lärm über Erfolg oder Misserfolg, man will die Welt vorantreiben. Ich begann wieder zu denken, dass ich etwas mit der Welt zu tun habe, ich wollte nicht mehr von der Welt abgetrennt sein. Aber als ich an der Ostküste war, wollte ich nichts mit der Welt zu tun haben, wollte von der Welt vergessen werden — das ist ein ganz anderes Gefühl.

In meinem ersten Jahr an der Stanford University wollte ich Theorie forschen. Damals gab es an der Stanford University das PhD-Rotationsprogramm, bei dem man einen Betreuer zugewiesen bekommt, bevor man entscheidet, wie die nächsten fünf Jahre des Doktoratsstudiums verlaufen.

In den ersten Runden habe ich aus verschiedenen komplexen Gründen kein Problem gefunden, das mich in den Flow-Zustand versetzt hat, und es gab auch keinen Professor, mit dem wir beide gegenseitig sehr begeistert voneinander waren. Vielleicht dachten die Professoren auch, dass ich nicht sehr an ihren Problemen interessiert bin, und manchmal dachte ich, dass der Professor nicht ganz zu mir passt. Als ich in der vierten Runde endlich zu meinem späteren Betreuer Clark Barrett passte, war ich bereits in ein neues Forschungsfeld eingetreten.

Professor Clark Barrett forscht auf dem Gebiet der formalen Verifikation. Dieses Gebiet ist sehr groß, ich kann kurz den Teil der Forschung beschreiben, an dem ich damals gearbeitet habe. (Anmerkung: Formale Verifikation ist eine Technik, die mit mathematischen Methoden die Korrektheit von Computersystemen beweist. Ihr Kern umfasst Modellprüfung, Theorembeweiser und Äquivalenzprüfung. Sie hängt nicht von zufälligen Tests ab und kann logische Fehler grundsätzlich ausschließen.)

Unser damaliges Forschungsprojekt bestand darin, den von Menschen geschriebenen Code zu zerlegen und auf die zugrundeliegende mathematische Logik abzubilden. Man kann Code in Prädikatenlogik erster Stufe abbilden. Sobald die Logik vorliegt, kann man aus mathematischer Sicht beweisen, ob der von Ihnen geschriebene Code eine bestimmte Eigenschaft hat.

Genauer gesagt haben wir etwas namens Spec, also Spezifikation. (Anmerkung: Die Spezifikation (kurz Spec) in der formalen Verifikation ist ein strenges mathematisches Logiksprache, das das erwartete Verhalten eines Computersystems oder von Software und Hardware eindeutig beschreibt, was es tun soll und was nicht.) Spec beschreibt, welche Vorbedingungen der Code erfüllen muss, welche Invarianten er hat und welche Bedingungen erfüllt sein müssen, nachdem der Code ausgeführt wurde. Man kann eine solche Sprache verwenden, um das Programm zu beschreiben. Das, was man beweisen will, ist, ob der Code wirklich dieser Logik entspricht, wenn es diese Spec gibt. Nachdem der Code in logische Formeln abgebildet wurde, ist das Beweisen und Schlussfolgern zwischen den Formeln genau das, was der SMT-Solver (SMT-Löser) in meinem Forschungsfeld tut.

Der größte Teil meiner Forschung konzentriert sich auf die Optimierung des SMT-Solvers selbst. Diese Optimierung hängt einerseits mit der Effizienz zusammen, andererseits mit der Korrektheit, aber vor allem damit, wie man Semantik definiert — also welchen semantischen Raum man definiert, um die Dinge auszudrücken, die ein Code tut.

Chen Xi: Kann man das einfach so verstehen, dass man Rechenprobleme mit mathematischen Methoden beweist?

Ying Sheng: Ich denke, das kann man so sagen.

Chen Xi: Nachdem Sie an der Stanford University tief in die formale Verifikation eingestiegen sind, haben Sie gesehen, dass Sie ständig wissenschaftliche Arbeiten veröffentlicht haben. 2020 haben Sie den Best Paper Award der IJCAR (International Joint Conference on Automated Reasoning) erhalten, 2022 wurden Sie für die IJCAR nominiert und später als einer der Mitwirkenden von cvc5 den Best Tool Paper Award der TACAS gewonnen. Sie sind sehr produktiv. Wie war Ihr Forschungsz