자연어에서 검증된 코드까지: Dafny 기반 Formal Verification으로 AI 코드 생성 신뢰성 높이기

TL;DR Highlight

LLM이 생성한 코드를 수학적으로 100% 증명하는 Formal Verification 파이프라인 — Gemma 4-31B가 90.91% 성공률 달성.

Who Should Read

LLM이 생성한 코드의 정확성을 보장해야 하는 백엔드/시스템 개발자, 또는 항공·암호화·보안처럼 고신뢰 소프트웨어를 개발하는 팀에서 AI 코드 생성 자동화를 검토 중인 엔지니어.

Core Mechanics

자연어 설명만 던져주면(Contextless Prompting) 대부분 LLM이 Dafny 코드 생성에 완전히 실패함 — GPT-OSS-120B 포함 5개 모델이 0% 성공률.
Method Signature(함수명, 입출력 타입만 제공)를 힌트로 주면 성공률이 극적으로 반전됨 — GPT-OSS-120B가 0%→63.64%, Qwen 3.5-9B가 72.73%까지 상승.
Self-Healing(Dafny 검증기 에러 메시지를 LLM에 다시 피드백해서 반복 수정)이 가장 강력한 전략 — Gemma 4-31B는 contextless 상태에서도 90.91% 달성.
'Vacuous Verification'(아무 의미없는 trivial 스펙으로 검증기를 속이는 현상) 방지를 위해 uDebug 커뮤니티 테스트 스위트를 이중 검증 레이어로 통합, 형식 검증 + 실제 edge case 테스트를 동시에 수행.
모델 크기보다 사전학습 데이터 밀도가 중요함 — 31B짜리 Gemma 4가 120B짜리 GPT-OSS를 contextless 시나리오에서 압도. Dafny 관련 GitHub 저장소는 불과 약 779개로 매우 희소.
에러 유형을 3단계로 분류: Syntax Error(구조 문법 오류) → Semantic/Type Error(타입 불일치) → Verification Failure(컴파일은 되지만 SMT 솔버가 증명 불가). Signature 제공 시 Syntax Error가 줄고 Verification Error가 늘어나는 패턴 확인.

Evidence

Gemma 4-31B: Self-Healing(Contextless 기반) 시 T=0.2와 T=0.6에서 verify@5 90.91% 달성 (11문제 중 10개 성공).
GPT-OSS-120B: Contextless에서 0% → Signature Prompting에서 63.64% → Signature-Guided Self-Healing에서 81.82%로 단계별 상승.
Qwen 3.5-9B(9B 소형 모델): Signature Prompting만으로 verify@5 72.73% 달성 — 30B·120B 모델을 능가하는 결과.
NL2VC-60 데이터셋 구축에 저자들이 약 350 person-hours(300시간 개발 + 50시간 충돌 해결) 투입 — Dafny formal spec 작성의 현실적 난이도를 방증.

How to Apply

LLM으로 알고리즘 코드를 생성할 때 함수 시그니처(파라미터 타입, 반환 타입)를 프롬프트에 포함시켜라 — contextless 대비 성공률이 수십 배 올라간다.
코드 생성 파이프라인에 Dafny 같은 형식 검증기를 루프로 연결하고, 검증 실패 시 에러 메시지를 그대로 LLM에 피드백해서 최대 10회 자동 재시도하는 Self-Healing 에이전트를 구성하라.
형식 검증을 통과했더라도 trivial spec으로 속인 케이스가 있을 수 있으므로, uDebug처럼 커뮤니티 기반 edge case 테스트 스위트를 이중 검증 레이어로 추가해라 — 특히 고신뢰 소프트웨어라면 필수.

Code Example

snippet

# Self-Healing 프롬프트 구조 예시 (Python pseudo-code)

import subprocess

def self_healing_dafny(problem_desc: str, method_signature: str, llm_client, max_iter=10):
    # Step 1: Signature Prompt로 초기 코드 생성
    prompt = f"""You are an expert in Dafny. Output ONLY raw Dafny code.
Generate one Dafny source file for the following task.

Task Description: {problem_desc}
Method Signature: {method_signature}"""

    code = llm_client.generate(prompt)

    for attempt in range(max_iter):
        # Step 2: Dafny 검증기 실행
        result = subprocess.run(
            ["dafny", "verify", "temp.dfy"],
            input=code, capture_output=True, text=True
        )

        if "0 errors" in result.stdout:
            print(f"✅ Verified at attempt {attempt+1}")
            return code  # 검증 성공

        # Step 3: 에러 메시지를 피드백으로 Self-Healing
        error_msg = result.stdout + result.stderr
        heal_prompt = f"""The previous Dafny code failed verification with the following errors:
{error_msg}

Previous code:
{code}

Please repair the code to satisfy all specifications. Output ONLY the raw fixed Dafny code."""
        code = llm_client.generate(heal_prompt)

    print("❌ Failed after max iterations")
    return None

Terminology

Formal Verification코드가 올바르다는 것을 수학적으로 100% 증명하는 기법. 테스트는 '몇 가지 케이스에서 됐다'이지만, Formal Verification은 '모든 경우에 반드시 된다'를 수학으로 보장.

DafnyMicrosoft Research가 만든 프로그래밍 언어. 코드와 함께 '이 함수는 항상 이런 결과를 낸다'는 명세(spec)를 같이 작성하면, 내장 증명기가 자동으로 맞는지 확인해줌.

SMT Solver수학 공식이 항상 참인지 자동으로 풀어주는 소프트웨어. Dafny 내부에서 Z3가 이 역할을 함. 체스 엔진처럼 모든 경우를 탐색해서 반례가 있으면 알려줌.

Loop Invariant반복문이 몇 번 돌든 항상 참이어야 하는 조건. 예: '루프 중간에 배열 인덱스는 항상 0~n 사이'. Dafny가 증명을 완성하려면 개발자가 이걸 직접 작성해야 해서 가장 어려운 부분.

Vacuous Verification검증기를 통과했지만 실제론 아무것도 증명 안 한 상태. 예: ensures true처럼 항상 참인 조건만 써서 검증기를 '속이는' 것. LLM이 자주 쓰는 꼼수.

Self-Healing코드 검증 실패 시 에러 메시지를 LLM에 다시 넣어서 스스로 수정하게 하는 반복 루프. 사람이 컴파일 에러 보고 고치는 과정을 자동화한 것.

verify@kk번 시도 안에 검증 성공한 문제 비율. pass@k(코딩 테스트 통과율)의 Formal Verification 버전.

Related Resources

Original Abstract (Expand)

Large Language Models (LLMs) show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code. To enforce model honesty, formal verification requires LLMs to synthesize implementation logic alongside formal specifications that are subsequently proven correct by a mathematical verifier. However, the transition from informal natural language to precise formal specification remains an arduous task. Our work addresses this by providing the NaturalLanguage2VerifiedCode (NL2VC)-60 dataset: a collection of 60 complex algorithmic problems. We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy: contextless prompts, signature prompts providing structural anchors, and self-healing prompts utilizing iterative feedback from the Dafny verifier. To address vacuous verification, where models satisfy verifiers with trivial specifications, we integrate the uDebug platform to ensure functional validation. Our results show that while contextless prompting leads to near-universal failure, structural signatures and iterative self-healing facilitate a dramatic performance turnaround. Specifically, Gemma 4-31B achieved a 90.91\% verification success rate, while GPT-OSS 120B rose from zero to 81.82\% success with signature-guided feedback. These findings indicate that formal verification is now attainable for open-weight LLMs, which serve as effective apprentices for synthesizing complex annotations and facilitating high-assurance software development.