Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought
이 논문은 LLM 이 Rust 프로그램 검증에서 자동 정리 증명기와 같은 추론 능력을 갖는지 평가하기 위해, 검증 과정의 논리적 단계를 명시화한 'VCoT-Lift' 프레임워크와 이를 기반으로 한 'VCoT-Bench' 벤치마크를 제안하며, 현재 LLM 들의 추론 능력이 자동 정리 증명기에 비해 여전히 취약함을 밝혔습니다.
지금까지 AI 가 Rust(안전한 프로그래밍 언어) 코드를 검증할 때, 우리는 **"이 코드가 통과했나요? (O/X)"**만 확인했습니다.
비유: 학생이 수학 시험을 봤는데, 우리는 정답지만 보고 "맞았습니다"라고 점수를 매긴 셈입니다.
문제점: 학생이 진짜 공식을 이해하고 풀었는지, 아니면 운 좋게 정답을 외워서 적었는지, 혹은 엉뚱한 계산으로 우연히 맞췄는지 알 수 없습니다. AI 도 마찬가지입니다. "코드가 안전하다"는 결과만 보고 AI 가 논리를 진짜 이해했다고 착각할 수 있습니다.
2. 해결책: "생각의 과정"을 보여달라 (VCoT)
저자들은 AI 가 어떻게 그 결론에 도달했는지, 그 **생각의 과정 (Chain of Thought)**을 단계별로 보여달라고 요구했습니다. 이를 **'검증 사고 과정 (VCoT)'**이라고 부릅니다.
비유: 이제 학생에게 "정답만 쓰지 말고, 풀이 과정을 자세히 적어봐"라고 시켰습니다. "왜 A 가 B 가 되는지, 어떤 공식을 썼는지"를 하나하나 설명해야 합니다.
3. 도구: "번역기"와 "정리꾼" (VCoT-Lift)
컴퓨터가 만든 증명 과정 (Z3 솔버) 은 인간이 보기엔 너무 난해하고 지저분한 1 만 줄짜리 기계어입니다.
비유: 컴퓨터가 쓴 증명은 "A=1, B=2, A+B=3... (중략) ...x775=x775" 같은 1 만 줄짜리 장난감 레고 조각 같습니다. 인간은 이걸 보고 의미를 알 수 없죠.
VCoT-Lift 의 역할: 이 난해한 레고 조각들을 모아, **"이건 'A+B=C' 공식이 적용된 거야"**라고 사람이 읽을 수 있는 명쾌한 해설서로 바꿔주는 '고급 번역기'입니다.
번역: 기계어를 인간 언어로 바꿈.
정리: 불필요한 잡음 (A=A 같은 당연한 것) 을 제거.
수정: 문법 오류를 고쳐서 완벽하게 만듦.
4. 시험지: "구멍 뚫기" (VCoT-Bench)
이제 만든 '해설서'를 바탕으로 AI 를 시험했습니다.
방법: 해설서의 중간중간 **구멍 (Proof Holes)**을 뚫고, AI 가 그 빈칸을 채우게 했습니다.
비유: 수학 문제집에서 중간 단계 30% 를 지우고, "이제 너가 이 빈칸을 채워봐"라고 한 것입니다.
시험 내용:
양: 지운 부분이 10% 일 때 vs 90% 일 때 (정보를 얼마나 잃어도 풀 수 있나?)
유형: 루프 (반복문) 증명 vs 단언 (assertion) 증명 등 (어떤 유형을 잘 풀까?)
위치: 문제의 앞부분 vs 중간 vs 끝부분 (중간 연결 고리를 잘 잇나?)
5. 결과: "AI 는 아직 수학자가 아니다"
10 개의 최신 AI 모델을 시험해 본 결과는 충격적이었습니다.
결론: AI 는 주변에 힌트가 많이 있을 때는 잘 풀지만, 중요한 연결 고리 (빈칸) 가 조금만 사라져도 완전히 망가졌습니다.
비유:
AI 의 방식: "아, 앞쪽에 'A+B'가 있네? 그럼 여기서 'C'가 나오겠지?"라고 패턴을 외워서 맞추는 방식입니다. (문맥이 사라지면 당황함)
자동 증명기 (Z3) 의 방식: "A 와 B 의 관계를 논리적으로 따져서 C 를 유도한다."는 진짜 추론을 합니다.
결과: AI 는 **중간 연결 고리 (Connective Reasoning)**를 채우는 데 특히 약했습니다. 앞뒤가 다 보여도, 그 사이를 잇는 논리가 끊기면 AI 는 "어? 뭐지?" 하며 멈춰버립니다.
6. 요약 및 시사점
현재 상태: AI 는 코드를 작성하는 데는 훌륭하지만, 코드가 왜 안전한지 논리적으로 증명하는 '수학자'의 능력은 자동 증명기 (ATP) 에 비해 훨씬 부족합니다.
미래: 이 연구는 AI 가 단순히 "코드 짜기"를 넘어, "왜 이 코드가 안전한지 논리적으로 설명하고 증명하는" 단계로 나아가기 위해, **생각의 과정 (VCoT)**을 훈련 데이터로 써야 한다고 제안합니다.
한 줄 요약:
"AI 가 코드를 검증할 때, 단순히 정답만 맞추는 '암기왕'이 아니라, 논리 과정을 하나하나 설명할 수 있는 '수학자'가 되려면 아직 갈 길이 멀다. 우리는 이제 AI 의 '생각 과정'을 들여다보고 훈련시켜야 한다."
1. 문제 제기 (Problem)
Rust 검증의 중요성: Rust 는 메모리 안전성과 동시성 보장을 위해 널리 사용되지만, LLM 이 생성한 코드에는 미묘한 논리적 오류가 포함될 수 있어 형식적 검증 (Formal Verification) 이 필수적입니다.
기존 평가의 한계: 현재 LLM 을 이용한 Rust 검증 연구 (AlphaVerus, SAFE 등) 는 주로 증명 힌트 (proof hints) 생성에 초점을 맞추며, 검증이 성공했는지 여부만 이진 (Pass/Fail) 으로 평가합니다.
블랙박스 문제: 이러한 평가 방식은 LLM 이 실제 논리적 추론을 수행했는지, 아니면 통계적 패턴이나 문법적 유사성만 exploited 했는지를 구분할 수 없습니다. 또한, 자동 증명기 (Z3) 가 생성하는 증명 로그는 인간이 이해하기 어려운 저수준 (low-level) 명령어와 방대한 양의 불필요한 단계로 구성되어 있어 분석이 어렵습니다.
2. 방법론 (Methodology)
2.1. VCoT-Lift (프레임워크)
저자들은 Z3 솔버의 저수준 증명 로그를 인간이 읽을 수 있는 고수준의 **VCoT (Verification Chain-of-Thought)**로 변환하는 프레임워크를 개발했습니다. 이는 다음과 같은 4 단계 파이프라인으로 구성됩니다:
Proof Transformer: Z3 증명 로그를 Verus 수준의 검증 단계 (루프 불변식, 어설션, 레마 등) 로 변환합니다. 긴 컨텍스트 처리를 위해 Z3 규칙을 중요도 (High/Medium/Low) 에 따라 계층화하여 LLM 의 주의를 집중시킵니다.
Proof Checker: 변환된 증명의 완전성 (Completeness) 을 평가합니다. 고수준 규칙 위주로 검증하며, 불필요한 단계 (Trivial/Redundant) 를 필터링하고, 각 Z3 단계가 Verus 증명의 어떤 단계에 대응되는지 명시적으로 매핑하여 허위 답변 (Hallucination) 을 방지합니다.
Proof Pruner: 변환 과정에서 발생한 불필요하거나 중복된 논리 단계를 제거하여 증명의 간결성 (Conciseness) 을 확보합니다.
Proof Repair: Verus 컴파일러와 상호작용하여 문법적/의미적 오류를 감지하고 수정하여 증명의 건전성 (Soundness) 을 보장합니다.
2.2. VCoT-Bench (벤치마크)
VCoT-Lift 를 통해 생성된 VCoT 를 정답 (Ground Truth) 으로 사용하여 VCoT-Bench를 구축했습니다.
데이터 구성: 1,988 개의 VCoT 완성 태스크로 구성되며, 기존 Verus-Bench 의 150 개 프로그램을 기반으로 합니다.
평가 차원: LLM 의 이해도를 3 가지 직교하는 차원에서 평가합니다.
Ratio (비율): 증명 블록의 제거 비율 (10%~100%) 에 따른 성능 변화.
Type (유형): 루프 불변식 (Invariant), 어설션 (Assertion), 레마 함수 (Lemma) 유형별 복원 능력.
Location (위치): 증명 과정의 앞 (Front), 중간 (Middle), 뒤 (End) 에 위치한 블록 제거 시 성능 변화.
3. 주요 기여 (Key Contributions)
개념 제안: 형식적 검증의 내부 논리를 인간이 이해할 수 있는 단계별 추론 과정인 VCoT 개념을 도입했습니다.
도구 개발: Z3 의 저수준 증명을 고수준 VCoT 로 변환하는 최초의 프레임워크인 VCoT-Lift를 개발했습니다.
벤치마크 구축: 1,988 개의 태스크를 포함하며, 다양한 차원에서 LLM 의 검증 능력을 세밀하게 평가할 수 있는 VCoT-Bench를 공개했습니다.
포괄적 연구: 10 개의 최첨단 LLM (GPT-5, Claude, Gemini, DeepSeek 등) 을 대상으로 한 대규모 평가를 통해 LLM 의 형식적 검증 능력에 대한 한계를 규명했습니다.
4. 실험 결과 (Results)
10 개의 SOTA LLM 을 대상으로 한 평가 결과는 다음과 같은 중요한 통찰을 제공합니다:
취약한 추론 능력: LLM 은 충분한 문맥 (Context) 이 주어지면 일부 단계를 완성할 수 있지만, 정보가 조금만 누락되어도 (예: 10% 블록 제거) 성능이 급격히 떨어집니다. 이는 LLM 이 1 차원적 추론 (First Principles) 을 하지 못하고, 국소적인 문법적 패턴 매칭에 의존하고 있음을 시사합니다.
임계점 (Threshold): 증명 블록의 40% 가 제거되면 대부분의 모델이 논리적 연속성을 잃고 추론이 붕괴됩니다.
증명 유형별 차이:
어설션 (Assertion): 가장 어려운 유형으로, 정밀한 상태 의존적 추론이 필요하여 성능이 가장 낮았습니다.
루프 불변식 (Loop Invariants): 상대적으로 정확도가 높았지만, 모델 간 편차가 가장 커서 LLM 의 진정한 검증 능력을 가르는 가장 민감한 지표였습니다.
위치에 따른 민감도:
중간 (Middle) 블록: 증명 과정의 연결고리 역할을 하는 중간 단계에서 성능이 가장 크게 저하됩니다. 이는 LLM 이 상태 전이를 추적하고 다단계 추론을 구성하는 데 어려움을 겪고 있음을 보여줍니다.
앞/뒤 (Front/End): 제약 조건 설정이나 종료 패턴과 같은 단순한 부분에서는 상대적으로 잘 수행합니다.
모델 규모와 추론: 모델 크기가 클수록 전반적인 성능은 좋지만, '생각하는 (Thinking)' 모드가 오히려 형식적 증명에서는 노이즈를 유발하여 성능을 저하시키는 경우도 있었습니다.
5. 의의 및 결론 (Significance)
현실적 한계 규명: 현재 LLM 은 자동 증명기 (Z3 등) 가 보여주는 수준의 엄밀한 논리적 추론 능력을 갖추지 못했습니다. LLM 은 여전히 문법적 스키에일딩 (Syntactic Scaffolding) 에 의존하고 있습니다.
새로운 평가 패러다임: 단순한 '성공/실패' 평가를 넘어, 검증 과정의 논리 구조를 얼마나 이해하고 재구성할 수 있는지를 평가하는 VCoT 기반 평가가 필요함을 강조합니다.
미래 방향: VCoT 는 단순한 평가 도구를 넘어, LLM 을 훈련시키기 위한 구체적인 감독 신호 (Supervision Signal) 로 활용될 수 있으며, LLM 이 형식적 검증의 논리를 재구성하고 추론할 수 있도록 유도하는 데 기여할 것입니다.
요약하자면, 이 논문은 LLM 이 Rust 코드 검증에 있어 아직 자동 증명기를 대체할 수 있는 수준이 아니며, 그 이유를 '논리적 추론의 부재'와 '문맥 의존성'에서 찾았으며, 이를 체계적으로 증명하기 위해 VCoT-Lift와 VCoT-Bench를 제안했습니다.