![[2511.21104] BRIDGE: Building Representations In Domain Guided Program Synthesis](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2511.21104] BRIDGE: Building Representations In Domain Guided Program Synthesis
Summary
The paper presents BRIDGE, a framework for improving program synthesis through structured prompting, enhancing correctness and efficiency in generating verified code.
Why It Matters
BRIDGE addresses the limitations of existing program synthesis methods by integrating code generation, specifications, and theorem statements into a unified framework. This is crucial for advancing the reliability of large language models in formal verification tasks, which is increasingly important in software development and AI safety.
Key Takeaways
- BRIDGE improves Lean executable correctness by nearly 1.5x over existing methods.
- The framework enhances sample efficiency, requiring fewer samples for verified solutions.
- Specification-driven prompting significantly boosts Python pass rates by up to 17.5%.
- Supervised fine-tuning on BRIDGE-style reasoning traces yields higher pass success rates.
- BRIDGE lays the groundwork for future advancements in verified synthesis and proof generation.
Computer Science > Machine Learning arXiv:2511.21104 (cs) [Submitted on 26 Nov 2025 (v1), last revised 25 Feb 2026 (this version, v2)] Title:BRIDGE: Building Representations In Domain Guided Program Synthesis Authors:Robert Joseph George, Carson Eisenach, Udaya Ghai, Dominique Perrault-Joncas, Anima Anandkumar, Dean Foster View a PDF of the paper titled BRIDGE: Building Representations In Domain Guided Program Synthesis, by Robert Joseph George and 5 other authors View PDF HTML (experimental) Abstract:Large language models (LLMs) are good at generating code, but remain brittle for formal verification in systems like Lean4. A core scalability challenge is that verified synthesis requires consistent outputs across multiple artifacts: executable code, precise specifications, theorem statements, and ultimately proofs. Existing approaches rarely treat these as a unified pipeline. We present BRIDGE, a structured prompting framework that decomposes verification into three interconnected domains: Code (implementations), Specifications (formal intent), and Theorem Statements (constructive correctness claims), and elicits domain-specific intermediate reasoning to connect them. In Lean4, BRIDGE often adopts a code-first workflow, using the generated implementation as a semantic anchor for downstream specification and theorem statement generation. Across 178 algorithmic problems and five LLMs, BRIDGE improves Lean executable correctness by nearly 1.5x (pass at 5) over direct baselines...
