SkyDiscover — Weaviate Podcast 147

Author: Weaviate vector database · Watch on YouTube

Video authored by the channel shown, not by IANIA; all rights belong to the creator. Transcript and summary generated automatically; the original-language content is preserved.

Original language: English

Original video: SkyDiscover — Weaviate Podcast 147 · Channel: Weaviate vector database · 52:22 · Watch on YouTube

Topics: AI agents, AI evaluation and benchmarks, Data, databases and embeddings, Software engineering with AI

Summary

The SkyDiscover team discusses using AI agents to synthesize and optimize complete software systems, moving beyond code completion and individual functions. Their goal is to build systems tailored to specific workloads while addressing the central challenge of ensuring correctness through domain-aware specifications, rigorous tests, and formal verification. The conversation uses key-value stores to explore workload specialization, performance gains, and the trade-offs between building from scratch and adapting existing software. The team also considers how these methods could extend to managed infrastructure and user-facing software, and explains why evaluating and optimizing systems remains a difficult research problem.

Key points

SkyDiscover aims to use AI agents to build or optimize entire systems, such as databases and inference engines, rather than only generating code snippets.
Systems tailored to a user’s workload could avoid the generality tax of software designed for many use cases.
A database’s design can depend on workload patterns, consistency and reliability requirements, available resources, and whether the priority is latency or throughput.
The team reports up to four times better performance for specialized key-value store workloads compared with existing systems.
A key challenge is preventing reward hacking, where an agent exploits gaps in requirements or benchmarks instead of building a genuinely useful system.
SkyDiscover’s approach uses domain-aware questions to clarify requirements, then relies on test-driven development or formal specification and verification.
The choice of programming language and implementation level depends on the system’s requirements, including performance and memory safety.
Building from scratch can sometimes outperform modifying an existing system, which may constrain the agent to its existing abstractions.
Future applications could include hosted systems that adapt to changing traffic and user-facing products, though specifying human preferences is difficult.
System optimization is constrained by the cost of evaluation and by trade-offs among metrics such as memory use, throughput, and latency.

Chapters

Start	Chapter	Summary
00:01	Meet the SkyDiscover team	The guests introduce their research backgrounds in distributed systems, networking, machine-learning systems, and formal methods.
03:06	From code generation to system synthesis	The team explains why building production-ready systems is more complex than generating lines of code or individual functions.
08:19	Specializing databases for workloads	Using key-value stores as an example, the guests describe how workload patterns and requirements can guide specialized designs.
12:26	What is the artifact, and can it be trusted?	The discussion considers whether synthesized software becomes a workload-specific function and why verification is essential.
15:00	Defining requirements and avoiding reward hacking	The guests explain how users specify environments, reliability, consistency, and performance goals, and how agents can exploit vague benchmarks.
23:16	Testing, verification, and language choices	The conversation covers tests tied to specifications, formal verification, and choosing implementation languages to balance safety and performance.
30:27	From existing systems to custom implementations	The team discusses low-level code generation and when starting from scratch may outperform adapting an existing system.
38:09	Managed infrastructure and user-facing software	The guests consider how synthesis might fit hosted services and why specifying products such as note-taking apps is harder than specifying machine systems.
45:25	The challenges of system optimization	The team describes the difficulty of identifying optimization targets, running costly evaluations, and balancing competing system metrics.
49:04	Evolving tests and closing remarks	The guests discuss adapting specifications and tests over time before wrapping up the conversation.

Quotes

open source repo comes with something we call generality tax — 06:46

the remaining problem is can you trust the system that we’ve built? — 14:29

the optimization pressure is something that leads to reward hacking — 22:43

you have to skate to where the puck is going, not where it is. — 38:09

80 to 90% of the time is pending evaluations. — 48:02

Concepts and entities

SkyDiscover, SkySynth, key-value store, RocksDB, Redis, YCSB, Lean, Rust, Geppa, Ion Stoica, Weaviate

Full transcript (original language)

00:01 [music] [music] [music] [music]

00:32 [music] >> Alex Mert, Shoe, Shoven. Welcome to the We View podcast. Thank you so much for joining. >> Thank you so much. Yes. >> Thanks for hosting us. >> Yeah, thanks. >> Awesome. Well, we’ve got a packed house. I think the work behind Sky Discover is just super captivating. I’m so excited to dive into the story. Maybe especially because we have sort of a a big panel here. Do you mind each maybe giving a little bit of your background and how you came to be working on Sky Discover? >> Um Okay, maybe I can get started.

01:02 Um hello. My name is Shoe. I’m currently a 5th year PhD student at Sky Computing Lab advised by Ion Stoica. And then my work has been focusing on previously mostly about like distributed systems, storage systems, and recently moving towards more of like AI systems and like how AI can solve this like complicated more and more complicated like systems task. Yeah. >> And I maybe I’ll go next. I’m also a 5th year. I’m Alex Krenzler. I’m a a 5th year advised by Sylvia Ratnasamy.

01:32 But I work pretty closely with Scott Shenker and Ion Stoica. I kind of come from core networking and core network systems, global scale internet control systems, and internet architecture. But especially the last year I’ve shifted into AI driven discovery and and now with the Sky Discover team into AI driven synthesis. >> Okay. Um all right. I I’m Mert. I’m a 4th year PhD student at UC Berkeley EECS. I’m co-advised by Ion Stoica, Alex Tamarkin, and Kanan Ramachandran.

02:04 My work is on ML systems and particularly like these test time scaling algorithms. How can we make them faster, more efficient, um but also more performant. So by ways of either like making the accelerating like this speculative decoding like methods or um making them more performant with these evolutionary algorithms and like we have at Sky Discover. Um yeah, pretty excited to be here. Thanks for hosting us.

02:34 >> Hey, um I’m Shubham. I’m a second year PhD student, just turned second year. And yeah, I’ve been working on machine learning systems as well and recently more focused on using agents for building systems and also in the area of using like formal techniques and things like that to actually guarantee that the systems built are practically useful. Yeah, pretty excited to be here. >> Yeah, amazing. I mean, I I’ve started seeing a bit about this evolution into AI building systems coming out of Berkeley. I think like probably the cat’s out of the bag. Everyone knows AI can code really well. We’ve had

03:06 SWE-bench and all these different coding tasks, but this evolution into building entire systems, I think it’s just such an amazing concept. You might maybe now like setting the stage on maybe just what does it mean for AI to build systems? >> I think we’ve seen this transition where the very earliest AI systems, you think back to Copilot, were like just trying to auto complete, complete your lines. And even that was pretty magical. You would start typing and it would figure out, okay, here’s the remainder of the variable you’re trying to assign or whatever. Um and then we got a little bit further

03:37 along and you’d have a comment and it would synthesize a function. Um and then I think the last year or two, especially maybe starting with Claude Code, uh was it last February, was it? A year and a half ago. Um we started to see what could happen if you exposed like files and a file level view of light coding. But I think even then people still were going to uh these like coding systems and say, “Hey, help me um help me build out a particular function or particular piece of functionality.”

04:07 Um I think the Sky is Covered team, we were really looking at this as you can tell we all are really coming from assistant backgrounds um and you get this difference where there’s a big difference between a piece of code, an algorithm and and a a a system. In a system you start to kind of reason about how you manage complexity uh by putting it into kind of layers of abstraction. And you want to do this because systems are not kind of a static thing. You design a system to be scalable, to be extensible, to be interpretable, um to be kind of able to

04:39 run in production. And it’s it’s kind of an order of more complexity kind of reasoning about a task like that. Um but we were looking at where these coding systems were headed and we’re kind of thinking and following that line and going watching it go from line completion to functions to file level. And so we were really inspired by the thought of these things that today take kind of PhD level expertise to go build um a database, a inference engine, a KV store. Um if we were to really like trace out where these things are headed, what would it look like to go and um optimize

05:11 existing systems of that that kind of complexity or synthesize uh systems to that scale. Um um yeah. That’s a little bit of how we’re thinking about it. >> Yeah. And uh I would just like to add on like for example since last year like at the very beginning of like this model this models are coming out, we’re seeing this models solving more and more complicated let’s say like math task and very simple coding task. And now like as people are starting to use all of these coding agents more and more often and then these coding agents are powerful in

05:42 generating like thousands of lines of code, we’re thinking about okay like what about daily software? Like let’s say the databases that we use, the storage systems that we build, or even like the inference that the post running stack that people are particularly optimizing for their own requirements and workloads. How can AI automate that and optimizing that entire stack according to my requirements? And how can we trust like whatever AI is generated, like you can always see like those agents are generating a bunch of tasks and say like okay, agents passed like 3 100 out of 300 tasks, but is it really that trustworthy? So when AI are

06:14 like expanding, you can use like multi agents and everything to scale up the amount of code that you generate, um how do you actually like make sure that it’s actually performance and actually work as you expect it. Yeah. So that’s why we shifted from a little bit. So when we started Sky Discover, we started about like optimizing like algorithms, optimizing let’s say scheduling algorithms, like congestion control, etc. Some of the systems problems that we have and moving more towards uh like end-to-end software stack and look at like what are the challenges out there. Yeah.

06:46 >> Yeah, I mean one one one comment to add there is like in fact in our in our work we one focus that we had seen is this thing called just-in-time system. So imagine that you you now are basically capable of building whatever you used to use from some open source uh repo, but of course the open source repo comes with something we call generality tax, which is basically that you are you are using something that has been built for hundreds of use cases, but maybe you know your use case well. You know your work workload well. In fact like very very like in couple of days we might be

07:17 able to show you something more where we are thinking that the inference engines that that we build for on-device things, in fact Mert is leading one of them where we are seeing that if you make your inference engine for a very specific Mac metal uh machine and for a model and a workload, you can do a lot of optimizations that you would not be able to do because you are you were doing things for a general setup. And that that gives you that unlocking power, but because you’re using agents now, it’s very, very brittle. There are like hundreds of hacks agents do and there are a lot of things that agents will

07:47 just find ways to break things and exploit the gaps that we see on the requirement side and on the model side, which is like the world where the final thing is going to deploy. So, given those gaps, the SkySynth project is some sort of a uh our angle to tackle that where we are trying to make sure that the agents do the right work and don’t try to exploit the gap which are already there in any software system. >> Yeah, so I guess if I can maybe start

08:19 applying this sort of some really interesting ideas in this but if I can start applying maybe from a sort of selfish angle sort of from the perspective of Weaviate and our vector databases, we make a lot of this argument of, you know, we have a specialized vector database. It’s a data database that’s customized to, you know, vector search and vector storage from, you know, how you implement like a custom LSM to the custom indexes. And so I guess and and um you know, we had a podcast with Andy Pavlov from Carnegie Mellon who’s well-known database professor who had who was explaining this division of self-driving

08:49 databases. And I always imagine it sort of is like hyper parameters, you know, say like with the HNSW vector index, you have like the EF parameter max, you know, like these little index tuning parameters and or you could have like how often the LSM is going to compact or, you know, how your replication is configured. So, I guess I’m just curious about if we can maybe start on the database example. I know the paper describes like a customized key-value store and maybe just I’d love to understand how SkySynth could create a database for a specialized workload and

09:21 what you think the future is of tailor-made database systems. >> So, um I think that’s a very good uh question that I have. So, we started working on key-value store uh mainly because like key-value store has many, many diverse different kinds of properties. So, you can think about it as like, okay, like how many requests do you have? And And in this request, like how many are read requests and how many are write requests? And then, uh among these uh requirements of like building a key-value store, like what are What is your amount of resources that is

09:51 available? Are you building like a single-machine key-value store? Or are you building it in a distributed setup that you need to manage the consistency and stuff? Um so, and also what is your consistency requirements? Like, when you uh actually get back your uh like the the value for your key, like can you tolerate some staleness so that you can uh maybe like have better latency to answer your request. So, there are many different dimensions of properties here. So, this can be separated into, let’s say, uh those requirements. So, let’s say how reliable is the system, how reliable is your key-value store or databases. Like, what if it failed?

10:22 Like, how long would it take to actually recover? Um so, this is one perspective. And second perspective, as I talked about before, is consistency. Like, what kind of consistency level or requirements do you require uh for your for your setup? And uh also, what is your objective? Like, are you going to optimize for throughput? Or are you going to optimize for latency? And what is your workload scenarios? So, this has like very uh diverse range or diverse dimensions of like uh all of these requirements and things that we can potentially specialize. So, for example, if all of your requests are like hot

10:53 keys, then you can design your read cache in the way that it’s like caching all of the hot keys in memory so that you don’t need to uh actually fetch it from, let’s say, uh from disk or something like that. But if you all of your uh requests are sort of like write requests, then you design something completely different uh comparing to like a a read-heavy request. So, um we started exploring uh basically taking existing uh traces. Uh so, uh some of the existing traces are like just like basic traces, but tuning tuning it in different ways that it has like different read and write ratio. Um and

11:25 then also, we have like some production traces we take uh from Tencent and also like all of the other um like Twitter traces as well. And then we see whether if given that you know this workload information and you you know like what is the objective functions they are going to optimize for and can AI actually generate something that is better let’s say comparing to RocksDB or Redis and different stuff. And actually indeed like those agents are coming up with new designs, different sort of caching designs and different sort of workloads and requirements. And also like different

11:56 sort of let’s say hierarchical memory management you put different sort of like size of the cache in in memory or different size of the things that you put on disk. And then also for consistency management then like how do you make sure that it’s actually correct to maintain let’s say read after write consistency or like strong consistency if you expected that. So we created like I think around like six to eight different kind of traces and then we see if given this information for this particular

12:26 specialized workloads whether the agents can specialize for that. And actually it’s achieve like up to four times better performance comparing to those like even like a very specialized systems from let’s say like Microsoft. And yeah see good performance there. >> I guess my first question is well I guess this I don’t want to like I really want to kind of talk about like I’m worried this pivots the topic out too much but I guess like would it build on to an existing system? Like do

12:56 you think it like the specific maybe let me just ask like so I think about like kind of this is being like a DS Pi for systems or you know specifications I think is a paper that came from Berkeley and Jared Davis and this idea of yeah like abstracting how you design a system. So so do you like I guess it almost makes me ask like what is software now like like what happens to the artifact of the system that’s created? >> Yeah we’re we’re we’re really curious about this question too. Like what is

13:27 the artifact now? Look, if you take our vision to the extreme, you’re getting you’re hitting on something really interesting here. If you take our vision to the extreme, you get to a point where the artifact is kind of a unique function it’s it’s a output as a as a function of the traces that you that you you provide. And the reason that we’ve had our artifacts before, why these things have stood on their own, why you have something like Redis, is because it used to take years and years to build these systems. It takes years to train someone to understand. Takes a team of engineers or a PhD team of PhD students 5 years to go build a system, harden it, get it to

13:59 the point where you can trust it in production. And then no one is going to go pick and build a brand new system unless you’re Meta or Google and you have this huge scale and, you know, the savings you can get are actually worth the millions of dollars that it costs you to develop your custom system. Otherwise, no it doesn’t make say it’s not saying sense for anyone else to do. I think we’re trying to build a system of saying uh if you could if you could hire a bunch of people to build a custom database just for you for your exact kind of things that you want to store, you could get better performance, but it used to cost you so much and we’re driving that cost way down with coding agents and

14:29 with the frameworks that we have. And I think as as True very correctly put earlier, the remaining problem is can you trust the system that we’ve built? And and a lot of our research the last 4 months has really been on how do we prove to you that the system that we’ve built is correct, either by tests and extensive test suite that’s evolving or actually by formal specification, formal verification, like a guarantee that this is correct. >> Yes, I think that’s maybe the topic that then dives deeper into the details is um how you think about testing and I’m

15:00 sorry if like we stay in the database if if you don’t mind if we kind of frame this mostly through databases just cuz that’s like all that I understand, but uh I mean maybe later we could talk about like how this might differ for a task queue versus a database, but but like if we could stay on the database thing and I I I guess maybe let me backtrack and ask how how how do you think about the specification? How it does it How does someone come in and tell you about what kind of workload they have, what kind of database they need? >> Um so I think there are some requirements that are about environments

15:30 that every user or whatever they’re trying to build something for their environments, they have the environments in mind. So let’s say how many machines do you have and each of the machine configuration like what is the memory size and what is the disk disk size that you can put. So this is definitely like something that user will provide in default. And then if you think about like different domains, actually different domains have different properties that the user might want to specify. So it can go from very high level. So let’s say I just talk about reliability. Like for example, if your database where if your data systems like fail, like how long do you expect it to

16:01 recover? Um and what is the data loss um that you can tolerate in this case? Like maybe most of the time like people won’t tolerate like data loss for for any sort of like database system you create. And so for example, reliability and second thing is about consistency. Like when users they have their requests like when they read their stuff, like what is the staleness of the data that it’s being read. Like if you can tolerate more uh about staleness, maybe I can give you better performance from the database I create, right? So this is another dimension. And um about the workloads

16:32 itself, like sometimes people uh when they build their systems, they have their workloads in mind. So let’s say uh particularly let’s say for the key value store in in our cases, maybe you know what is the rough like read write ratio. What is the uh like recency or frequency of a particular key uh in your workloads that you can optimize your systems for, right? So as I talk about like if you have a very read heavy workloads, it would be completely different than optimizing for a very write heavy workloads for a different like consistency level. So uh I think there are some basic characteristics about uh

17:03 let’s say the workloads that you have, the requirements that you have, and also maybe including that like the objective functions. Like maybe you know that you want to just like minimize the user uh latency SLOs and you have some particular constraint over like I’m not going to violate uh this SLO while while building my system. So, um there are like basic properties that uh let’s say it’s probably domain knowledge or like expert knowledge in a particular domain. So, let’s say databases I just like list out a couple of things. But maybe in storage system it would be something different. And in inference systems it would be completely

17:33 different, right? So, probably like in that cases like there’s uh consistency is like something in in a different notion and correctness is a different notion as well. So, how we learn from this like what is considered as what I should provide in specification is very domain specific. And probably people have uh built like years of systems that follow this routine, right? So, let’s say when you write a database paper about like building a database engines, maybe you write about this particular property about fault tolerance, about like reliability, about consistency,

18:03 about performance metrics. So, uh from either the codes or the literature you know sort of like what are the basic properties that you want to post. And if the user doesn’t know uh I should probably talk about Okay, I should specify my consistency level. Then the AI should be able to post the question and say like, “Oh, so what is your requirements? Like, what is your uh what is your constraint here?” Like, it shouldn’t like assume something that the user doesn’t even say. So, I feel like the the gap between like let’s say if you just naively use CockroachDB, it might go ahead and do something that you don’t expect. But then of course like uh

18:36 if you have a good pipeline and you know like the domain knowledge and what people have been built before, then you know that there are several principles and properties about the domain of this uh artifacts that you should ask and you should clarify before proceeding uh proceed to like build a brand new system. So, uh I think this is the spec that we’re trying to build and we’re trying to build this spec in a way that is like follow domain knowledge. And when we shouldn’t assume something, you should post the question. And uh and just proceed building like a specialized systems from there. And I I I think this

19:06 spec can be let’s say uh I’m talking about a way that like let’s say I’m just daily user of like CockroachDB and I’m like typing like oh I want to build a database for my workout. And I’m I’m expecting cloud code to ask like oh so what do you want to optimize for? Um what is your consistency requirements? What is your uh what is your reliability requirements, etc. Um but of course like Shriram can talk more about how do you actually like if you are domain expert already and you know what you want to write, you probably can write like a formal spec and then let’s say that they uh the coding agents according to the formal spec can generate some sort of verification where like uh formal proof

19:38 so that it proves that it completely satisfied by the spec, yeah. >> Yeah, completely agree with this. I think I think one more point to highlight here is that we again given that we were using this tool to generate systems, we kind of understood some pain points about that okay writing spec is very difficult. Like you can’t expect a user to come and tell the entire routine or entire laundry laundry list of everything that they might expect from a system. So in the pipeline again if if if you go for cloud code, it might and if you prompt it well, it might actually

20:09 ask you questions or it might show that it can ask questions. it might like show off that capability. But one thing that we realized were was that when a engineer actually builds a system, so when the code development happen, then there are a lot of gaps that start surfacing. And when those gaps start surfacing, cloud always takes the cheaper way. For example, if you ask it to optimize for performance, it will take that assumption where performance optimization was easy to do and it will not care if it is hacking. Very simple example, we started using some YCSB

20:40 traces and things like that. And again, if you don’t know about the trace, that trace is more or less deterministic. Where given the key, you can actually predict or not even predict, you can map the value from the key. The initial systems that we built, it was like 30 times throughput, 40 times throughput. And of course without seeing anything, we were like okay I think we have we have built something. But as we get got into the details, it was very clear that cloud was basically hacking it and it was a very obvious you You it’s like an axiom that in a system I’m not going to give you keys where the values can be determined. It’s all about storing those

21:11 values. And then our insight there was that when the code development happens, then only there are more and more holes that are going to be exposed. And our synthesis system, which is like SkySynch, is able to surface the right level of abstraction that the user should be able to answer. In So, we again, we do two types of generation. One is a generation where you are actually starting with requirements as she was uh mentioning. Where the system you designer knows the requirements that they want at some level. But they might

21:41 not be the people who can actually do things in a formal way. By formal way, what you can imagine if if I ask you to write a sorting function. Of course, you will be having some properties that okay, my negative number should be on the left-hand side, my positive number should be on the right-hand side. If there are duplicates and this is this is how I’m going to handle. So, you can give some high-level specifications to what you want. But if you’re doing things in a very critical domain. For example, in databases, of course, you know uh read your write or there are like properties that you care about. Those properties, there are sometimes

22:13 they those properties are actually sometimes very hard to define in natural language. Because it is not clear because you’re talking about like concurrency, distribution. And it’s not easy unless you start defining things in a slightly mathematical format. That we call formal language. Like that is what Lean and Rock used to do. So, in our pipeline, the thing is that when a user comes with a system design or comes with something which they want to build. The the agentic system is going to probe the user with the right level of questions. And take the route of either the formal

22:43 way or the test-driven way. And in that then again, our loop is basically designed to keep on finding out what the gaps the user missed. And as and when those assumptions need the user, the user will be probed. Otherwise, right level of assumptions will be made so that the system can be built more robustly. So, the optimization pressure is something that leads to reward hacking and Sky is in this somewhat a vaccine that basically prevents the system from doing a lot of reward hacking. >> Yeah, it kind of reminds me of like quad

23:16 code. Like, you know, it writes some tests. It’s like, I passed the test that I also just wrote and and that kind of thing. And then, I mean, it’s just amazing thinking about like it still sounds like you have the sort of like classic deep learning machine learning like training data testing data. But now, the artifact instead of a trained model is code, a system. And then, the data is also like more persistent, I think, than you you Well, in the sort of search and information retrieval sense, you kind of have like this persistence of like the corpus. And that maybe comes into this

23:47 territory bit, but um Yeah, I guess like kind of maybe talking about testing and you mentioned like formal proof. I guess it just makes me think like, you know, if I say, “I need you to sort these numbers.” And okay, so, you know, it’s going to either maybe bubble sort it or it’s going to quick sort it. It’s like, how do you then like how how do I know the difference between if the system has done either bubble sort or quick sort? >> Yeah, so, these type of things ideally, um so, you should specify when you first ask

24:18 like Sky to synthesize to synthesize these things. But, our system first on tries to understand what you implied in your task specification. So, if you asked it to come up with a sorting algorithm, probably it would first ask you back, uh okay, um do you have like any preferences on the time complexity of this? Um then, if you say nothing, okay, just give me a quick one, it will do some

24:50 literature review and try to see what other code bases exist in that domain. Then, it would try to implement what it thinks is the best given your specifications you provided. >> So basically like the test should be tight with whatever you specify in your properties, right? So for example like let’s say if you don’t formally prove your let’s say consistency or whatever other fault tolerance level, you probably want to stress test a little

25:20 bit about how like how how fault tolerant is the system, right? You can like send a bunch of requests like many many concurrent requests as well and see whether it can it would just fail and see after when it fails like how long does it take to recover as well. So I think people have this like test-driven development things in production system as well like because they cannot formally specify each part or each component of their end-to-end system. And this stress testing is tight with particular properties that you desire and you typically want to see like okay how long

25:51 does it take to recover, whether it does like garbage collection and do when when workload shifted it’s like completely like breaking down or something like that. So I think yeah so so so test is like basically tight with whatever you specify and whatever the users want in in their specification. Yeah. >> Yeah. And and in general again you you put that point very correct that this cloud will basically tell you that I generated 100 tests and and 100 tests are passing because writing good quality tests that are actually capturing those specifications is the key. And in the

26:21 pipeline again the idea is that every test that is added is actually enforcing that spec. So again there are some details here that the test will have to prove that it is actually testing the particular specification by generating say a reference implementation which is correct on that aspect and incorrect on that aspect. And if it is actually able to differentiate this that that then only that test is actually like a gate that can allow a system to pass or not pass. So it’s more more like a rigorous way to do things because the domain actually requires you to take care about

26:52 those specifications. >> Yeah, I mean I guess like on on I’m really interested in it just inspires me to think about like Python versus like Go and just how you think about the abstraction of what the system is working with cuz if it’s say something like Go or maybe I know Rust is maybe more popular but I would use Go maybe it’s not that’s what I mean by like slightly lower language but I’m like and it’s looking at something like heap allocation and just I guess that is quite different like when you’re

27:23 I don’t know if you want to call this vibe coding or like what we call sort of LLM coding but like what language it’s using on top of that really I think influences just like how it works with these specifications. Some I guess I’m just curious how you think about maybe even just like programming languages with this. >> Yeah, I mean again good question. So that one one thing to take care of this when when you’re building a system is of course you you you can either have preferences that is one thing but if you

27:54 don’t have a preference then the goal of the system is that it is optimizing for a particular workload. So you really care about performance in that part. And when you are caring about performance when it starts getting into like the blind spots there there would be some languages that might be easy to build in terms of closing those blind spots. For example, if you are caring about something where memory safety is actually a thing the system will steer the agent to use that memory safe language like like Rust because the

28:25 system is going to be built more carefully and it will be it will have a hard time compiling and hence whatever is built is going to be memory safe. But maybe the performance will get compromised. So in fact the language is also something that is very attached to the performance that you need the specifications that you care about and to make those specifications abide by you are basically writing tests. So so the whole thing is that me for example, if you do kernel engineering like a very simple example, it is very easy to write a correct kernel when you start with the

28:55 high-level say PyTorch or Pythonish language, but then you all you care about is performance. Now, if you are dealing with a TPU versus say X version GPU, you want to go into that stack where it allows you to write the things where you can say fuse the kernels very effectively or if it’s like a quantized kernel, you are caring about how the precision errors can be minimized. So, it’s it’s really really an implementation detail the user should not be caring about it unless they have a preference and that’s how our system currently actually helps the user that unless and until this is an assumption

29:26 that is leading to a path where the specification needs to be changed here or there, the user will not be even exposed with that. He will be given that implementation that is ideally most performant and least reward hacking. By least reward hacking, if it’s the test route, it’s more about where the tests can be done very very properly. As I said, Rust will be more more favorable if it’s like a memory safe thing, but if there are things where you don’t care about it and you can get better performance not caring about your compile time memory safety

29:56 requirements, you will go in a say a C route or something. And on the other side in the formal space, they again there are like Lean and Rock which acts in the model world where you are trying to prove things. In the downstream again, you either try doing some old-style OCaml kind of languages, but in the latest world again, you have CompCert kind of compilers which is in the C world. Plus Verus kind of things which is in the Rust world. So again, these are like very very intricately attached to what you really care about because you can write everything in every language. What

30:27 you choose will basically decide how easy it was to test it and how performant it was at the end. So, it’s really depending on your objective that you care about. >> Yeah, you make me want to brush up on my understanding of compilers. It’s been to be since I did >> [laughter] >> all of that um and I guess like yeah so I guess my question is like you know from the specifications you could just go all the way into maybe generating like a binary I guess like in a super crazy way. Like you like do you think that’s ever

30:58 or does it always have to be some intermediate code artifact? >> I mean again very very very good good question. So that the whole thing here is that if you are if you if you give me a specification and you care all about performance again at the end of the day you really really want a binary that was not built off any compiler that was making any assumptions to speed up your implementation in a general way. So you really want your agent to actually write you like assembly code if not if not binary that

31:28 is like very very performant for your system and again if it knows your workload it might be doing some pre-fetching some things that can’t be done on the higher level languages. You want to go there but obviously like there is a cost aspect attached there also because you would require the LLM to iterate more and more and more to get to that level. So it’s it’s somewhere where you basically close your boundary saying that okay I’m fine running this experiment or running this system building task for X hours and I spend N number of dollars on this. In that time you really want to want your system to

31:59 be there. But again once you have a version LLMs can be made to work without eating and sleeping. So in an ideal world you can just make them optimize the thing more and in the optimization again when the language becomes a barrier that okay now to optimize further I just need to go to a lower level language it’s again like kernel engineering once the once the idea of how to write flash attention gets invented you really need to go into the lower level level language to actually do the memory fetching because Python or PyTorch won’t allow allow you to do that. But yeah I

32:30 mean I hope I I answered you the question but that’s the point. >> Yeah I mean I hope I’m keeping the conversation but yeah, it just makes me think about like right now I think you I mean, you’d have to be pretty cracked, as they say, to like have be managing a repo in like multiple like language abstractions. I think that’s kind of what where this is taking me. Like if I had a Python project that also has like a like a parts I mean, yeah, you you have like connection Sorry, it’s been a while since I’ve done projects like this where

33:02 you would like connect like C into Go. So, it’s just been a while since I’ve really thought about that kind of thing. But, uh Yeah, cool. And And I guess I’m still just kind of thinking about like you know, like building on top of say Postgres or you know, Weaviate’s open source like just how you think about extending open source say databases and just what role that has to play in this research.

33:32 >> Um so, maybe like I think we’re still actively thinking about like in what cases does it make sense to synthesize something completely from scratch versus like optimizing some existing systems. So, of course, like synthesizing something completely from scratch can take probably a lot of time. So, there are maybe like for very mature production ready systems, maybe they’re like they have their built for like general workloads, they have like many many test building in their original like the the systems that is open source

34:04 or closed source. And then so, it takes less time to build those components, but probably synthesizing from scratch can allow you to jump out of the local optimum that is being heavily constrained by whatever structure that the general systems has. So, let’s say if I were to build on my general system, maybe I first need to understand like 40K lines of codes for the general system to be able to see like oh, maybe tuning this parameter will work for this kind of specialized workloads. Maybe tuning a combination of these two configurations will work for my particular requirements. So, of

34:35 course, like it takes time for understanding the code bases and probably the structure or the abstraction that the general systems has might not be the best for your specialized use cases. And it’s unclear that like whether one case optimizing it is actually can achieve better performance comparing to synthesizing something completely from scratch. And we actually try like in our key value store use cases of like building on top of like marker Microsoft faster and see whether it can like do it well. But then comparing to our synthesizing from scratch from

35:05 scratch experiments is actually achieve less throughput comparing to just like building something completely from scratch. And in in of course like a time constraint like sometimes coding agents can get stuck in the local optimum and thinking about oh this abstraction is everything that I have. So, I’m just going to tune partial or partial like components of the system. But versus like when it thinks something completely fresh maybe it can come up with a better design from like thinking about backing up in a high level like how should I design my memory? How should I

35:36 coordinate between memory and disk? And how should I handle all of the requirements that the user have? So, ideally I think the system that we trying to build is like knowing when to synthesize, knowing what to optimize. But then at the same time like ensuring that everything either you do optimization or synthesize from scratch, you want to make sure that you don’t break some of the guarantees that the systems should have what the user specify in their specification. So, correctness still matters when even if you’re just like optimizing for a particular system. So, let’s say if you change the cache the caching algorithm

36:08 or the caching components of Redis and then actually something break whenever you you input a new work code then it’s not correct. So, I think in both cases we should think about like okay, so what are the set of right right set of tasks and what are the right set of guarantees that we should provide to the user so that the user would trust the ultimate artifact that are being generated by the by the agents. And second thing is of course performance. Like in given like a limited let’s say time budgets and also cost constraints, is it better that I start from let’s say existing well-known

36:38 system? If so, start from what system? Because like many different There are many sort of like open source like databases out there and which one should I get started with? And versus like completely synthesizing from scratch. I think those questions as models become more powerful, hopefully like the model will know like what kind of high-level spec that the each systems will provide and what whether each system will have like specialized [clears throat] strength in terms of optimizing for a particular workload so

37:09 that it can dynamically choose between okay, like I am going to optimize the system and I’m going to choose this system to get started with because it has this kind of properties that it’s easy for me to to optimize. Or I’m just going to completely start something from scratch where I see let’s say some features are completely not supported in any of the existing open source databases. So, I might as well just build my own design. I have a whiteboard, maybe I can draw like my key design idea to optimize for this workloads and I’m just going to synthesize something completely from scratch. So, hopefully this will be more

37:39 automated and I think yeah, so we’re trying to build something that can achieve this, but the goal here is having both correct and also being very specialized in performance. Yeah. >> If I can I want to call out here just like how surprising this this like take is. I think it was like surprising for us when we got to it too, but I think for the current stage just of where the field is at, if you’re working in AI, you shouldn’t be like designing or building or thinking of what you’re doing as for today. You should be thinking if you look and follow the

38:09 trends of where they’re headed, you have to skate to where the puck is going, not where it is. And so this is it’s this really weird thing, right? Where it’s like it’s counterintuitive to think that you should start from scratch to build your system if there’s an existing system out there. But if you assume as the model is getting better and better at building and reasoning and designing, um it’s so easy for it to even get to any particular design. You should just let it start from scratch and be fully unconstrained, and that actually takes you to the best outcome. We used to start from existing systems and it would shortcut. We would save a lot of work, but if that work is actually easy for a really smart model,

38:41 there’s no need to constrain it or from starting from that point. >> Yeah, I think it’s amazing, especially like from the sort of research what’s possible angle, but I’m I’m also curious about so like, you know, when we have these systems like when we have Weaviate Cloud, we I guess there’s like there’s like a few levels to it. It’s like we sort of have like the knowledge of how to host it, like how to like how to run it in like how to run it at scale, and then like how to debug it. And I and I think those kind of arguments I could see

39:11 these systems certainly like having a huge impact on that, if not completely being able to do that. But then I’m there’s something to I think like the concept of like uh like managed infrastructure, where it’s like you have like a provider like like Redis as we’ve been mentioning. Like they have like Redis Cloud, and so there’s probably still something to like these systems that like that still like have a managed infrastructure somewhere else, but can you still tailor those? Does this research have some intersection with that kind of thinking? >> I I think I totally I I I think that um

39:44 yeah, look, there’s independent like like like there’s business reasons you might want to have someone else host something for you. You just want to don’t have the kind of people on call managing it. There’s kind of like technical reasons, like maybe you don’t have the the team to go and build out or check or even write your specification correctly, so you’re going to pay someone you know that Redis has the right specification for the system that you’ve built and you’re not a technical team or something. Um I still think that the ideas that we’re working on are eventually going to slot into even those systems, because you could imagine a hosted version of something like a Sky Synthesizer

40:15 Sky Synthesizer Optimizer or Synthesizer that given a streaming set of queries great. There’s still an interface of puts and gets, but given the last 24 hours of puts and gets, I should have a re-synthesized system that’s going to do really well on that distribution of of uh, of traffic. So, I actually think this will this will fold really well into that that model. Um, >> Yeah, it’s so cool cuz you yeah, you might have like these machines with like cuz you have like a shared set of like machines with their RAM and disk and then it’s like perfectly allocating what fits into it. With this new one, yeah,

40:47 wow. That’s so cool. >> Yeah. >> Yeah, amazing. Um, yeah, so I guess maybe I’d love to kind of come up the abstraction quite a bit and maybe talking a little more broadly about like systems that everyday people might want to use. Alex and I had a little joke before we were before we started recording where um, I was explaining to Alex that I use Zen caster for recording instead of Riverside and we’re talking is that I think I know of some software that might be able to create me a podcast recording software. Uh, how do you guys think about like this idea of um,

41:18 generating software for say note taking or email? >> And you I I can try to briefly add this which is just to say that like humans are much messier than machines. So like it’s to write out the like semantics that the like the actual formal specification for a key value store, it’s it’s ugly. Specs are hard to write. Um, we’re trying to make that easier. We’re doing research on that, too. But there’s kind of formal languages to model interaction between machines. Uh, it’s much trickier to kind of formally model how would you even

41:49 specify what what uh, like a note taking app should do, right? The way that we often do this we you know, there are people that actually do this. We have name we have a name for them and they’re product managers. Product managers are like they’re kind of responsible for for translating between the like conceptual idea of what we want to talking to engineers and trying to explain to them in their language, still in English, but in English that that programmers understand and the programmers going to write it in code. So, um conceptually, so today, if you look at SkySynth uh like up just the Sky Discoverer framework in general, as we

42:19 think about specification, a lot of what we’re reasoning about is either you give us a formal spec, or you kind of in in human language describe what you want, but we kind of generate tests that in in in code the the human spec. Um the this the the the intent of the human. You could probably get to a world where you could just as well synthesize um uh kind of sets of tests of behaviors with a note-taking app, where like you can take notes, you can go and create a new note, kind of feature descriptions or PRD-style designs. Like that’s what a spec looks like for a product.

42:51 I think that we as a Sky Discoverer team are really quite focused on the core systems aspect of this, partly because it’s just it’s a really hard problem, but I think that the product synthesis side will be really interesting, and just looking at what the right medium is to capture a spec for a product, which to me is a PRD, um we’re we’re not looking at that in our research, but I do think some of the techniques we’re developing would would be applicable. >> Yes, yes, yeah. As Alex said, um so

43:22 Sky Discoverer Synthesizer has two main arms, uh either test-driven development or formally specified like doing formal verification on uh formally specified systems. Um yeah, unfortunately, it’s incredibly hard to capture uh what humans actually desire from like these um unverifiable domains, like design me a good web application, a nice UI. Um so, we’ve been also trying to build some UIs for some of the systems we

43:53 built using Sky Discoverer. Um that part takes some other set of skills, uh definitely. >> Yeah, and I they kind of remind me of what uh Shu was explaining earlier with the like I think like the idea of asking someone like um what recover like what what recovery can you tolerate? Like I you know, I’ve done a lot of talking to start ups and entrepreneurs like product builders who are like this idea of communicating these these ideas.

44:23 I think there’s like a huge gap there that’s really interesting and just yeah, what specific like when is the specification like a chatbot? No. Yeah. Okay. Yeah, cool. >> Yeah, so at the start of our um framework, uh there’s a spec building part. The spec building part takes in some specifications from the human um about what should be built. Um now it for the case that is test driven development,

44:53 um the framework essentially checks um if the spec that the human provided is clear and comprehensive enough. In that case, it would start doing some uh profiling on the workload that you specified. Uh it would go and see uh what other specs exist in related code bases that are out there, etc. But there are also many cases uh like you mentioned uh where the input specs are not clear and

45:25 human input is needed. Uh then yeah, um it acts like a chatbot in the sense that it tries to iteratively disambiguate uh what’s going on with the human. >> Yeah, amazing. Yeah, so um I know we’re kind of coming up on the time and I usually anchor the We Have Podcast with you know, this general like what excites you about AI, but I am I have to ask one more technical question about this. How do you think about optimizing the system? Is it something like say like Geppa for system design? Like or is it

45:57 like a Yeah. >> I think optimizing system first of all the problem is larger in scope because systems if if if you care about a system generally that system is also very large and even finding out what is the right way to optimize what is the target in it meaning a code base is going to be huge there are like hundreds of things that you can optimize but there are specific things that are worth optimizing. And in optimizing systems there also

46:28 there’s also one more point unlike say text optimization that the evaluation is not that easy. Like if you really care about say hardware design or if you care about something like even inference engines you optimize something and the loop of getting the full feedback is like running lots of tests like if you care about VLMs there’s like probably 25,000 or more tests and then you actually are going to run all the workloads to check for correctness and then you will run several workloads like different pre-fills different decodes different agentic workloads to get some numbers in

47:00 terms of say throughput or whatever and again even though in text optimization also there is generally a multi objective space with trade-offs in the case of or in the world of system optimization the trade-off is actually very real because you tune something for memory your throughput will be fully bad or or you are you are tuning something for latency and your throughput is just going away so it’s very hard to and and as always it’s very hard to define these trade-offs it’s not like the human knows what is the right perfect point to have so in optimizing of systems which is

47:31 obviously like one of the arms that system optimization had been a thing all the laws had been there for how you find the right problems to solve and how you optimize them in the Sky Discover pipeline making it agentic and the next version which we are of hopefully planning to have is where the agents can themselves scout for right problems the agents can themselves build the small simulators you can imagine or some sort of like proxy evaluators which can give it the capability to hill climb. So, once it is able to hill climb, then it

48:02 becomes a hill climbing problem which is equally same as like Jepa for text optimization or any other technique which could be doing evolution over the text. But, the problem becomes identifying the problem and getting the feedback in a way that the LLM can do. If I If I like give you a number in our KV generation, like the key value generation or optimization, probably 80 to 90% of the time is pending evaluations. Hardly 10% is actually like text manipulation. So, the bottleneck becomes that and if you want to scale your agents now, if you want to like run

48:33 hundreds of agents doing this, you your objective actually becomes like a meta problem which is first get me the right kernel that is supposed to be optimized and get me a right proxy to actually measure just that kernel which is like very fine-grained details or fine-grained profiling that is going to help me in identifying how to evaluate and how to find out the bottlenecks which are the key to getting better performance. So, that’s how we kind of see that it’s like a meta problem and which doesn’t really exist in the text space because in text space it’s more

49:04 Again, it’s not a simpler problem. I’m not not trying to infer that, but it’s more defined in that world and the bottlenecks are different. >> So, [clears throat] also circling back to uh what Alex said at the beginning of the uh podcast actually about So, given some evaluation evaluators, um you could imagine trying to optimize some prompt of a system or a function that is doing a a specific job. Um as um like select part of the system.

49:36 But, now if you start from the specs, it’s not even question It’s It’s not even clear what the tests should be. It’s not even clear um which parts of the code base should you be optimizing. Um it’s moreover um it’s not even clear if the specs are complete. Um did you the user specified maybe some workloads, but as you said, hopefully the design system should be robust. It should be it should

50:09 generalize to perturbations around what the user asked for. So, can you come up with some other adversarial workloads to test the system? And moreover, what if the specs change over time? Um can you adapt to that sort of outer loop and like get human feedback to iterate on your tests even more these sort of workloads over which you optimize more. So, yeah, it gets a little broader than the

50:40 >> [clears throat] >> sort of classical evolutionary systems with which we use to optimize functions, etc. >> Yeah, I guess if I can just give my quick take on it, I think of it as like Geppa has this Pareto frontier of candidate program like you know prompts usually it’s used for text optimization, but like it could be candidate programs like it could be code for the database designs. And then the Pareto frontier I guess instead of being like training examples

51:11 and again like the text sense like you know a particular prompt for writing a blog post and like for like you know this one prompt wrote a better blog post about mitosis than this other did about you know another topic in biology. And like that’s how you think about it in that world, but in this world I can imagine that the tests like kind of define the Pareto frontier. But then I think what I’m learn what I’m what I agree a lot with this idea is that the evolutionary optimization should also be coming up with tests. Like it should be able to propose new tests and like evolve that concept as well and

51:42 evolutionary optimization is definitely a very cool topic. It’s fun thing to think about. >> Amazing. Well, Alex, Mark, Shue, Shobha, it’s just been such a fun conversation. I’ve learned so much and so cool to meet you all. Thank you so much for joining the We View podcast. >> Thank you so much. It’s a very >> Thank you. >> Yes. Thank you. >> It was very fun to talk to you. >> [music]

52:22 [music]