BRIDGE: Building Representations in Domain-Guided Verified Program Synthesis

Motivation

• Known: 기존 연구에서는 LLM을 이용한 코드 생성이 unit test 통과율을 기준으로 평가되어 왔으며, LEAN4와 같은 proof assistant에서는 코드, 명세, 정리, 증명이 하나의 dependent type theory 안에서 결합되어야 한다는 점이 알려져 있다.
• Gap: 기존 접근들은 code, specification, theorem/proof artifact를 독립적으로 생성하여 각 요소가 개별적으로는 타당해 보여도 서로 semantic drift가 발생하기 쉽고, 코드가 테스트를 통과해도 명세가 vacuous하거나 정리 진술이 의도한 속성을 포착하지 못하는 문제가 있었다.
• Why: LLM이 생성한 코드가 그럴듯해 보여도 미묘한 버그, edge case 누락, 가정 불일치를 포함할 수 있으므로, code뿐 아니라 명세와 증명까지 상호 일관되게 검증하는 verifiable coding 접근이 신뢰할 수 있는 자동 코드 생성을 위해 중요하다.
• Approach: BRIDGE는 verifiable coding을 단일 생성 문제가 아닌 artifact alignment 문제로 취급하여, Code(실행 가능한 구현), Specification(의도된 동작 명세), Theorem/Proof(정리 진술 및 증명 시도) 세 도메인 각각에 특화된 reasoning과 도메인 간 cross-check를 결합한 structured prompting framework를 제안한다.

Achievement

Figure 2. Main quantitative results. Functional scaffolding improves executable Lean synthesis, reaches comparable succe

1. Executable correctness 향상: 178개 문제로 구성된 자체 Lean benchmark에서 direct prompting 대비 최대 1.5배 executable correctness 향상을 달성했다.
2. 평가 효율성 개선: 비슷한 성공률을 약 2배 적은 Lean evaluation 횟수로 도달할 수 있음을 보였다.
3. Specification guided 생성 개선: specification guided code generation에서 최대 17.5 percentage point의 성능 향상을 보였다.
4. 공개 benchmark로의 전이: VERINA, CLEVER, DafnyBench 등 공개 검증 benchmark에서도 BRIDGE의 향상 효과가 전이됨을 확인했다.
5. Fine-tuning 내재화: BRIDGE 스타일 functional trace로 supervised fine-tuning 시 matched direct trace fine-tuning보다 우수했으며, Goedel-Code-Prover-8B는 VERINA에서 20.3%에서 29.4%로 향상되어 표현이 prompt 없이도 내재화될 수 있음을 시사했다.

How

Figure 3. Specification and theorem/proof diagnostics. Generated specifications often have useful discriminative power,

• 178개 LeetCode 스타일 문제로 구성된 자체 Lean benchmark(자연어 설명, Lean harness, 100개 oracle test 포함)와 공개 VERINA(187 tasks), CLEVER(161 tasks), DafnyBench pilot을 사용해 평가.
• CLAUDE SONNET 4, DEEPSEEK CODER V2, DEEPSEEK R1, LLAMA-3.1-70B, QWEN2.5 CODER 등 5개 모델로 실험.
• Code 도메인에서는 OCAML/HASKELL 영감의 functional scaffold와 PYTHON/C++ 영감의 imperative scaffold를 비교하되 최종 평가는 Lean 출력 기준으로 수행.
• Specification 도메인에서는 functional specification, design-by-contract pre/postcondition, invariant 기반 명세, dependent-type 제약, task-specific predicate 등 여러 스타일을 비교.
• Theorem/Proof 도메인은 elaboration, termination/totality 체크, test 통과, nonvacuity check, implementation relevance, 잘못된 구현 거부, sorry 없는 proof completion 등 다수 기준으로 진단.
• k개 독립 sample에 대해 pass@k로 성공 여부 평가.
• BRIDGE 스타일 functional trace로 supervised fine-tuning을 수행하여 matched direct trace fine-tuning과 비교.

Originality

• 검증 가능한 코드 생성을 Code, Specification, Theorem/Proof 세 도메인으로 명시적으로 분해하고 도메인별 특화 reasoning과 cross-artifact check를 결합한 구조화된 프레임워크를 제안한 점이 독창적이다.
• LEAN4 executable correctness(elaboration, termination/totality, benchmark test 통과)라는 단순 unit test 정확도보다 엄격한 code metric을 정의하여 evaluation 기준을 강화했다.
• OCAML/HASKELL 스타일 functional scaffold와 PYTHON/C++ 스타일 imperative scaffold를 비교함으로써 reasoning structure 자체가 Lean 코드 생성 품질에 미치는 영향을 체계적으로 분석했다.
• prompting뿐 아니라 fine-tuning 단계에서도 BRIDGE 표현이 내재화될 수 있음을 보여, 단순 prompt engineering을 넘어선 representation-level 기여를 제시했다.

Limitation & Further Study

• BRIDGE는 완전한 semantic verification이나 verified compiler가 아니며, 중간 프로그램은 인증된 소스 artifact가 아닌 reasoning scaffold에 불과하다는 한계가 명시되어 있다.
• 대규모의 full semantic proof completion은 여전히 open problem으로 남아 있으며, 논문은 이를 스스로 인정하고 있다.
• 평가된 모델과 benchmark가 제한적(5개 모델, 178~200개 내외 문제 규모)이어서 더 크고 다양한 실제 산업 코드베이스로의 일반화 가능성은 추가 검증이 필요하다.
• theorem/proof 도메인의 성과가 완전한 proof automation이 아니라 진단적 성격(diagnostics)에 머물러 있어, 실제 증명 완결률 향상으로 이어지는지는 후속 연구가 필요하다.

Evaluation

총평: LEAN4 기반 검증 가능한 코드 생성을 세 도메인으로 분해하는 구조화된 접근으로 실질적인 executable correctness 향상과 평가 효율성 개선을 실험적으로 입증했으며, prompting을 넘어 fine-tuning까지 확장 가능함을 보인 의미 있는 연구이나 완전한 formal verification까지는 아직 갈 길이 남아있다.