Recursive Program Synthesis - Aws Albarghouthi

Recursive Program Synthesis - Aws Albarghouthi

Aws Albarghouthi, Associate Professor of Computer Science at the University of Wisconsin-Madison, discusses his paper “Recursive Program Synthesis”, which introduced Escher, an inductive synthesis algorithm for learning recursive programs from input-output examples.The project emerged from Albarghouthi’s early work in program verification and inductive proofs for recursive procedures. After he and fellow graduate student Zachary Kincaid developed initial ideas for synthesizing recursive programs, they cold-emailed Sumit Gulwani at Microsoft Research, whose feedback and collaboration helped shape the direction of the paper.In This Episode -- Recursive synthesis from examples- Escher’s forward and backward search- Goal graphs for partial programs- Components as reusable building blocks- Synthesis benchmarks and comparisons with Sketch- Quantum compiler synthesis- Qubit mapping and routing synthesis- Agent correctness and prompt injectionReferences -- Microsoft PROSE: https://www.microsoft.com/en-us/research/project/prose/- SKETCH: https://people.csail.mit.edu/asolar/papers/Solar-Lezama09.pdf- Generating Compilers for Qubit Mapping and Routing: https://arxiv.org/abs/2508.10781- Synthesizing Quantum-Circuit Optimizers: https://arxiv.org/abs/2211.09691- ‘Introduction to Neural Network Verification’ book: https://verifieddeeplearning.com/About the Paper -“Recursive Program Synthesis”Aws Albarghouthi, Sumit Gulwani, and Zachary KincaidComputer Aided Verification, CAV 2013The paper presents Escher, a synthesis algorithm that learns recursive procedures from input-output examples. Escher combines component-based enumeration, interactive example refinement, and a goal graph that helps assemble partial programs into complete recursive solutions.https://www.microsoft.com/en-us/research/publication/recursive-program-synthesis/About the Guest -Aws Albarghouthi is an associate professor of computer science at the University of Wisconsin-Madison. His research focuses on program synthesis, formal verification, quantum computing systems, and the correctness of AI agents.https://pages.cs.wisc.edu/~aws/Credits -Host & Music: Bryan Landers, Technical Staff, NdeaEditor: Alejandro Ramirezhttps://x.com/ndeahttps://x.com/bryanlandershttps://ndea.com

DreamCoder's Wake-Sleep Library Learning - Kevin Ellis

Kevin Ellis, Assistant Professor at Cornell University, discusses his influential paper “DreamCoder,” which presents a system that jointly learns reusable program abstractions and a neural search strategy through an iterative wake-sleep process. The work emerged from early efforts in library learning and a broader question about how humans accumulate concepts over time. Ellis reflects on the challenge of searching vast program spaces and how inspiration from cognitive processes, particularly dreaming and replay, led to a system that incrementally builds knowledge by reusing prior solutions. In This Episode - • Program synthesis beyond formal specifications • Natural language as executable programs • Library learning for compositional reuse • Wake-sleep cycles for program learning • Neural-guided search over program space • E-graph refactoring for abstraction discovery • Emergence of map and fold primitives • Probabilistic programs for uncertainty • World models beyond frame prediction • Program synthesis benchmarks References - • ARC-AGI-3: https://arcprize.org/arc-agi/3 • ExoPredicator: https://arxiv.org/abs/2509.26255 • AutumnBench: https://www.basis.ai/blog/autumn-platform-2025/ About the Paper - “DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning” Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, Joshua B. Tenenbaum PLDI 2021 (ACM SIGPLAN Conference on Programming Language Design and Implementation) DreamCoder is a program synthesis system that learns both a library of reusable program components and a neural search policy by iteratively solving tasks and compressing solutions into abstractions. It alternates between solving problems (wake phase) and improving its internal representations via abstraction and dreaming phases, enabling more efficient search and generalization across domains. https://dl.acm.org/doi/10.1145/3453483.3454080 About the Guest - Kevin Ellis is an Assistant Professor at Cornell University working on program synthesis, neurosymbolic AI, and computational models of cognition. His research focuses on learning structured representations such as programs that capture compositional knowledge about the world. https://www.cs.cornell.edu/~ellisk/ Credits - • Host & Music: Bryan Landers, Technical Staff, Ndea • Editor: Alejandro Ramirez • https://x.com/ndea • https://x.com/bryanlanders • https://ndea.com

Semantic Programming by Example with Pre-trained Models - Gust Verbruggen

Gust Verbruggen, Senior AI researcher and member of the PROSE team at Microsoft, discusses his paper "Semantic Programming by Example with Pre-trained Models," which introduces a framework for integrating inductive program synthesis with large language models. The project emerged from an attempt to extend Flash Fill-style program synthesis beyond purely syntactic string transformations. Motivated by limitations in symbolic systems - especially their inability to access semantic knowledge without manually encoding it - Verbruggen and collaborators explored how GPT-3 could serve as a semantic oracle within the PROSE framework. The result is a neurosymbolic architecture that preserves the efficiency and guarantees of symbolic synthesis while selectively delegating semantic subproblems to a language model. In This Episode • Limitations of both program synthesis and LLMs • Programming by example • Syntactic versus semantic • Integrating GPT-3 as semantic operators • Semantic map, position, and condition operators • Deductive backpropagation in PROSE • Deferred query execution for efficiency • Greedy clustering to control search explosion • Ranking programs to minimize semantic calls References • https://www.microsoft.com/en-us/research/group/prose/ • https://www.microsoft.com/en-us/research/project/prose-framework/ • https://www.dagstuhl.de/en/seminars/seminar-calendar • Sumit Gulwani's Flash Fill talk: https://youtu.be/421gU482xFE About the Paper "Semantic Programming by Example with Pre-trained Models" Gust Verbruggen, Vu Le, Sumit Gulwani Proceedings of the ACM on Programming Languages (OOPSLA), 2021 This paper presents a framework for augmenting inductive program synthesis with semantic operators powered by large language models. By decomposing tasks into syntactic and semantic subproblems, the system delegates only the irreducibly semantic components to a pre-trained model, while maintaining symbolic guarantees elsewhere. A deferred query execution strategy allows efficient learning without excessive model calls. https://dl.acm.org/doi/10.1145/3485477 About the Guest Gust Verbruggen is a researcher at KU Leuven and a member of Microsoft’s PROSE team. His work focuses on program synthesis, data wrangling, and neurosymbolic integration, particularly in real-world automation settings such as spreadsheets and code refactoring tools. • https://www.microsoft.com/en-us/research/people/gverbruggen/ • https://scholar.google.com/citations?user=TmU3sKMAAAAJ&hl=en Credits • Host & Music: Bryan Landers, Technical Staff, Ndea • Editor: Alejandro Ramirez • https://x.com/ndea • https://x.com/bryanlanders • https://ndea.com

February 2026 Podcast Recap

Program synthesis is the problem of automatically generating code that satisfies a specification. The real challenge isn’t searching faster, it’s making the right parts of the search space searchable at all. This week's episode is a short recap of the podcast so far. Across the past 8 conversations - spanning grammar filtering, temporal synthesis, inductive logic programming, vision-language programs, and symbolic world models - we explore 3 emergent themes. 1. Shrinking the search space, without breaking correctness 2. Why "correct" programs still behave badly 3. The real meaning of "neurosymbolic" At a high level, all of the solutions we've explored are grappling with the problem of search - from problem representation to the optimal divide between neural and symbolic. Credits - Host, Editor, Music: Bryan Landers, Technical Staff, Ndea https://x.com/ndea https://x.com/bryanlanders https://ndea.com

Relational Decomposition for Program Synthesis - Céline Hocquette

The way a problem is represented can determine whether it is solvable at all. Céline Hocquette, AI researcher at Ndea and former postdoctoral researcher at the University of Oxford, discusses her paper “Relational Decomposition for Program Synthesis”, which introduces a representation-driven approach to inductive program synthesis based on decomposing examples into relational facts. The paper emerged from Hocquette’s long-standing engagement with inductive logic programming (ILP), beginning with her doctoral work at Imperial College London under Stephen Muggleton and continuing through her time in Andrew Cropper’s group in Oxford. Motivated by the scalability limits of learning long chains of reasoning, the work reflects a broader intellectual trajectory focused on making symbolic learning systems more efficient by rethinking representation and decomposition rather than adding domain-specific heuristics. In This Episode - • Inductive logic programming (ILP) • Deductive vs. inductive program synthesis • Relational vs. functional programs • Decomposing examples into logical facts • Datasets: ARC-AGI, 1D-ARC, strings, list functions • Systems & approaches: POPPER, ARGA, METABIAS, BEN, Hacker-Like References - • https://github.com/logic-and-learning-lab/Popper • https://andrewcropper.com/ • ARC-AGI - https://arcprize.org/arc-agi • 1D-ARC - https://arxiv.org/abs/2305.18354 • ARGA - https://arxiv.org/abs/2210.09880 • METABIAS - https://www.doc.ic.ac.uk/~shm/Papers/ECAI-546.pdf • BEN - https://arxiv.org/abs/2301.03094 • Hacker-Like - https://www.nature.com/articles/s41467-024-50966-x About the Paper - “Relational Decomposition for Program Synthesis” Céline Hocquette, Andrew Cropper arXiv, 2024 The paper proposes transforming inductive program synthesis problems into sets of relational input–output facts, allowing systems to learn smaller, reusable logical rules instead of long functional compositions. This decomposition significantly improves scalability and generalization when learning programs from few examples across strings, lists, and ARC-style reasoning tasks. https://arxiv.org/abs/2408.12212 About the Guest - Céline Hocquette, Technical Staff at Ndea, works on program synthesis, inductive logic programming, and symbolic reasoning. She completed her PhD at Imperial College London and previously held a research position at the University of Oxford in Andrew Cropper’s lab. Her work focuses on scalable learning of interpretable programs from small data. https://celinehocquette.github.io/ Credits - Host & Music: Bryan Landers, Technical Staff, Ndea Editor: Alejandro Ramirez https://x.com/ndea https://x.com/bryanlanders https://ndea.com