Chronological feed of everything captured from Matei Zaharia.
Inductive Deductive Synthesis (IDS) is a novel agentic LLM framework that jointly and incrementally co-synthesizes implementation and formal proof for distributed systems, learning from failed attempts to guide strategy selection. It solves all 7/7 distributed key-value-store specifications—compared to 2/7 for SOTA coding agents—at roughly 200x the speed of human expert effort and at lower cost. Beyond correctness, IDS integrates performance feedback into the same synthesis loop, producing verified implementations up to 3x faster than previously published verified systems.
AI-Driven Research for Systems (ADRS) leverages LLMs to automate database optimization by generating hundreds of candidate solutions without human supervision, but the core bottleneck is building fast, accurate evaluators to guide convergence. This paper proposes co-evolving evaluators alongside solutions to automate the evaluation pipeline itself. Validated across three case studies — buffer management, query rewriting, and index selection — the approach discovers novel algorithms that surpass state-of-the-art baselines, including a deterministic query rewrite policy achieving up to 6.8x latency reduction.