[기술 요약] 자연어에서 검증된 코드로: Dafny 기반 형식 검증을 이용한 AI 지원 문제-코드 생성 연구

1. 문제 정의 (Problem Statement)

현재 대규모 언어 모델(LLM)은 소프트웨어 공학 분야에서 유망한 도구로 떠오르고 있으나, '환각(Hallucination)' 현상으로 인해 생성된 코드가 문법적으로는 그럴듯해 보여도 논리적으로 틀린 경우가 많다는 치명적인 결함이 있습니다.

특히, 보안이 중요한 시스템(항공우주, 암호화 라이브러리 등)에서는 단순한 테스트를 넘어 수학적 증명을 통한 **형식 검증(Formal Verification)**이 필수적입니다. 하지만 형식 검증을 위한 명세(Specification, 예: 루프 불변량, 사전/사후 조건)를 작성하는 작업은 매우 복잡하고 전문적인 지식을 요구하며, 이는 개발자에게 큰 비용 부담을 줍니다. 따라서 **"비정형적인 자연어 요구사항을 어떻게 하면 수학적으로 증명 가능한 정확한 코드(Dafny 등)로 자동 변환할 것인가?"**가 본 연구의 핵심 문제입니다.

2. 연구 방법론 (Methodology)

본 연구는 자연어 요구사항을 Dafny 언어를 이용한 검증된 코드로 변환하기 위해 다음과 같은 체계적인 프레임워크를 제안합니다.

A. NL2VC-60 데이터셋 구축

• 데이터 소스: UVa Online Judge의 복잡한 알고리즘 문제들을 활용.
• 일반화 과정: 경쟁 프로그래밍 특유의 부수적인 설명(입력 형식, 제약 조건 등)을 제거하고, 핵심 계산 로직에 집중한 **'요구사항 중심의 일반적 설명(Generic Description)'**으로 재구성.
• 품질 보증: 저자들이 직접 60개의 고품질 Dafny 프로그램을 수동으로 작성하여 정답(Ground-truth)을 구축함.

B. 계층적 프롬프팅 전략 (Tiered Prompting Strategy)

모델의 성능을 단계별로 측정하기 위해 세 가지 전략을 사용합니다.

1. Contextless Prompting (RQ1): 아무런 구조적 힌트 없이 자연어 설명만 제공 (Baseline).
2. Signature Prompting (RQ2): 함수의 입력/출력 타입이 정의된 **메서드 시그니처(Method Signature)**를 제공하여 구조적 앵커 역할 수행.
3. Self-Healing Prompting (RQ3): Dafny 검증기(Verifier)에서 발생한 에러 메시지를 모델에게 다시 피드백하여, 모델이 스스로 코드를 수정하도록 하는 반복적 피드백 루프 적용.

C. 이중 레이어 검증 (Dual-layer Validation)

• 형식 레이어 (Formal Layer): Dafny 검증기를 통해 코드가 수학적 명세를 만족하는지 증명.
• 기능 레이어 (Functional Layer): uDebug 플랫폼의 테스트 케이스를 통합하여, 모델이 '공허한 검증(Vacuous Verification, 즉, 아무 의미 없는 명세를 작성해 검증을 통과하는 행위)'을 하지 않고 실제 기능적으로도 정확한지 확인.

3. 주요 기여 (Key Contributions)

1. 최초의 벤치마크 제시: 단순 교과서 수준을 넘어 실제 알고리즘 문제의 복잡성을 반영한 NL2VC-60 데이터셋을 공개.
2. 오류 분류 체계 구축: Dafny 생성 과정에서 발생하는 오류를 **구문 오류(Syntax), 의미/타입 오류(Semantic/Type), 검증 오류(Verification)**의 세 단계로 분류한 최초의 진단 데이터셋 제공.
3. 검증 루프 통합: uDebug를 활용하여 형식적 증명과 기능적 정확성을 동시에 보장하는 엄격한 평가 파이프라인 구축.

4. 연구 결과 (Results)

7개의 오픈 웨이트(Open-weight) LLM을 대상으로 실험한 결과는 다음과 같습니다.

• 프롬프팅의 효과:
  • Contextless 환경에서는 대부분의 모델이 0%에 가까운 성공률을 보이며 실패함.
  • Signature Prompting을 적용하자 성능이 극적으로 반전됨. 특히 Qwen 3.5-9B 모델이 72.73%의 높은 성공률을 기록함.
• Self-Healing의 강력함:
  • 에러 피드백을 통한 자기 수정 능력이 탁월함.
  • Gemma 4-31B 모델은 Contextless 환경에서도 스스로 수정하여 **90.91%**라는 경이로운 검증 성공률을 달성함.
  • GPT-OSS-120B 모델은 시그니처 가이드와 결합했을 때 성공률이 0%에서 **81.82%**로 급상승함.
• 오류 패턴: 초기에는 구문 오류가 지배적이지만, 모델이 코드를 수정해 나갈수록 논리적 증명 단계에서의 '검증 오류'로 병목 현상이 이동함.

5. 연구의 의의 (Significance)

본 연구는 **"LLM이 단순한 코딩 보조 도구를 넘어, 고신뢰성 소프트웨어 개발을 위한 숙련된 조수(Apprentice)가 될 수 있음"**을 입증했습니다.

특히, 모델의 크기(Parameter)보다 형식 논리에 대한 사전 학습 밀도와 구조적 가이드(Signature), 그리고 **검증기와의 반복적 피드백(Verification-in-the-Loop)**이 결합되었을 때 비로소 수학적으로 증명 가능한 코드를 생성할 수 있음을 보여주었습니다. 이는 향후 고신뢰성 소프트웨어 개발 비용을 획기적으로 낮출 수 있는 중요한 기술적 토대를 제공합니다.