BRIDGE: Building Representations In Domain Guided Program Synthesis

Abstract

BRIDGE is a framework for improving verified program synthesis with large language models. The approach decomposes verification into three interconnected domains: Code (implementations), Specifications (formal intent), and Theorem Statements. BRIDGE uses a code-first workflow, using the generated implementation as a semantic anchor for downstream specification and theorem statement generation. Evaluated across five LLMs on 178 algorithmic problems, the method achieves nearly 1.5x better Lean executable correctness compared to baselines and demonstrates 2x more sample-efficient inference. The framework also improves Python pass rates by up to 17.5% through specification-driven prompting. Supervised fine-tuning with BRIDGE-style reasoning yields nearly 1.5x higher Lean pass success than code-only SFT.