VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

이 논문은 Verus 의 데이터 구조 모듈에 대한 AI 지원 자동 검증을 가능하게 하는 새로운 프레임워크인 VeriStruct 를 제안하며, 구문 안내와 자동 수정 단계를 통해 11 개 모듈 중 10 개 (129 개 함수 중 128 개) 에서 높은 성공률을 보인 결과를 제시합니다.

핵심

📝 VeriStruct: AI 가 코드를 '수학적으로' 증명하는 마법사

이 논문은 VeriStruct이라는 새로운 도구를 소개합니다. 이 도구는 인공지능 (AI) 을 활용하여 컴퓨터 프로그램의 복잡한 부품인 '데이터 구조'가 정말로 안전하고 오류가 없는지 자동으로 검증해 줍니다.

이 개념을 이해하기 쉽게 비유를 들어 설명해 드리겠습니다.

---

1. 문제 상황: AI 가 쓴 코드는 '부실 공사'일 수 있다? 🏗️

요즘 개발자들은 AI 의 도움을 받아 코드를 많이 작성합니다. AI 는 매우 빠르고 똑똑하지만, 가끔은 보이지 않는 구멍을 남기거나 안전 규정을 어기는 코드를 만들기도 합니다.

• 전통적인 해결책: 전문가들이 코드를 하나하나 뜯어보고 "이건 안전하다"라고 수학적 증명서를 발급해 줍니다. 하지만 이 작업은 너무 어렵고 시간이 많이 걸려서, 실제로는 거의 쓰이지 않았습니다.
• 새로운 시도: AI 가 이 증명서를 대신 써주면 어떨까요? 하지만 AI 는 코딩은 잘해도, **엄격한 수학 규칙 (Verus 라는 언어)**을 잘 모릅니다. 마치 "요리법은 알지만, 식중독 검사 기준은 모르는 요리사"와 같습니다.

2. VeriStruct 의 등장: AI 를 위한 '현명한 감독'과 '수선공' 👷‍♂️🔧

VeriStruct 는 AI 가 코드를 검증할 때 겪는 문제를 해결하기 위해 고안된 스마트 워크플로우입니다. 이를 건축 현장에 비유해 보겠습니다.

🧠 1 단계: '기획자 (Planner)'가 먼저 나섭니다

AI 가 바로 코드를 쓰기 시작하면 엉망이 될 수 있습니다. 그래서 먼저 **기획자 (Planner)**가 나옵니다.

• 역할: "이 건물을 짓는데 어떤 자재가 필요할까?"라고 생각합니다.
• 작동: 데이터 구조의 종류를 보고, "이건 '수학적 모델 (View)'이 필요하고, '안전 규칙 (Type Invariant)'도 필요해. 하지만 '루프 증명'은 필요 없겠네"라고 필요한 작업 목록을 짭니다.
• 효과: AI 가 불필요한 일을 하지 않게 하여 실수를 줄입니다.

🎨 2 단계: '설계사 (LLM)'가 청사진을 그립니다

기획자의 지시를 받은 AI 는 코드의 **추상화 (View)**와 안전 규칙을 작성합니다.

• 비유: 실제 기계 부품 (코드) 을 설명할 때, "나사 10 개, 톱니 5 개"라고 나열하는 대신, **"이 기계는 물을 담는 통이다"**라고 개념적으로 설명하는 것입니다. 이렇게 하면 복잡한 기계 내부보다 '물'이라는 개념으로 안전성을 증명하기 훨씬 쉬워집니다.
• 주의: AI 는 Verus 라는 언어의 규칙을 잘 몰라 실수하기 쉽습니다. (예: "이 함수는 실행 중이라서 증명서에 쓸 수 없어!" 같은 실수)

🔨 3 단계: '수선공 (Repair Module)'이 실수를 고칩니다

AI 가 쓴 증명서는 100% 완벽하지 않습니다. 이때 수선공이 나옵니다.

• 작동: 검증 도구 (Verus) 가 "여기 오류가 있어!"라고 경고하면, 수선공은 그 오류를 분석해서 AI 에게 "아, 이 함수는 증명용이 아니었구나. 증명용 버전을 새로 만들어서 바꿔야겠다"라고 알려줍니다.
• 반복: 이 과정이 몇 번이고 반복됩니다. AI 가 실수하면 고치고, 다시 검증하는 수선 - 검증 사이클을 돌립니다.

---

3. 실제 성과: 11 개 중 10 개를 완벽하게! 🏆

연구팀은 이 시스템을 11 가지의 복잡한 데이터 구조 (링 버퍼, 트리, 동시성 잠금 장치 등) 에 적용해 보았습니다.

• 결과: 11 개 중 10 개를 성공적으로 검증했습니다.
• 함수 단위: 총 129 개의 함수 중 **128 개 (99.2%)**를 오류 없이 증명했습니다.
• 비교: AI 만을 단순히 반복해서 사용하는 기존 방식은 11 개 중 4 개만 성공했고, VeriStruct 는 2 배 이상 더 많은 문제를 해결했습니다.

4. 핵심 요약: 왜 이것이 중요한가? 🌟

이 논문은 **"AI 가 코드를 작성하는 시대에도, 수학적으로 안전한 코드를 자동으로 만들 수 있다"**는 것을 보여줍니다.

• 기존 방식: 전문가가 일일이 증명서를 써야 함 (너무 느리고 비쌈).
• 기존 AI 방식: AI 가 증명서를 쓰려다 규칙을 어김 (실패율 높음).
• VeriStruct 방식: 기획자가 계획을 세우고, AI가 초안을 쓰고, 수선공이 실수를 고쳐서 완벽한 증명서를 만듦.

결론

VeriStruct 는 AI 를 단순히 '코드 작성 도구'가 아니라, **엄격한 규칙을 지키는 '안전 관리자'**로 변신시킨 혁신적인 도구입니다. 앞으로는 우리가 AI 가 만든 소프트웨어를 믿고 사용할 수 있는 기반이 될 것입니다. 마치 AI 가 만든 자동차를 타기 전에, AI 가 스스로 안전성 검사를 통과하고 인증서를 발급해주는 것과 같습니다. 🚗✅

기술 요약

1. 문제 정의 (Problem Definition)

• 배경: 생성형 AI 는 코드 생산성을 높이지만, 동시에 새로운 버그와 보안 취약점을 도입할 위험이 있습니다. 이를 해결하기 위해 프로그램 검증 (Program Verification) 이 필요하지만, 기존 검증 도구 (SMT 솔버 등) 는 수학적 논리 주석 (전제조건, 사후조건, 불변식 등) 을 작성하는 데 막대한 전문가의 노력과 시간이 필요하여 실용성이 제한되었습니다.
• 기존 연구의 한계: 최근 LLM 을 활용한 자동 검증 연구는 주로 단일 함수 (textbook algorithms) 에 집중되어 있었습니다. 그러나 실제 소프트웨어 시스템의 핵심인 데이터 구조 모듈 (Data Structure Modules) 은 단일 함수 검증보다 훨씬 복잡합니다.
  • 데이터 구조는 여러 메서드가 공유하는 타입 불변식 (Type Invariants) 을 유지해야 합니다.
  • 구체적인 구현을 추상적인 수학적 모델 (View) 로 매핑해야 합니다.
  • LLM 은 Verus(Verus 는 Rust 용 최신 프로그램 검증 도구) 의 특수한 주석 문법과 검증 의미론 (Verification Semantics) 을 잘 이해하지 못해, 실행 가능한 함수를 명세 문맥에서 호출하는 등 문법 오류를 자주 범합니다.

2. 방법론 (Methodology)

논문은 VeriStruct라는 새로운 AI 지원 자동 검증 프레임워크를 제안합니다. 이는 Verus 환경에서 Rust 데이터 구조 모듈을 검증하기 위해 설계되었으며, 크게 두 단계의 파이프라인으로 구성됩니다.

A. 입력 및 출력

• 입력: 검증할 Rust 소스 코드 (주석 없음) 와 데이터 구조의 의도된 사용법 및 예상 동작을 보여주는 유닛 테스트 스위트.
• 출력: Verus 검증기를 통과하는 주석이 포함된 완전한 코드.

B. 주요 구성 요소 및 워크플로우

1. 플래너 모듈 (Planner Module):

   • 검증 작업을 분석하여 어떤 생성 모듈이 필요한지 결정합니다. 모든 모듈을 무조건 실행하는 대신, 데이터 구조의 특성에 따라 필요한 모듈 (View, Type Invariant, Specification, Proof Block) 만 선택적으로 실행하여 안정성과 효율성을 높입니다.

2. 1 단계: 주석 생성 (Generation Stage)

   • 플래너의 지시에 따라 4 가지 전용 모듈을 순차적으로 실행합니다.
     • View 모듈: 데이터 구조의 구체적 구현을 추상적인 수학적 객체 (Seq, Set, Map 등) 로 매핑하는 view 함수를 생성합니다.
     • Type Invariant 모듈: 데이터 구조 인스턴스가 반드시 만족해야 하는 논리적 조건 (예: 인덱스 범위, 용량 제약) 을 정의합니다.
     • Specification 모듈: 함수의 전제조건 (requires), 사후조건 (ensures), 그리고 명세 함수를 생성합니다.
     • Proof Block 모듈: 검증기를 돕는 증명 블록과 루프 불변식을 생성합니다.
   • 프롬프트 설계: LLM 이 Verus 문법을 오해하는 것을 방지하기 위해, Verus 튜토리얼과 표준 라이브러리에서 추출한 구체적인 문법 가이드라인을 프롬프트에 포함시켰습니다. 또한, 추상화 수준이 낮은 (구현 세부사항을 그대로 드러내는) View 가 생성될 경우, 이를 View Refinement 단계를 통해 더 간결하고 논리적인 형태로 재구성합니다.

3. 2 단계: 주석 수정 (Repair Stage)

   • 단일 실행으로 완벽한 검증이 이루어지지 않는 경우가 많으므로, 검증기 (Verus) 의 오류 메시지를 기반으로 반복적인 수정 루프를 수행합니다.
   • 오류 분류 및 수정 모듈: 검증기 오류 메시지를 패턴 매칭하여 분류하고, 해당 오류 유형에 맞는 전용 수정 모듈을 호출합니다.
     • 예: 실행 가능 함수를 명세 문맥에서 호출한 경우, 이를 spec 함수 버전으로 교체하도록 지시.
     • 예: Rust 의 가변성 (mutability) 시스템 위반, 전/사후 조건 불일치, 논리형과 Rust 형 불일치 등 7 가지 주요 오류 유형을 처리.
   • 테스트 assertion 실패 처리: 테스트 실패 시, 실패 직전 호출된 메서드의 사후조건을 강화하도록 LLM 을 지시하여 교차 절차적 (interprocedural) 분석을 수행합니다.

3. 주요 기여 (Key Contributions)

1. 새로운 워크플로우 제안: 단일 함수를 넘어 복잡한 데이터 구조 모듈 전체를 검증하기 위한 LLM 지원 워크플로우를 최초로 제안했습니다. 이는 View, 타입 불변식, 명세, 증명 블록을 통합적으로 생성하고 수정하는 체계적인 접근법입니다.
2. VeriStruct 도구 구현: 위 워크플로우를 Verus 환경에 구현하여 오픈소스로 공개했습니다.
3. 효율성 입증: 11 개의 벤치마크에 대한 실험을 통해 기존 방식보다 월등히 높은 검증 성공률을 보임을 입증했습니다.

4. 실험 결과 (Results)

• 벤치마크: Verus 예제 및 타 오픈소스 저장소에서 가져온 11 개의 Rust 데이터 구조 모듈 (Ring Buffer, Treemap, Bitmap, RwLock 등) 을 사용했습니다. 총 129 개의 검증 대상 함수가 포함되었습니다.
• 성능:
  • 성공률: 11 개 벤치마크 중 10 개를 성공적으로 해결했습니다.
  • 함수 검증: 총 129 개 함수 중 128 개 (99.2%) 를 성공적으로 검증했습니다.
  • 비교:
    • 단순 반복 호출 방식의 Baseline: 11 개 중 4 개만 해결 (52 개 함수 검증).
    • Claude Code(최신 모델 사용): 8 개 벤치마크, 102 개 함수 검증.
    • VeriStruct는 Baseline 보다 150% 더 많은 벤치마크를 해결하고, Claude Code 보다 더 많은 함수를 검증했습니다.
  • 비용: VeriStruct 는 Claude Code 와 유사하거나 더 낮은 토큰 비용 (평균 22k 토큰) 으로 더 높은 성능을 달성했습니다.
• Case Study (Bitmap): 인간 전문가가 작성한 복잡한 2 차원 배열 추상화 대신, LLM 이 Verus 의 내장 Seq 타입을 활용한 더 단순하고 효율적인 단일 배열 추상화를 찾아내어 성공적으로 검증한 사례가 있었습니다.

5. 의의 및 결론 (Significance)

• 자동화 수준 향상: 수동으로 주석을 작성하는 고비용 장벽을 낮추고, LLM 을 통해 데이터 구조 수준의 복잡한 형식 검증을 자동화할 수 있음을 증명했습니다.
• 신뢰성 있는 라이브러리 구축: 검증된 데이터 구조 모듈은 추후 더 복잡한 시스템 코드 검증의 기반이 되어 전체 소프트웨어의 신뢰성을 높이는 데 기여합니다.
• 향후 방향:
  • 자동 유닛 테스트 생성: 현재는 사용자가 테스트를 제공해야 하지만, LLM 을 이용해 테스트 케이스도 자동 생성하여 인간 개입을 최소화할 계획입니다.
  • 강화 학습 (RL) 적용: 검증 성공을 보상 신호로 사용하여 명세 추론 및 증명 생성을 최적화하는 강화 학습 기법 도입을 고려하고 있습니다.
  • 복잡한 동시성 검증: Verus 의 리소스 대수 (Resource Algebra) 라이브러리 지원을 통해 더 복잡한 동시성 데이터 구조 검증으로 확장할 예정입니다.

이 논문은 AI 와 형식 검증의 융합을 통해 소프트웨어의 안전성과 신뢰성을 획기적으로 높일 수 있는 중요한 이정표로 평가됩니다.