Technical Summary: BRIDGE – Building Representations in Domain-Guided Verified Program Synthesis

1. Problem Statement

Large Language Models (LLMs) are increasingly capable of generating code, but in the context of formal verification, generated programs often appear correct while harboring subtle bugs, missing edge cases, or mismatched assumptions. In proof assistants like Lean, program verification is not a single-generation task but a multi-artifact prediction problem. A successful verification requires the mutual consistency of four coupled artifacts:

1. Executable Code: The implementation.
2. Formal Specification: Behavioral constraints (preconditions, postconditions, invariants).
3. Theorem Statements: Claims connecting the code to the specification.
4. Proof Attempts: Scripts checked by the kernel to verify the claims.

Current LLM systems struggle in this setting because treating these artifacts independently leads to semantic drift. A model might generate code that passes tests but fails Lean's termination checks, a specification that typechecks but is vacuous, or a theorem that is provable but irrelevant to the original task. The core challenge is translating informal intent into a sequence of artifacts where syntax, types, recursion structures, contracts, and proof obligations remain aligned.

2. Methodology: The BRIDGE Framework

The authors propose BRIDGE, a structured prompting framework that decomposes the verifiable coding process into three linked domains: Code, Specification, and Theorem/Proof. Rather than asking a model to jump directly from natural language to a final proof, BRIDGE enforces a structured reasoning flow where artifacts constrain and check one another.

2.1 Domain Decomposition

• The Code Domain: Produces the final Lean implementation. BRIDGE compares direct Lean generation against intermediate reasoning scaffolds.
  • Functional Scaffolds: Inspired by OCaml and Haskell, these encourage immutable data, pattern matching, structural recursion, and compositional definitions. This aligns naturally with Lean's dependent type theory and termination discipline.
  • Imperative Scaffolds: Inspired by Python and C++, these encourage loops and mutation.
  • Key Insight: The intermediate program is a reasoning scaffold, not a certified source artifact. It does not need to compile in its source language; its purpose is to bias the model toward a structure that Lean can verify.
• The Specification Domain: Describes intended guarantees. BRIDGE utilizes various reasoning styles (Design by Contract, Property-Based Testing, Test-Driven Development, Defensive Programming) to make assumptions, edge cases, and guarantees explicit. Specifications are evaluated not just for type-checking, but for non-vacuity and their ability to distinguish correct implementations from plausible incorrect ones.
• The Theorem/Proof Domain: Makes correctness claims explicit. Models are prompted to propose properties (bounds, invariants, monotonicity) and attempt proofs. This domain serves as a diagnostic for downstream verification, checking if generated theorems can be elaborated and if proofs can be completed without sorry (placeholder for unproven goals).

2.2 Reasoning Hypothesis

The central hypothesis is that verification success depends on the structure of intermediate reasoning. Direct generation forces the model to recover the algorithm, express it in Lean, satisfy type/termination constraints, and infer specifications simultaneously. BRIDGE separates these pressures. Specifically, the authors find that an ordering beginning with functional code generation is particularly effective: the model first generates Lean-compatible code using a functional scaffold, then uses that implementation as a semantic anchor for specifications and theorem statements.

3. Key Contributions

1. A Multi-Artifact Framework: BRIDGE introduces a structured approach to verifiable coding that decomposes the task into linked Code, Specification, and Theorem/Proof domains, using cross-artifact reasoning to reduce semantic drift.
2. Functional Reasoning Improves Synthesis: On a 178-problem Lean benchmark, functionally aligned intermediate reasoning improves Lean executable correctness by up to 1.5× compared to direct prompting. It achieves comparable success rates with roughly 2× fewer Lean evaluations, indicating improved sample efficiency.
3. Improved Downstream Artifacts: BRIDGE-style prompting produces more useful formal artifacts. It yields more theorem statements that successfully elaborate in Lean and more completed proof attempts aligned with the implementation. Specification-guided prompting also improves conventional code generation (up to 17.5 percentage points in Python).
4. Learnable Inductive Bias: Supervised Fine-Tuning (SFT) on BRIDGE-style functional traces outperforms matched direct trace fine-tuning (e.g., a 9.1 percentage point gain on the VERINA benchmark). This suggests the framework captures a learnable inductive bias rather than being a one-time prompt effect.

4. Experimental Results

The authors evaluated BRIDGE on a custom 178-problem Lean benchmark and public benchmarks including VERINA, CLEVER, and a solver-backed DAFNYBENCH pilot.

• Executable Correctness: Using functional scaffolds, the pass rate on the 178-task benchmark increased from 44/178 (Direct) to 59/178 (Functional) in the minimal core setting. With repair rounds, the gap remained positive (83/178 vs. 77/178).
• Sample Efficiency: Functional scaffolds reached comparable success with roughly half the number of Lean evaluations compared to direct prompting, reducing the cost of checking candidates.
• Transferability: The benefits transferred to public benchmarks. On VERINA, functional prompting improved pass rates by up to 6.3 percentage points. On DAFNYBENCH, it improved verified pass@5 by 7.3 percentage points.
• Proof Diagnostics: In a full proof experiment, functional code yielded more completed proofs without sorry (34/178 vs. 20/178 with functional SFT prover) and produced shorter, cleaner implementations that were easier for proof models to discharge.
• SFT Gains: Fine-tuning on functional traces improved performance on VERINA from 20.3% to 29.4%, demonstrating that the reasoning structure can be internalized by the model.

5. Significance and Limitations

The paper claims that reasoning representation matters. By structuring the generation process to align with the target verification system (Lean), BRIDGE reduces syntax, type, and termination failures. The framework provides a verification-oriented inductive bias that connects code, specifications, theorem statements, and proof attempts, making the pipeline easier to inspect and more amenable to downstream proof search.

Modest Claims and Limitations:

• Not Full Verification: BRIDGE studies the "front end" of verified synthesis. It does not claim to solve full semantic verification at scale. Generated specifications and theorem statements may still be weak, vacuous, or overly shaped by the implementation.
• Scope: The evaluation focuses on local, algorithmic tasks. The authors have not yet tested BRIDGE on large formal libraries, rich stateful programs, or long-horizon proofs.
• Model Dependence: Results vary across models, prompts, and search budgets. BRIDGE is presented as a useful inductive bias rather than a universal improvement independent of the underlying model.
• Future Work: The authors note that the next step is to close the loop between BRIDGE artifacts and stronger proof search, potentially integrating tool-using theorem provers, formal library retrieval, and reinforcement learning from verifiable rewards.

In summary, BRIDGE demonstrates that decomposing verified coding into structured, domain-aligned reasoning steps significantly improves the quality and verifiability of generated artifacts, offering a pathway toward more reliable formal synthesis without requiring full automation of the proof process.