ProofWright: CUDA 를 위한 에이전트 기반 형식 검증 (Agentic Formal Verification) 기술 요약

이 논문은 대규모 언어 모델 (LLM) 이 생성한 CUDA 커널의 정확성과 안전성을 보장하기 위해 제안된 ProofWright라는 자동화된 형식 검증 프레임워크를 소개합니다. LLM 이 생성한 코드는 성능 최적화 측면에서는 우수할 수 있지만, 데이터 레이스 (data race) 나 메모리 접근 오류와 같은 미묘한 결함을 포함할 가능성이 높으며, 기존 테스트 방식으로는 이러한 결함을 완전히 발견하기 어렵다는 문제를 해결합니다.

1. 문제 정의 (Problem)

• LLM 생성 코드의 신뢰성 부재: LLM 은 CUDA 커널을 자동으로 생성하고 최적화할 수 있지만, 생성된 코드는 종종 정합성 (correctness) 문제가 있거나 안전성 보장이 부족합니다.
• 기존 검증 방법의 한계:
  • 동적 테스트 (Runtime Testing): 입력 데이터에 의존하므로 모든 실행 경로를 커버하지 못하며, '보상 해킹 (reward hacking)'으로 인해 잘못된 코드가 테스트를 통과하는 경우가 발생합니다.
  • 수동 형식 검증: 기존 형식 검증 도구 (VerCors 등) 는 높은 정확도를 제공하지만, 수동 주석 (annotation) 작성에 의존합니다. LLM 이 생성하는 코드의 속도에 비해 인간 전문가가 주석을 작성할 수 있는 속도가 훨씬 느려 병목 현상이 발생합니다.
  • 단순 프롬프트 엔지니어링의 실패: LLM 에 형식 검증 도구를 단순히 프롬프트로 연결하는 것만으로는 정확한 주석을 생성하거나 검증을 성공적으로 수행할 수 없습니다.

2. 방법론 (Methodology)

ProofWright 는 피드백 기반의 에이전트 (Agent) 시스템으로, VerCors(SMT 기반 정적 분석기) 와 Rocq(정리 증명기) 를 활용하여 LLM 생성 CUDA 코드를 자동으로 검증합니다. 프레임워크는 크게 두 가지 주요 구성 요소로 나뉩니다.

2.1 에이전트 형식 검증 프레임워크 (Thread & Memory Safety)

LLM 이 생성한 커널의 메모리 안전성과 **스레드 안전성 (데이터 레이스 부재)**을 보장합니다.

• VerCors 에이전트: LLM 기반 에이전트가 VerCors 에 필요한 주석 (contracts, permissions) 을 자동으로 생성합니다.
• 지식 기반 (Knowledge Base): VerCors 문법, 오류 - 수정 쌍 (error-fix pairs), 검증 사례 등을 포함하는 정적 데이터베이스입니다.
• 주석 가이드 (Annotation Guide): 에이전트가 검증 경험을 통해 학습한 동적 문서입니다. 성공적인 검증 사례에서 새로운 패턴 (예: 알고리즘 계열별 접근 방식, 스레드 - 데이터 매핑 전략) 을 추출하여 가이드를 업데이트하고, 이를 통해 에이전트의 일반화 능력을 향상시킵니다.
• 작동 방식: 에이전트는 주석을 생성하고 VerCors 로 검증한 후, 실패 시 오류 메시지를 분석하여 주석을 수정하는 반복적인 피드백 루프를 수행합니다.

2.2 에이전트 의미 동등성 프레임워크 (Semantic Equivalence)

생성된 CUDA 코드가 원래의 **PyTorch 명세 (Specification)**와 기능적으로 동일한지 증명합니다.

• 전단 (Front-end): PyTorch 프로그램을 정적 분석하여 계산 그래프 (Computation Graph) 로 변환하고, 이를 MLRocq 라이브러리를 통해 Rocq(정리 증명기) 의 형식적 명세로 변환합니다.
• 후단 (Back-end): 생성된 CUDA 코드를 Rocq 명세로 변환하고, 두 명세 간의 동등성을 증명하는 정리 (Theorem) 를 Rocq 에이전트가 자동으로 구성합니다.
• 하향 변환 (Lowering): 증명된 Rocq 명세를 VerCors 기능 주석으로 변환하여, 생성된 CUDA 코드가 원래 명세를 준수함을 최종적으로 검증합니다.

3. 주요 기여 (Key Contributions)

1. 에이전트 형식 검증 프레임워크: 컨텍스트 학습 (In-context learning) 과 경험 기반 학습 (Annotation Guide) 을 결합하여 SMT 솔버 기반 도구 (VerCors) 를 위한 주석을 자동으로 생성하고, 메모리 및 스레드 안전성을 증명합니다.
2. 에이전트 의미 동등성 프레임워크: 정적 분석과 수학 추상화 라이브러리 (MLRocq), 정리 증명기 (Rocq) 를 활용하여 LLM 생성 코드가 원래 PyTorch 명세와 의미적으로 동등한지 자동으로 검증합니다.
3. 실용적 검증 가능성 입증: LLM 생성 GPU 코드에 대한 확장 가능하고 자동화된 형식 검증이 가능함을 보여주었으며, 개발 생산성을 희생하지 않으면서도 신뢰할 수 있는 고성능 코드 생성 경로를 제시했습니다.

4. 실험 결과 (Results)

KernelBench L1 벤치마크 (LLM 이 생성한 PyTorch 프로그램 기반 CUDA 커널) 를 사용하여 평가했습니다.

• 안전성 검증 (Memory & Thread Safety):
  • 생성된 커널 중 **74%**에 대해 메모리 안전성과 데이터 레이스 부재를 성공적으로 증명했습니다.
  • 기존 테스트에서 놓쳤던 미묘한 오류 (예: 꼬리 요소 처리 시 발생하는 레이스 컨디션) 를 발견했습니다.
  • 성공 요인: 지식 기반과 주석 가이드가 모두 포함된 경우에만 높은 성공률을 보였으며, 이 요소들이 없으면 검증이 거의 불가능했습니다.
• 의미 동등성 검증 (Semantic Equivalence):
  • 전체 커널 중 **14%**에 대해 기능적 정확성 (원래 명세와의 동등성) 을 완전히 증명했습니다. 주로 1:1 매핑을 하는 요소별 (element-wise) 커널 (ReLU, HardTanh 등) 에서 성공했습니다.
  • 한계: 축약 (reduction) 이나 복잡한 스레드 간 상호작용이 필요한 커널은 현재 하향 변환 로직의 한계로 인해 검증이 어렵습니다.
• 오버헤드:
  • 커널당 평균 약 3 분의 오버헤드가 발생했으나, 이는 형식 검증의 높은 신뢰도를 고려할 때 수용 가능한 수준으로 판단됩니다.

5. 의의 및 결론 (Significance)

• 신뢰할 수 있는 AI 코드 생성: LLM 이 생성한 GPU 코드의 안전성과 정확성을 수학적으로 증명함으로써, 자율 주행이나 항공기와 같은 고신뢰성 시스템에서도 AI 생성 코드를 활용할 수 있는 기반을 마련했습니다.
• 에이전트 학습의 중요성: 단순한 프롬프트 엔지니어링으로는 형식 검증이 불가능하며, **지식 기반 (Knowledge Base)**과 **경험 기반의 주석 가이드 (Annotation Guide)**가 에이전트의 일반화 능력과 성공률에 결정적인 역할을 함을 입증했습니다.
• 미래 전망: ProofWright 는 형식 검증과 LLM 을 결합한 새로운 패러다임을 제시하며, 향후 더 많은 CUDA 기능 (Tensor Core 등) 을 지원하고 Rocq-to-VerCors 변환의 신뢰성을 높여 확장될 예정입니다.

요약하자면, ProofWright 는 LLM 이 생성한 복잡한 GPU 코드의 결함을 테스트가 아닌 형식적 증명을 통해 자동으로 찾아내고 수정하는 선구적인 도구로, AI 기반 소프트웨어 개발의 신뢰성 문제를 해결하는 중요한 진전입니다.