Conversation with Sheng Ying: xAI, the romance of Infra, SGLang, open source, equal rights and "Empresses in the Palace"

She is the former head of the inference team at xAI.

The open-source inference engine SGLang, which she researched and initiated, has become a critical underlying tool for the deployment and inference of numerous large models, and is also one of the most influential open-source inference frameworks in the current AI infra field.

She graduated from the ACM Honors Program at Shanghai Jiao Tong University for her bachelor's degree, and later obtained her master's and doctorate degrees in computer science at Columbia University and Stanford University respectively. Her research experience spans algorithms, formal verification, and large model systems.

She is our guest in this interview — Sheng Ying.

After the wave of large models emerged, as a core member of the LMSYS open-source community, Sheng Ying participated in promoting a series of industry-influential projects.

Later, Sheng Ying joined xAI to co-lead Grok's inference team, bringing open-source research into the world's most cutting-edge large model engineering practice. Today, she has spun out the startup company RadixArk from the SGLang open-source ecosystem, hoping to turn the cutting-edge AI infrastructure that only a few tech giants could access into an open technology base available to the entire industry.

RadixArk completed a $100 million seed round of financing at its inception, with investors covering almost all the computing power giants and tech leaders in Silicon Valley.

In this conversation, we talked about the beauty of mathematics, academic papers and low points in Sheng Ying's eyes, SGLang, xAI and RadixArk, and also discussed how a person gradually understands their own nature and decides not to fight against it anymore.

Sheng Ying said that what she cares about is not "making impact", but whether those things she thinks are right have finally happened. From "the world has nothing to do with me" to "wanting to build a future where humans coexist with powerful AI without losing". Below is Sheng Ying's story.

Penalty, New York and the Beauty of Mathematics: "The World Has Nothing to Do With Me"

Chen Xi: Thank you so much Sheng Ying, welcome to "Silicon Valley 101".

Sheng Ying: Thank you for the interview.

Chen Xi: I see you just moved into this new office, how many people do you have here now?

Sheng Ying: Yes, we just moved in on June 1st, and now we have more than 40 people.

Chen Xi: Will the expansion be very rapid?

Sheng Ying: Our expansion is growing faster than we expected. We need people everywhere, and there are more qualified candidates coming in than I thought, so we are a little bit under pressure, but we are already controlling the pace.

Chen Xi: Today we will talk about your entire student days, your later research period, your time at xAI, and your current startup company.

You attended the ACM Honors Program at Shanghai Jiao Tong University, and came to Columbia University in the United States to pursue a master's degree in 2017. Did you go abroad at that time because everyone else was going abroad? Why did you choose this path?

Sheng Ying: It's true that many people were going abroad at that time, but I actually knew very little about the idea of going abroad until very late. When I came from Jiangxi to Shanghai for my undergraduate studies, I experienced a strong cultural shock. People around me had a better understanding of career and life development, and they had more plans, while I was in a state of ignorance.

I remember when I first graduated from undergraduate, I didn't even get into any schools at first. I applied to universities in the United States, but I didn't receive an admission offer for a long time. At that time, I got an admission offer for a PhD at the Chinese University of Hong Kong, and I even accepted it. But there was a gentleman's agreement for applications, with a deadline of April 15th.

The day after the gentleman's agreement expired, I suddenly received a very ordinary master's admission offer from Columbia University. It was actually a very ordinary offer that many people could get. But at that time I felt I wanted to get in touch with new things, because the academic center at that time was still in the United States. Even though this master's program at Columbia was not a top-tier program, I still wanted to go out and see. I called my dad at that time and asked if I could break the contract with the previous PhD offer, and I would have to pay a penalty. I hesitated for a moment, but my dad answered very quickly, thinking for less than a minute and saying: "Okay, go."

Chen Xi: You said you experienced a cultural shock when you came from Jiangxi to Shanghai. So did you also experience a cultural shock when you went from Shanghai to the United States?

Sheng Ying: Yes, I did. In my early experiences, every stage broke my comfort zone. But my feeling in New York was different. New York is a very inclusive city. The shock I felt when I went to New York was not really like a shock. I felt different, but I felt extremely accepted.

Chen Xi: What specific aspects does this reflect in?

Sheng Ying: The culture of New York at that time made me feel that no one was staring at me, no one cared what I wore, what I thought, what I did, or what I wanted. The shock I felt in New York was more like a shock of not needing to be judged, and not needing to judge others. This shock was from a restricted state to a completely free state. Although it was a shock, it was actually a more relaxing process.

Chen Xi: I see that the papers you published during your master's studies at Columbia were more theoretical, mainly about the mathematical properties of test functions and linear regression. Later, when you went to Stanford for your PhD, you chose the direction of formal verification. Could you first tell us if the research you did at Columbia had any impact on your later research?

Sheng Ying: I didn't want to do research when I first started graduate school. But in the first semester, I took a course on computational complexity, which I found very interesting. (Note: Computational complexity theory: a branch of theoretical computer science and mathematics, which is dedicated to classifying computable problems according to their inherent complexity and establishing connections between these categories.) I also happened to make some friends who were PhD students at that time, and they were all doing theory. I thought this field was very interesting, so I went to ask teachers and these classmates if there were any problems I could study. After researching for a period of time, I found it very interesting and got results, so I naturally went to Stanford.

Chen Xi: When you graduated from graduate school, did you consider going to work or applying for a PhD?

Sheng Ying: I didn't want to apply for a PhD at first, or I didn't think I wouldn't apply for a PhD, but I didn't focus on this goal. I thought it was open, so I kept this option and explored it. Later, I found that theoretical problems were very interesting, and I enjoyed them very much. At that time, I felt that I didn't even need to make a lot of money. I wanted to stay poor and find a place where no one was around. I once went to Princeton to attend a workshop, and I was completely surrounded by that environment. When I walked into the campus environment of Princeton, I suddenly felt detached from the world.

Chen Xi: Very academic, different from Columbia.

Sheng Ying: It's not just academic, it's just detached from the world. The feeling when you walk in there is that many things that everyone cares about in the world, and the things you usually struggle with, are completely meaningless, that's how I felt at the time.

Chen Xi: Was it the school environment that gave you this feeling, or the atmosphere of the people there?

Sheng Ying: It should be the workshop that brought me this feeling. The environment plus the atmosphere of the people discussing in the workshop. That atmosphere made me feel that everything is unimportant, human thoughts and emotions are unimportant, and it even seems a bit absurd.

Chen Xi: Then what is important?

Sheng Ying: What's important is that nothing is important. This is a kind of nihility. You feel that nihility is the real thing, and only the truth is important.

Mathematics at that time seemed particularly beautiful and elegant, because it is deterministic and absolute. When you deal with it, you don't need to think about anything else. It allows you to be fully immersed and focused, or you can enter a state of flow in this environment. This state of flow has nothing to do with people, and nothing to do with everything else. When your brain is fully mobilized, you enter a state of physical pleasure, which I can hardly describe.

Chen Xi: I can understand what you mean, but I think this state is very pure, very similar to the state of someone who will become a mathematician. But why didn't you become a mathematician later?

Sheng Ying: At that time, I really wanted to be a mathematician, and I felt that I only wanted to do mathematics. But the development of things is never that simple. After all, I still have all kinds of disturbances in my life. In my first year at Stanford, I lost that feeling.

Chen Xi: Do you think Stanford is less pure than Princeton?

Sheng Ying: That time in Princeton was just a trip. I was at Columbia, but I could also feel that atmosphere when I was there. I even wonder now if there is this cultural difference between the West Coast and the East Coast. On the West Coast, you will gradually feel more noise about success or failure. You want to participate in the advancement of the world, and I start to feel that I am related to the world again, and I don't want to be irrelevant to the world anymore. But when I was on the East Coast, I hoped I had nothing to do with the world and wanted to be forgotten by the world. That's a very different feeling.

In my first year at Stanford, I wanted to do theory. At that time, Stanford had a PhD rotation program, where you had to match with a supervisor, and after matching, you would decide how your 5-year PhD journey would go.

For various complicated reasons in the first few rounds, I didn't encounter any problems that could make me enter a state of flow, and I didn't find any teacher who was equally excited with me. Maybe the teachers also felt that I was not particularly interested in their problems, and sometimes I also felt that the teacher didn't fully match me. When I got to the fourth round and matched with my later supervisor Clark Barrett, I had already entered a new topic.

Professor Clark Barrett works in the field of formal verification, which is a very broad field. I can briefly talk about the part of the topic I was working on at that time. (Note: Formal Verification: a technique that uses mathematical methods to prove the correctness of computer systems. Its core includes model checking, theorem proving, and equivalence checking. It does not rely on random testing and can fundamentally eliminate logical loopholes.)

Our topic at that time was to disassemble and map the code written by humans to the underlying mathematical logic. You can map the code to first-order logic. Once the logic is generated, you can prove from a mathematical perspective whether the code you write has a certain property.

More specifically, we have something called Spec, which is specification. (Note: The specification (abbreviated as Spec) in formal verification refers to using strict mathematical logic language to unambiguously describe the expected behavior standards of what a computer system or software and hardware should do and should not do.) Spec explains what preconditions the code should meet, what kind of invariant it will have, and what conditions should be met after the code is executed. You can have such a set of language to describe the program. What you need to prove is whether your code really conforms to such a set of logic under the condition of this Spec. After mapping the code to the logical formula, the proof and reasoning between the formulas is what my research field SMT solver (Satisfiability Modulo Theories solver) does.

Most of my research is on the optimization of the SMT solver itself. This optimization is related to efficiency on the one hand, and correctness on the other, but it is more related to how you define semantics, that is, what kind of semantic space you define to express what a piece of code does.

Chen Xi: Can it be simply understood as using mathematical methods to prove computational problems?

Sheng Ying: I think that's a valid way to put it.

Chen Xi: After you started to delve into formal verification at Stanford, we saw that you started publishing papers non-stop. You won the Best Paper Award at IJCAR (International Joint Conference on Automated Reasoning) in 2020, got nominated for IJCAR in 2022, and later won the Best Tool Paper Award at TACAS as one of the contributors to cvc5. You are extremely productive. What was your research state during this period?

Sheng Ying: Actually, the real process is much emptier and more boring than what you see on the resume on the surface. My first few years at Stanford were not smooth. First of all, finding a supervisor in my first year was not smooth, I was passively led into the field of formal verification. Because I wanted to pursue a PhD, I needed to keep doing research and producing papers in this field, so I was in a relatively passive state. Of course, in the process of doing it, I gradually appreciated its beauty, gradually understood why this thing is interesting, and later had more thoughts. I think it actually has a very interesting future.

But when I first worked on the politeness paper, the one that won me the IJCAR Best Paper Award for the first time, I was completely taken by surprise. Because I was in a completely novice state at that time, I didn't know much about this field. My supervisor gave me a problem, and I just went to solve it. When I finished it, I had no idea what a top paper in this field was like, because I hadn't read enough papers. So when the award came out, I had no idea at all, I only knew I won it when others congratulated me.

That was the first paper I published in this field. But after it was published, I fell back into a low state again, and still couldn't find the next exciting problem I wanted to work on. After that paper was finished, I remember that for a period of time, the pandemic started. During the pandemic, I didn't do anything for almost a year, and I was in a low state for nearly a year.

But I had a very good supervisor, Clark was very supportive of me. He told me at that time that he fully understood me, and he only cared about whether I was in a good mental state and whether I could get out of it. He didn't put any pressure on me to continue producing papers or doing research. He said I could take some courses, be a teaching assistant, and do some very lightweight things. I also went back to China for half a year during that period, which was a healing period. I didn't produce any papers, but Clark never cut off my funding. He is really a very good supervisor.

It took me