VeruSAGE: Rust 시스템에 대한 에이전트 기반 검증 연구 (VeruSAGE: A Study of Agent-Based Verification for Rust Systems) 기술 요약

이 논문은 대규모 언어 모델 (LLM) 이 시스템 소프트웨어, 특히 Rust로 작성된 소프트웨어의 정형 검증 (Formal Verification) 증명 작업을 수행할 수 있는 능력을 종합적으로 조사한 연구입니다. 저자들은 기존 연구가 단순한 프로그래밍 문제에 집중하거나 작은 규모의 벤치마크에 그쳤던 한계를 극복하기 위해, 실제 시스템 수준의 복잡한 증명을 다루는 새로운 벤치마크와 에이전트 시스템을 제안했습니다.

1. 연구 배경 및 문제 정의 (Problem)

• 배경: AI 코딩 에이전트는 방대한 양의 코드를 빠르게 생성할 수 있지만, 신뢰성이 중요한 시스템 소프트웨어의 경우 정확성 보장이 부족합니다. 반면, Verus 와 같은 도구를 사용한 정형 검증은 수학적으로 정확성을 증명할 수 있으나, 인간 전문가의 수작업이 필요하여 속도가 느리고 접근성이 낮습니다.
• 문제: LLM 이 실제 시스템 소프트웨어의 복잡성을 가진 정형 증명 (Proof) 을 작성할 수 있는가?
• 기존 연구의 한계:
  • 기존 벤치마크 (예: VerusBench) 는 작은 프로그램 (이진 검색 등) 에 집중하여 실제 시스템의 복잡성 (수천 줄의 명세, 보조 정리, 루프 불변식 등) 을 반영하지 못함.
  • 기존 에이전트 (AutoVerus, RagVerus 등) 는 GPT-4o 등을 사용하여 실제 시스템 프로젝트 (VeriSMo, IronKV 등) 에서 증명 성공률이 20% 이하로 매우 낮았음.
  • 에이전트 아키텍처의 한계인지, 모델 자체의 능력 한계인지에 대한 명확한 분석이 부족함.

2. 방법론 (Methodology)

2.1. 새로운 벤치마크: VeruSAGE-Bench

저자들은 8 개의 오픈소스 Verus-검증 Rust 시스템 (Atmosphere, IronKV, Anvil 등) 에서 추출한 849 개의 증명 작업으로 구성된 새로운 벤치마크를 구축했습니다.

• 특징:
  • 각 작업은 독립적으로 컴파일 및 검증 가능한 단일 Rust 파일로 추출됨.
  • 원본 프로젝트의 증명 본문 (Proof bodies) 은 제거하고, 명세 (Spec) 와 의존성만 포함시켜 LLM 이 실제로 증명을 생성하는 능력을 평가.
  • 복잡성: 기존 벤치마크 대비 명세 코드 (Spec LoC) 가 50 배 이상 많고, 보조 정리 (Helper Lemmas) 사용 빈도가 훨씬 높으며, 루프 불변식 (Loop Invariants) 은 드물지만 그 복잡도는 매우 높음.

2.2. 에이전트 시스템 설계

LLM 의 특성에 맞춰 두 가지 접근 방식을 설계하고 비교했습니다.

1. Hands-Off 접근법 (자동화 중심):

   • 대상: 강력한 코딩 모델 (Sonnet 4, Sonnet 4.5, GPT-5).
   • 방식: GitHub Copilot CLI 와 같은 범용 코딩 에이전트를 사용. LLM 에게 Verus 표준 라이브러리 (vstd) 와 'Cheating Checker' (불법 증명 방지 도구) 에 대한 접근 권한만 부여하고, 간단한 프롬프트로 증명을 요청.
   • 핵심: LLM 이 스스로 도구를 호출하고 증명을 개발하도록 유도.

2. Hands-On 접근법 (VeruSAGE 에이전트):

   • 대상: 상대적으로 작은 모델 (o4-mini, GPT-5) 또는 복잡한 전략이 필요한 경우.
   • 방식: AutoVerus 를 대폭 확장한 VeruSAGE 에이전트 시스템.
   • 구조:
     • 계획 (Planning) 에이전트: 검증 오류를 분석하고 어떤 전략 (귀납, 반증, 비트 벡터 솔버 등) 을 사용할지 결정.
     • 행동 (Action) 에이전트: 구체적인 오류 수정 (논리 추론, 산술 증명, 양화사 처리 등) 을 수행하는 다수의 전문 에이전트.
     • 후보 선택기: 단순 오류 개수 감소가 아닌, 증명 전략의 유효성을 고려하여 중간 증명 후보를 선택.
     • 컨텍스트 관리: 과거 시도 기록과 관련 코드만 집중적으로 제공하여 토큰 효율성 및 학습 효과 극대화.

3. 주요 결과 (Key Results)

3.1. 성능 평가

• 최고 성능: Sonnet 4.5 + Hands-Off 조합이 849 개 작업 중 81% 이상을 성공적으로 증명했습니다.
  • 특정 프로젝트 (Anvil Library, Node Replication, Vest) 에서는 100% 성공률을 기록했습니다.
  • 2025 년 11 월에 공개된 Atmosphere 프로젝트 (모델 학습 데이터에 포함되지 않음) 에서도 **83%**의 성공률을 보였습니다.
  • 인간 전문가가 아직 완료하지 못한 33 개의 미완성 증명 작업도 LLM 이 성공적으로 완료했습니다.
• 작은 모델의 향상: VeruSAGE(Hands-On) 를 적용한 o4-mini는 기존 AutoVerus 대비 성공률이 2 배 이상 향상되어 **41%**에 도달했습니다.
• 모델 간 비교: Sonnet 4.5 > Sonnet 4 > GPT-5 > o4-mini 순으로 성능이 우수했습니다.

3.2. LLM 과 인간의 증명 차이

• 전략: LLM 은 귀납 (Induction) 보다는 반증 (Contradiction) 을 더 자주 사용하며, 비선형 산술 솔버 대신 표준 라이브러리 보조 정리를 활용하는 경향이 있습니다.
• 길이: LLM 이 생성한 증명은 인간이 작성한 것보다 평균적으로 훨씬 길었습니다 (LLM: 평균 44.2 줄 vs 인간: 평균 17.3 줄). 이는 LLM 이 자동 증명기로 해결 가능한 부분까지 과도하게 증명하려는 경향 때문입니다.
• 명세 수정: LLM 은 인간 전문가가 놓친 명세 (Specification) 의 오류를 발견하고 수정을 제안하는 경우도 있었습니다 (예: Atmosphere 프로젝트의 seq_skip_lemma).

3.3. 실패 원인 및 비용

• 실패 원인:
  • Hands-Off: 복잡한 추상화 (Abstraction) 처리 실행, 매크로 확장 실패, 인덕티브 불변식 (Inductive Invariant) 생성 실패.
  • Hands-On: Sonnet 모델의 경우 VeruSAGE 의 단계별 제한이 오히려 속도를 저하시켜 실패하는 경우 발생.
• 비용:
  • Sonnet 4.5 (Hands-Off) 는 평균 7.2 분, 작업당 약 $5.61 의 비용으로 증명을 완료했습니다. 이는 인간 전문가의 작업 시간 (평균 10 분 이상) 과 비교해 경쟁력 있는 수준입니다.

4. 주요 기여 (Key Contributions)

1. VeruSAGE-Bench: 실제 시스템 소프트웨어의 복잡성을 반영한 최초의 대규모 Verus 검증 벤치마크 (849 개 작업) 를 공개했습니다.
2. 에이전트 아키텍처 비교: "Hands-Off"(강력한 모델 + 도구) 와 "Hands-On"(약한 모델 + 전문 에이전트) 전략의 효과성을 체계적으로 비교하고, 모델 특성에 맞는 최적의 접근법을 제시했습니다.
3. 실제 시스템 검증 가능성 입증: LLM 이 학습 데이터에 없는 최신 시스템 (Atmosphere) 의 증명 작업을 80% 이상 성공적으로 수행할 수 있음을 보여주었습니다.
4. 인간 - AI 협업 모델: LLM 이 인간 전문가의 미완성 작업을 완성하거나, 명세 오류를 수정하는 등 실제 개발 워크플로우에서 유효한 파트너가 될 수 있음을 입증했습니다.

5. 의의 및 결론 (Significance)

이 연구는 LLM 이 단순한 코드 생성을 넘어, 고신뢰성 시스템 소프트웨어의 정형 검증이라는 어려운 영역에서도 실용적인 성과를 낼 수 있음을 보여줍니다.

• 시스템 검증의 민주화: LLM 을 활용하면 정형 검증의 진입 장벽을 낮추고 검증 속도를 획기적으로 높일 수 있어, 대규모 검증 시스템 개발이 더 빈번해질 것으로 기대됩니다.
• 한계와 전망: 현재 LLM 은 복잡한 인덕티브 불변식 생성이나 대규모 시스템의 추상화 처리에는 여전히 어려움을 겪고 있으며, 명세 자체를 설계하는 단계에서는 인간 전문가의 역할이 필수적입니다.
• 미래 방향: LLM 이 생성한 코드는 검증기 (Verifier) 를 통해 신뢰성을 즉시 확인할 수 있으므로,proof writing 은 신뢰할 수 없는 LLM 을 활용하기에 이상적인 분야로 평가됩니다.

결론적으로, VeruSAGE 연구는 LLM 기반 에이전트가 시스템 소프트웨어의 정확성 보장을 위한 핵심 기술로 자리 잡을 수 있는 강력한 가능성을 제시합니다.