기술 요약: 모델 주도 공학을 통한 정형 기법 가이드형 바이브 코딩 (Formal-Method-Guided Vibe Coding via Model-Driven Engineering)

1. 문제 정의

본 논문은 개발자가 자연어로 의도를 설명하고 최소한의 검토만으로 생성된 코드를 수용하는 워크플로우인 "바이브 코딩(vibe coding)"의 급격한 도입과, 안전 필수 시스템(DO-178C, IEC 61508, ISO 26262와 같은 표준에 의해 규제되는)의 엄격한 보증 요구사항 사이의 결정적인 간극을 다룬다.

LLM이 생성한 코드를 검증하려는 기존 방식들은 두 가지 주요한 구조적 장벽에 직면해 있다:

1. 검증 친화적 언어의 부재: Dafny, Verus, 또는 Lean과 같은 언어를 대상으로 하는 방법론들은 LLM 사전 학습 데이터가 부족하고, 구성적 추론(compositional reasoning) 능력이 떨어지며, 기존 산업용 툴체인(주로 Java, C, C++ 사용)과의 통합이 부족하다.
2. 사후 필터링(Post-Hoc Filtering): 생성 후에 검증 계층을 추가하는 기존 도구들은 검증을 피드백 신호가 아닌 필터로 취급하며, LLM이 올바른 방향으로 나아가도록 유도하는 메커니즘을 제공하지 못한다.

결과적으로, 가이드가 없는 바이브 코딩은 인증에 필요한 형식적 정당성 보증과 추적 가능한 증거를 결여한 결과물을 생성한다.

2. 방법론: Forge 파이프라인

저자들은 LLM 생성과 확립된 모델 주도 공학(MDE) 인프라를 통합하는 폐쇄 루프 파이프라인인 Forge(Formal method Oriented Refinement loop for GEnerated code)를 제시한다. 핵심 철학은 LLM을 "초안 생성기(draft generator)"로, MDE 체인을 "판별기(discriminator)"로 취급하는 것이다. 이를 통해 개발자는 메인스트림인 Java를 사용하면서도, 직접 볼 필요 없이 추출된 모델 위에서 형식 검증이 작동하도록 한다.

파이프라인은 세 가지 패밀리로 그룹화된 7개의 단계로 구성된다:

단계 1: 요구사항 도출 (Requirements Elicitation)

자연어 요구사항을 정형화된 요구사항 세트로 구조화한다.

단계 2: 하향식 코드 합성 (Top-Down Code Synthesis - Vibe Coding)

LLM(특히 Anthropic Claude Code)이 5단계 프롬프트 시퀀스에 따라 Java 소스 코드를 생성한다:

1. 아키텍처(Architecture): 패키지/클래스 구조 및 요구사항-클래스 매핑.
2. 스켈레톤(Skeleton): 스텁(stub) 메서드가 포함된 컴파일 가능한 Java.
3. 리프(Leaves): 센서, 액추에이터 및 동작 로직.
4. 컨트롤러(Controller): 모드 중첩 상태 머신 로직.
5. 리뷰(Review): 임의로 설정된 기본값에 대한 자가 보고.

제약 사항: 충실한 모델 추출을 보장하기 위해, LLM은 특정 Java 서브셋(예: 람다, 스트림, 패턴 매칭 금지; 상태 머신은 2단계 if-else 구조 사용)으로 제한된다. 이 서브셋은 런타임 예측 가능성보다는 모델 추출의 용이성을 위해 결정되었다.

프리플라이트 체크 (2a–2c): 생성된 코드는 컴파일, 요구사항-코드 커버리지 확인, 그리고 추출 규칙에 따른 구조적 린팅(linting) 과정을 거친다.

단계 3–5: 추출 및 변환 (Extraction and Transformation)

이 단계는 인간의 개입 없이 Java 소스를 정형 산출물로 변환한다:

• 단계 3 (Text-to-Model): 커스텀 Spoon-to-EMF 브릿지가 Java AST(sealed interface 및 record와 같은 Java 17+ 기능 지원)를 파싱하여 Eclipse Modeling Framework(EMF) 모델로 변환한다.
• 단계 4 (Model-to-Model): Epsilon Transformation Language(ETL) 스크립트가 Java EMF 모델을 RoboChart 상태 머신으로 변환하며, 모드, 전이(transition), 가드(guard)를 식별한다.
• 단계 5 (Model-to-Text): 세 가지 독립적인 정형 산출물이 생성된다:
  1. Dafny 명세(Specifications): 연역적 검증을 위해 Java EMF 모델에서 직접 생성됨.
  2. CSP-M 스크립트: 행동 정제 확인(behavioral refinement checking)을 위해 RoboChart 모델에서 생성됨.
  3. Isabelle/HOL 이론: Z-Machine 표기법을 사용하여 RoboChart 모델로부터 생성된 정리 증명용 이론.

단계 6–7: 검증 및 폐쇄 루프 정제 (Verification and Closed-Loop Refinement)

• 단계 6 (검증): 세 가지 산출물이 각각의 도구에 의해 검증된다:
  • Dafny (Z3): 함수 수준의 계약(전제/사후 조건, 종료성)을 확인한다.
  • FDR4: CSP 정제를 통해 행동적 특성(데드락 프리, 발산 프리)을 확인한다.
  • Isabelle/HOL: 심볼릭 전이 관계에 대한 구조적 불변량과 데드락 프리를 증명한다.
  • 공허성 감사 (6d, Vacuity Audit): 증명이 비자명함(예: 단순히 true나 True가 아님)을 보장한다.
• 단계 7 (정제): 검증 실패는 구조화되고 실행 가능한 수정 프롬프트(JSON/Markdown 형태)로 변환된다. 이 프롬프트는 추적성 체인을 통해 특정 요구사항 및 소스 라인과 연결되어 LLM에 다시 전달되어 코드를 재생성하게 한다. 이 루프는 모든 검증기가 통과하거나 최대 반복 횟수에 도달할 때까지 계속된다.

3. 주요 기여

1. 폐쇄형 초안-및-판별 루프 (Closed Draft-and-Discriminate Loop): LLM이 생성한 메인스트림 코드를 MDE 인프라를 통해 정형 검증 가능하게 만들고, 검증 실패를 사후 필터가 아닌 반복적 수정 신호로 사용하는 새로운 아키텍처를 제시한다.
2. Spoon-to-EMF 브릿지: 현대적 Java(17+)를 지원하는 최초의 EMF 네이티브 텍스트-투-모델 변환 도구로, legacy 도구인 MoDisco가 남긴 공백을 메우며 sealed interface, record, 패턴 구문을 처리할 수 있다.
3. 상호 보완적인 3중 검증 설계: Dafny, FDR4, Isabelle/HOL을 병렬로 사용하는 시스템을 채택했다. 본 논문은 이 검증기들이 서로 대체 불가능함을 입증한다(예: Dafny는 계약 위반을, FDR4는 행동적 데드락을, Isabelle은 터미널 상태에서의 구조적 데드락을 포착함).
4. 엔드 투 엔드 추적성: 자연어 요구사항부터 생성된 소스, 중간 모델, 정형 증명까지 이어지는 완전한 추적 체인을 구축하여 요구사항별 수정 지침을 가능하게 한다.
5. 경험적 검증: 검증 피드백에 의해 구동되어 여러 독립적인 실행에 걸쳐 완전히 검증된 코드로 수렴한다는 것을 보여주는 실험적 근거를 제시한다.

4. 실험 결과

파이프라인은 복잡도가 증가하는 세 가지 외부 작성 케이스 스터디를 통해 평가되었다:

• SRanger: 단일 컨트롤러 지상 로봇 (요구사항 23개, 약 220 LOC).
• Last Response Engine (LRE): AUV 안전 거버너 (요구사항 51개, 약 613 LOC).
• Chemical Detector: 멀티 컨트롤러 자율 로봇 (요구사항 81개, 약 618 LOC).

주요 결과:

• 수렴성: 15회의 독립적인 실행(케이스 스터디당 5회) 전체에서, 모든 15회의 실행이 2~3회의 반복(중앙값 2) 내에 완전히 검증된 코드로 수렴했다.
• 피드백의 필요성: "콜드-베이스라인(cold-baseline)" 실험(검증 피드백 없이 30회 실행)에서는 단 한 건의 실행도 수렴하지 못했다. 단일 패스 생성은 검증된 코드를 생성하는 데 실패했다.
• 검증기의 역할: "컴파일 전용(compile-only)" 절제 실험(검증 피드백은 숨기되 컴파일 체크는 유지)에서, 15회의 실행 모두가 적어도 하나의 정형 검증기를 통과하지 못했다. 이는 단순한 반복이나 컴파일이 아니라, 검증 피드백이 수렴을 주도한다는 것을 확인시켜 준다.
• 결함 탐지: 세 검증기는 서로 다른 결함을 포착했다. 예를 들어, 터미널 모드에서의 구조적 데드락은 Dafny와 FDR4는 놓쳤으나 Isabelle이 포착했으며, 이는 특정 수정(idle self-loop 추가)을 요구했다.
• 비용: 수렴에는 보통 2~3회의 반복이 소요되었다. 벽시계 시간(wall-clock time)은 실행당 약 1분에서 15분 사이였으며, 구조적 문제가 있을 경우 Isabelle의 증명 시간이 주된 요인이었다.

5. 의의 및 주장

본 논문은 LLM 기반 워크플로우에서 정형 검증이 위치해야 할 구조적 논거를 제시한다: LLM 내부도 아니고, 사후 필터도 아닌, 폐쇄 루프 정제 과정의 판별기로서 존재해야 한다.

• 인증 관련성: 본 파이프라인은 안전 표준에서 인정하는 증거 유형(연역적 검증, 정제 확인, 정리 증명)을 생성하므로, 엔지니어가 정형 언어를 배우거나 기존 Java 툴체인을 포기하지 않고도 AI 생성 코드에 대한 인증 경로를 제공한다.
• 실현 가능성: 견고한 추출 및 변환 파이프라인이 갖춰진다면, 메인스트림 언어로 작성된 LLM 생성 코드가 정형 모델로 변환되어 검증될 수 있음을 입증한다.
• 겸허한 태도: 저자들은 본 연구가 인증 사례를 위한 증거를 제공하는 것이지, 인증 그 자체를 의미하는 것은 아님을 명시한다. 완전한 인증을 위해서는 도구 자격 부여(tool qualification), 프로세스 증거, 독립적인 안전 사례 검토 등 추가적인 단계가 필요하며, 이는 향후 과제로 남겨둔다. 본 연구의 기여는 검증 루프를 닫는 실행 가능한 파이프라인의 존재를 입증하는 것이다.