BRIDGE: Building Representations In Domain Guided Program Verification

TL;DR

BRIDGE reframes automated verified program synthesis as a three-domain inference task over Code, Specifications, and Proofs, using domain-specific prompting to maintain semantic coherence across Lean4-based verification tasks. Empirical results across 178 LeetCode problems and five LLMs show that functional reasoning improves Lean4 code synthesis and inference efficiency, while specification-driven prompts boost Python results and provide cross-domain benefits. The findings indicate that aligning reasoning paradigms with programming and proof structures yields multiplicative gains and suggests a scalable path toward RL-based internalization of verification strategies. The work lays a foundation for domain-aware training and iterative improvement toward end-to-end verified AI systems.

Abstract

Large language models (LLMs) have achieved impressive results in code generation, yet struggle with program verification, especially in interactive proof frameworks such as Lean4. A central challenge is scalability: verified synthesis requires not just code, but also precise specifications and correctness proofs, and existing approaches rarely span all three domains. We present BRIDGE, the first systematic study of structured prompting for scalable verified program generation. BRIDGE decomposes verification into three interconnected domains: Code (executable implementations), Specifications (formal intent statements), and Proofs (constructive correctness arguments). Our key idea is to elicit distinct reasoning behaviors functional, specification-driven, and proof-oriented as intermediate representations that preserve semantic structure and connect these domains. Through systematic ablations, we show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods. For example, functional reasoning improves correctness of code in formal languages (Lean4) by nearly 1.5x (pass@5) over direct baselines. In inference-time compute, functional reasoning is also 2x more efficient, achieving higher pass rates with fewer generations and lower total sampling budgets. Similarly, we find that specification-driven prompting boosts Python coding pass rates by up to 17.5%. These findings suggest that structured domain alignment is a promising direction for advancing verified synthesis. BRIDGE establishes a foundation for training via expert iteration or RLVR, enabling models to internalize these reasoning strategies across code, specifications, and proofs.

Figures (12)

• Figure 1: Functional reasoning improves verification accuracy while reducing inference-time compute. Lines show inference-time scaling via n-way parallel generation without iterative refinement. Circular markers (dots) report pass@5 with the Lean +API available in context (tool access) and with 3 rounds of error correction. The blue annotation applies only to the dot markers. Overall, functional reasoning reaches performance comparable to direct generation with roughly half the total sampling budget, improving both efficiency and accuracy.
• Figure 2: Minimum key pushes LeetCode problem.
• Figure 3: Functional reasoning content from Claude 4.
• Figure 4: Specification reasoning content from Claude 4.
• Figure 5: Theorem reasoning content from Claude 4.