Program Synthesis

Follow this topic Ask about this topic

Program synthesis studies how to turn desired behavior into executable code, from small transformations and algorithms to robot policies and engineering designs. Methods include enumerative and constraint-based search over domain-specific languages, learning programs from input-output examples, and language-model proposals refined through execution, counterexamples, or formal verification. These approaches can produce reusable, inspectable programs and support settings such as CAD, GPU optimization, and verified software; benchmarks such as ARC-AGI, PBEBench, and ProgramBench test how well systems infer behavior and generalize. Systems are increasingly effective when tasks have clear constraints and feedback, but open-ended synthesis remains difficult: plausible code may fail behavioral tests, miss the intended specification, or generalize poorly beyond the examples and search budget.

Latest papers

182 papers29 papers in the last four weeks, up 61% on the four weeks before. 0.2% of all new papers.

Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence
May 13, 2026Jun He, Deying YuAI Assurance Program Synthesis
Optimal LTLf Synthesis
May 12, 2026Yujian Cao, Sven Schewe, Qiyi Tang +1Program Synthesis Formal Verification
University of Liverpool
Equivariant Reinforcement Learning for Clifford Quantum Circuit Synthesis
May 11, 2026Richie Yeung, Aleks Kissinger, Rob CornishEquivariant Neural Networks Quantum Circuit Optimization
Department of Computer Science, University of Oxford · Quantinuum · College of Computing and Data Science, Nanyang Technological University, Singapore
Teacher-Aware Evolution of Heuristic Programs from Learned Optimization Policies
May 11, 2026Minyu Chen, Song Qin, Ling-I Wu +2Automated Heuristic Design Evolutionary Optimization
Shenzhen Technology University · Shanghai Polytechnic University · Shanghai Jiao Tong University
EGL-SCA: Structural Credit Assignment for Co-Evolving Instructions and Tools in Graph Reasoning Agents
May 11, 2026Zike Yuan, Yukun Cao, Han Zhang +7Program Synthesis LLM Agent Training
Harbin Institute of Technology, Shenzhen, China · School of Computer Science and Technology, Xidian University · Peng Cheng Laboratory, Shenzhen, China
Combining Mechanical and Agentic Specification Inference for Move
May 11, 2026Wolfgang Grieskamp, Teng Zhang, Vineeth KashyapProgram Synthesis Formal Verification
Aptos Labs, Palo Alto, USA
Prospective Compression in Human Abstraction Learning
May 11, 2026Leonardo Hernandez Cano, Ivan Zareski, Luisa El Amouri +6Program Synthesis Visual Program Synthesis
1Massachusetts Institute of Technology · 2Dalhousie University · University of Edinburgh +1
GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching
May 7, 2026Gabriel Bathie, Baptiste Mouillon, Nathanaël FijalkowGPU Acceleration Program Synthesis
CNRS, LaBRI, University of Bordeaux, France
ReaComp: Compiling LLM Reasoning into Symbolic Solvers for Efficient Program Synthesis
May 6, 2026Atharva Naik, Yash Mathur, Prakam +2Symbolic Reasoning LLM-Based Program Synthesis
Carnegie Mellon University · Independent Researcher
Library learning with e-graphs on jazz harmony
May 6, 2026Zeng Ren, Maddy Bowers, Xinyi Guan +1Program Synthesis
EPFL Lausanne, Vaud, Switzerland · MIT Cambridge, Massachusetts, USA
ProgramBench: Can Language Models Rebuild Programs From Scratch?
May 5, 2026John Yang, Kilian Lieret, Jeffrey Ma +9Software Engineering Agents Software Engineering Benchmarks
1Meta FAIR · 4Harvard University · 2Meta TBD +1
Learning to Theorize the World from Observation
May 5, 2026Doojin Baek, Gyubin Lee, Junyeob Baek +2Computational Cognitive Modeling World Model Learning
KAIST
CADFS: A Big CAD Program Dataset and Framework for Computer-Aided Design with Large Language Models
May 3, 2026Vladislav Pyatov, Gleb Bobrovskikh, Saveliy Galochkin +6Parametric CAD Modeling Program Synthesis
1Applied AI Institute · 2AI Foundation and Algorithm Lab · 3AXXX +1
Lifting Traces to Logic: Programmatic Skill Induction with Neuro-Symbolic Learning for Long-Horizon Agentic Tasks
May 2, 2026Jie-Jing Shao, Haiyan Yin, Yueming Lyu +5Program Synthesis LLM Agent Skill Learning
State Key Laboratory of Novel Software Technology, Nanjing University, China · Centre for Frontier AI Research, and Institute of High Performance Computing, Agency for Science, Technology and Research, Singapore · School of Intelligence Science and Technology, Nanjing University, China +2
DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
Apr 29, 2026Youyuan Zhang, Jialiang Sun, Hangrui Bi +4Automated Theorem Proving Program Synthesis
University of Toronto · UC Berkeley
Zero-to-CAD: Agentic Synthesis of Interpretable CAD Programs at Million-Scale Without Real Data
Apr 27, 2026Mohammadmehdi Ataei, Farzaneh Askari, Kamal Rahimi Malekshan +1Synthetic Data Generation Parametric CAD Modeling
Autodesk Research
SemML 2.0: Synthesizing Controllers for LTL
Apr 27, 2026Jan Křetínský, Tobias Meggendorfer, Maximilian ProkopProgram Synthesis Formal Verification
Masaryk University, Brno, Czech Republic · Technical University of Munich, Germany · Lancaster University Leipzig, Germany
LEGO: An LLM Skill-Based Front-End Design Generation Platform
Apr 25, 2026Jincheng Lou, Ruohan Xu, Jiecheng Ma +3Electronic Design Automation Code Generation
School of IC, Peking University · School of EECS, Peking University · School of Microelectronics, Xidian University +2
AutoRISE: Agent-Driven Strategy Evolution for Red-Teaming Large Language Models
Apr 23, 2026Tanmay Gautam, Alireza Bahramali, Sandeep AtluriLarge Language Model-Guided Optimization Program Synthesis
Responsible AI, Microsoft
Generalizing Numerical Reasoning in Table Data through Operation Sketches and Self-Supervised Learning
Apr 23, 2026Hanjun Cho, Gahyun Yoo, Hanseong Kim +1Table QA Self-Supervised Pre-Training
Seoul National University · Soongsil University
ChipCraftBrain: Validation-First RTL Generation via Multi-Agent Orchestration
Apr 21, 2026Cagri EryilmazElectronic Design Automation Code Generation
ChipCraftX San Francisco, CA
Gradient-Based Program Synthesis with Neurally Interpreted Languages
Apr 20, 2026Matthew V. Macfarlane, Clément Bonnet, Herke van Hoof +1Program Synthesis Differentiable Programming
AMLab, University of Amsterdam · Work completed while a visiting student at the University of Alberta. · Ndea +2
Symbolic Synthesis for LTLf+ Obligations
Apr 20, 2026Giuseppe De Giacomo, Christian Hagemeier, Daniel Hausmann +1Program Synthesis Formal Verification
University of Oxford, UK · University of Liverpool, UK · University of Gothenburg and Chalmers University of Technology, Sweden
LLM-Guided Strategy Synthesis for Scalable Equality Saturation
Apr 19, 2026Chenyun Yin, Youwei Xiao, Yuze Luo +2Compiler Optimization Large Language Model-Guided Optimization
Peking University Beijing, China · School of Integrated Circuits Peking University Beijing, China
Certified Program Synthesis with a Multi-Modal Verifier
Apr 17, 2026Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein +5Property-Based Testing LLM-Based Program Synthesis
National University of Singapore · Singapore · Neapolis University Pafos +2
Verification Modulo Tested Library Contracts
Apr 16, 2026Abhishek Uppar, Omar Muhammad, Sumanth Prabhu +3Program Synthesis Formal Verification
Indian Institute of Science, India · Relyance AI, India · University of Illinois Urbana-Champaign, Department of Computer Science, USA +1
Learning Hierarchical and Geometry-Aware Graph Representations for Text-to-CAD
Apr 11, 2026Shengjie Gong, Wenjie Peng, Hongyuan Chen +5Text-to-CAD Generation Program Synthesis
South China University of Technology · Zhuzhou CRRC Times Electric Co., Ltd. · Guangdong University of Technology
DeonticBench: A Benchmark for Reasoning over Rules
Apr 6, 2026Guangyao Dou, Luis Brena, Akhil Deo +4Logical Reasoning Legal Reasoning
Johns Hopkins University · Télécom Paris, Institut Polytechnique de Paris
Compositional Neuro-Symbolic Reasoning
Apr 2, 2026Anugyan Das, Omkar Ghugarkar, Vishvesh Bhat +1Neuro-Symbolic Reasoning Visual Reasoning
CoreThink AI · Stanford University
A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets
Apr 2, 2026Kaiwen Zhang, Guanjun LiuProgram Synthesis Compiler-Guided Program Synthesis
Tongji University, Shanghai, China

May 13, 2026J/K move · Enter open · S save

Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence

Jun He, Deying Yu

AI Assurance Program Synthesis

Open paper AskPDF arXiv

Automated program synthesis lowers the cost of producing implementations but introduces a harder governance problem: determining which generated artifacts are admissible. Natural-language specifications are ambiguous, and example-based tests sample only part of the behavioral space. Used alone, neither provides a sufficient control boundary. We introduce Protocol-Driven Development (PDD), where the primary software artifact is a machine-enforceable protocol rather than code. We define a protocol as the triplet P = (S, B, O), specifying structural, behavioral, and operational invariants. Their conjunction defines the admissible implementation space of a software component. Under PDD, implementations are replaceable realizations discovered through constrained search. An implementation is admitted only if it satisfies the protocol and produces a verifiable Evidence Chain of compliance. Admission is grounded in protocol satisfaction and recorded evidence rather than trust in the generator. For deployed systems, we extend the Evidence Chain into a Dynamic Evidence Ledger. Runtime verifiers append signed observations, invariant checks, and violations to the ledger, allowing monitorable obligations to be continuously attested. This connects live failures back to the generation loop without granting the generator runtime authority. Combining formal methods, property testing, runtime verification, policy-as-code, and software provenance, PDD defines a governance model for automated software engineering. Its organizing principle is that code is transient, while the protocol carries durable authority.