Automated Proof Generation for Rust Code via Self-Evolution
이 논문은 심볼릭 검증기의 피드백을 활용한 자기 진화 사이클을 통해 인간이 작성한 증명 데이터의 부족을 극복하고, 오픈 소스 모델이 Rust 코드에 대한 자동 증명 생성 능력을 비약적으로 향상시켜 GPT-4o 를 압도하는 정확도를 달성한 SAFE 프레임워크를 제안합니다.
원저자:Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, Lidong Zhou
1. 코드는 요리, 증명은 맛보기 코드를 작성하는 것은 요리를 하는 것과 같습니다. 하지만 요리가 끝났다고 해서 그 요리가 정말 맛있는지, 위생적인지, 독이 없는지는 알 수 없습니다.
기존 방식: 사람이 직접 맛을 보고 (테스트) "아, 이건 괜찮네"라고 말합니다. 하지만 모든 상황 (모든 손님, 모든 재료) 에서 맛을 볼 수는 없죠.
형식 검증 (Formal Verification): 코드를 수학적 논리로 증명하는 것입니다. "이 요리는 어떤 재료를 넣어도 절대 독이 나오지 않는다"라고 100% 확실하게 증명하는 거죠.
2. 하지만 증명하는 건 너무 어려워요! 이 '수학적 증명'을 하려면 코드를 작성하는 것보다 훨씬 더 어렵고 전문적인 지식이 필요합니다. 마치 요리사보다 '음식 과학자'가 되어야 하는 것과 비슷합니다. 그래서 지금까지는 증명된 코드가 거의 없었습니다. 데이터가 너무 부족해서 AI 가 배울 수 없었던 것이죠.
🚀 해결책: SAFE (자가 진화하는 증명 시스템)
저자들은 이 문제를 해결하기 위해 SAFE라는 시스템을 만들었습니다. SAFE 는 **"스스로 배우고 성장하는 AI"**입니다.
1. 식재료 구하기 (데이터 부족 문제 해결)
AI 가 배울 '증명된 요리 레시피'가 없어서 고민이었습니다.
해결책: AI 가 직접 '증명 가능한 요리'를 만들어냈습니다.
먼저, 유명한 요리책 (기존 데이터) 에서 레시피를 가져와서 증명 가능한 언어 (Rust) 로 번역했습니다.
그다음, AI 가 이 레시피에 맞는 '안전 규정 (명세)'을 스스로 만들어냈습니다.
2. 자가 진화 (Self-Evolving) 사이클
이게 이 논문의 핵심입니다. SAFE 는 다음과 같은 사이클을 반복합니다.
1 단계: 요리사 (AI) 가 레시피를 만듭니다. AI 가 코드를 작성하고, 그 코드가 안전하다는 '증명서'를 작성해 봅니다.
2 단계: 심사위원 (Verus) 이 감수합니다. 'Verus'라는 아주 엄격한 심사위원 (컴파일러) 이 AI 가 쓴 증명서를 봅니다.
합격: "이건 완벽해!" → 이 데이터를 AI 가 다음 학습에 사용합니다.
불합격: "여기서 오류가 있어!" → 이 실패한 증명서도 버리지 않고 학습 자료로 사용합니다.
3 단계: 실수에서 배우기 (Self-Debugging) AI 가 처음에 틀린 증명서를 썼을 때, 심사위원이 "어디가 틀렸는지" 알려줍니다. AI 는 이 오류 메시지를 보고 "아, 내가 여기서 실수했구나"라고 스스로 고칩니다.
마치 요리사가 "소금이 너무 짜요"라는 평을 듣고 다음엔 소금 양을 조절하는 것과 같습니다.
이 과정을 반복할수록 AI 는 점점 더 똑똑해지고, 증명하는 속도와 정확도가 높아집니다.
🏆 결과: 얼마나 잘하나요?
이 시스템으로 훈련된 AI 는 놀라운 성과를 냈습니다.
기존 AI (GPT-4o): 증명된 코드를 만드는 데 14% 정도만 성공했습니다. (대부분 틀렸습니다.)
SAFE (새로운 AI): 52% 이상을 성공했습니다.
특히, 자가 디버깅 (실수 고치기) 기능을 쓰면 정확도가 70% 이상으로 치솟습니다.
이는 인간 전문가가 만든 테스트에서도 GPT-4o 를 압도하는 결과입니다.
💡 핵심 요약 (비유로 정리)
문제: 코드가 안전한지 증명하는 건 너무 어려워서, AI 가 배울 교재가 없었습니다.
해결: AI 가 스스로 교재를 만들고 (데이터 생성), 스스로 시험을 보고 (증명 시도), 틀린 문제를 고치는 (자가 디버깅) 과정을 반복했습니다.
심사위원: AI 가 스스로 판단하지 못하게, 'Verus'라는 절대적인 심사위원이 정답과 오답을 가려주었습니다.
결론: 이제 AI 는 인간 전문가 못지않게, 혹은 그 이상으로 Rust 코드의 안전성을 자동으로 증명할 수 있게 되었습니다.
이 기술은 앞으로 우리가 사용하는 소프트웨어가 해킹이나 치명적인 오류 없이, 수학적으로 100% 안전하다는 것을 보장하는 시대를 열 것입니다.
1. 문제 정의 (Problem)
데이터 부족: 대규모 언어 모델 (LLM) 을 훈련시키기 위해 필요한 인간이 작성한 형식적 증명 (Formal Proofs) 데이터가 코드 스니펫에 비해 극히 적습니다. 특히 Rust 언어를 위한 검증 도구인 Verus의 경우, GitHub 에 검증된 파일이 500 개 미만으로, 파인튜닝에 사용할 데이터가 부족합니다.
검증의 어려움: Rust 코드를 Verus 로 검증하려면 함수의 동작을 설명하는 형식적 명세 (Specification, 전제조건/사후조건) 와 증명 주석 (Loop invariants 등) 을 직접 작성해야 하며, 이는 높은 전문성을 요구합니다.
기존 접근법의 한계:
프롬프트 엔지니어링/In-context Learning: 복잡한 프롬프트나 정적 분석에 의존하여 일반화 능력이 제한적입니다.
기존 파인튜닝: Lean 이나 F* 같은 언어는 수만 개의 인간 작성 증명이 존재하지만, Verus 와 같은 최신 도구는 데이터가 부족하여 적용이 어렵습니다.
2. 방법론 (Methodology: SAFE Framework)
SAFE 는 인간이 작성한 데이터가 없어도 대규모의 고품질 증명을 생성할 수 있도록 자기 진화 (Self-evolving) 사이클을 구축합니다. 이 과정은 크게 세 단계로 이루어집니다.
1 단계: Verus 호환 코드 생성 (Verus-Compatible Code Generation)
MBPP 및 CodeNet 데이터셋에서 가져온 Python 및 Rust 코드를 GPT-4o 를 이용해 Verus 가 지원하는 Rust 문법으로 변환합니다.
Verus 가 지원하지 않는 기능 (예: 특정 반복자, HashMap 등) 을 제거하거나 대체하여 컴파일 가능한 코드를 확보합니다.
2 단계: 자기 진화 명세 합성 (Self-Evolving Specification Synthesis)
목표: 변환된 Rust 함수에 대한 형식적 명세 (전제/사후 조건) 를 생성합니다.
과정:
초기 라운드 (Round 0) 에서는 GPT-4o 가 자연어 문서 (doc-string) 를 기반으로 명세를 생성합니다.
이후 라운드에서는 생성된 명세로 오픈소스 LLM 을 파인튜닝하여 더 높은 품질의 명세를 생성합니다.
품질 필터링: 생성된 모든 명세를 사용하지 않고, 정확성 (Correctness) 과 완결성 (Completeness) 점수를 기준으로 필터링합니다.
Verus 를 이용해 테스트 케이스가 명세를 통과하는 비율 (정확성) 과 변형된 잘못된 테스트 케이스를 명세가 거부하는 비율 (완결성) 을 계산합니다.
높은 점수를 받은 명세만 다음 라운드의 파인튜닝 데이터로 사용합니다.
3 단계: 자기 진화 증명 합성 및 자기 디버깅 (Self-Evolving Proof Synthesis & Self-Debugging)
증명 생성: 필터링된 명세와 코드를 입력으로 받아 Verus 가 검증할 수 있는 증명을 생성합니다.
자기 디버깅 (핵심 기여):
초기 모델은 많은 잘못된 증명을 생성합니다. SAFE 는 이 잘못된 증명, Verus 가 반환한 오류 메시지, 그리고 최종적으로 성공한 올바른 증명을 3 튜플 (Triplet) 로 구성하여 새로운 학습 데이터로 활용합니다.
이를 통해 모델은 처음부터 증명을 생성하는 능력뿐만 아니라, 오류 메시지를 보고 잘못된 증명을 수정 (디버깅) 하는 능력도 함께 학습합니다.
반복: 이 과정을 여러 라운드에 걸쳐 반복하며, 모델의 성능과 생성된 데이터의 양/질이 점진적으로 향상됩니다.
3. 주요 기여 (Key Contributions)
데이터 부족 해결: 인간이 작성한 Verus 증명이 거의 없는 상황에서도, 합성 데이터와 자기 진화 방식을 통해 대규모 고품질 훈련 데이터셋 (약 19,000 개 명세, 9,700 개 검증된 함수) 을 구축했습니다.
자기 디버깅 메커니즘: 단순히 증명을 생성하는 것을 넘어, 생성된 오류를 분석하고 수정하는 능력을 학습시켜 모델의 정확도를 획기적으로 높였습니다.
오픈소스 모델의 성능 향상: 형식적 검증에 익숙하지 않았던 오픈소스 모델 (DeepSeekCoder, LLaMa3.1) 을 Verus 전문 모델로 변모시켰습니다.
4. 실험 결과 (Results)
연구팀은 인간이 만든 벤치마크 (VerusBench) 와 합성 벤치마크 (CodeNet-Test) 에서 SAFE 를 평가했습니다.
성능 비교:
VerusBench: SAFE(DeepSeekCoder 기반) 는 **52.52%**의 정확도 (Accuracy@2, 자기 디버깅 포함) 를 기록했습니다. 이는 GPT-4o 의 **14.39%**보다 압도적으로 높은 수치입니다.
CodeNet-Test: SAFE 는 **48.43%**의 정확도를 달성했으며, GPT-4o 는 **0.70%**에 그쳤습니다.
자기 진화의 효과: 3 라운드의 자기 진화 과정을 거치면서 모델의 정확도가 지속적으로 향상되었습니다.
자기 디버깅의 효과: 초기 증명을 생성한 후 디버깅을 수행하는 방식 (SAFE+) 은 단순 생성 방식보다 정확도를 크게 높였습니다.
5. 의의 및 결론 (Significance)
형식적 검증의 민주화: SAFE 는 형식적 검증에 필요한 전문적인 데이터가 부족한 상황에서도 LLM 을 통해 자동화된 증명 생성을 가능하게 하여, 안전성이 중요한 Rust 코드의 검증 장벽을 낮췄습니다.
확장성: 이 프레임워크는 Verus 에 국한되지 않고, 데이터가 부족한 다른 형식적 검증 도구나 도메인에 적용 가능한 패러다임을 제시합니다.
실용성: 생성된 데이터셋과 모델은 오픈소스로 공개되어 (HuggingFace), 향후 Rust 생태계의 신뢰성 있는 소프트웨어 개발에 기여할 것으로 기대됩니다.
요약하자면, SAFE 는 데이터 부족이라는 근본적인 문제를 자기 진화 사이클과 자동화된 오류 피드백 (자기 디버깅) 을 통해 해결함으로써, 오픈소스 LLM 이 인간 전문가 수준의 Rust 코드 증명을 생성할 수 있게 만든 획기적인 연구입니다.