UC Berkeley

Modern large language models are trained on large corpora of static source code but receive limited supervision about how that code behaves at run time. This gap surfaces at every stage of the AI programming stack: benchmarks that grade with weak or missing tests, training pipelines bounded by signals that never execute the candidate code, and inference-time verifiers that select for textual plausibility rather than execution evidence.This dissertation studies how to synthesize and exploit executable specifications: runnable artifacts that expose program behavior to an automated system. In this thesis, they take three main forms: tests and input generators, performance harnesses, and dynamic-analysis annotations. Once these artifacts can be generated from problems, repositories, or executions, they make behavior quantitatively measurable: agents can be evaluated by running candidate programs and comparing the observed behavior against the specified behavior. The same mechanism is useful not only for evaluation, but also for constructing training data and guiding inference. The chapters follow this idea across three settings (evaluation, training, and agent design), one for each of the three parts of this dissertation.Part I studies synthesized executable specifications for evaluation. In LiveCodeBench, the specification is an input generator paired with a reference solution: new tests can be sampled for each live-contest problem, making evaluation less dependent on static benchmark instances. In R2E, an LLM and static-analysis context synthesize repository-level equivalence harnesses that run a candidate function against the original implementation inside its GitHub context. In GSO, the specification adds a timed workload to the correctness harness, turning optimization into a continuous executable check on which evaluated agents score below 5% at a speedup threshold calibrated against expert optimization commits in real-world open-source codebases.Part II uses synthesized executable specifications as training signal: as rejection sampling filters, as behavior-preservation constraints, and as rewards. In R2E-Gym, executable fail-to-pass tests are paired with synthesized issue descriptions to create a procedurally curated training environment, and supervised fine-tuning on the resulting trajectories yields 34.4% Pass@1 on SWE-Bench-Verified, a +13 8-point gain over SWE-Gym at matched model scale. Test suites can also constrain training-data cleaning: candidate rewrites are accepted only if they preserve behavior under the original tests, matching full-dataset performance with 15% of the cleaned data. DeepSWE trains an agent end-to-end using the test suite as the only reinforcement-learning reward, reaching 42.2% Pass@1 and, with hybrid test-time scaling, 59% Best@16.Part III uses executable specifications at inference time. One verifier scores sampled patches by running synthesized reproduction tests, while another scores whole agent trajectories without execution. Individually, these verifiers reach 43.7% and 42.8% Best@26 on SWE-Bench-Verified; together, their hybrid reaches 51.0%. Syzygy synthesizes specifications at a finer granularity: top-level executions are mined into per-function equivalence tests and LLVM-derived dynamic-analysis annotations, which guide each step of a long-horizon C-to-Rust translation. This translates Google’s Zopfli compression library (3,000 lines of C) into compilation-safe Rust, validated against the original over 1,000,000 equivalence inputs.Across these settings, executable specifications provide a common way to turn execution into objective feedback for evaluation, training, and inference, and a unifying lens on AI programming agents that close the gap between static source code and runtime behavior.