💻 computer science

Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

본 논문은 Rust 프로그램에 대한 690 만 개의 형식적 증명을 생성하는 확장 가능한 데이터 합성 파이프라인인 VeruSyn 을 소개하며, 이를 통해 미세 조정된 Qwen2.5-Coder-32B 모델이 최첨단 상용 및 연구 모델에 비해 증명 합성 분야에서 뛰어난 비용 효율성과 성능을 달성할 수 있음을 보여줍니다.

원저자: Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R. Lorch, Yuan Yao, Xiaoxing Ma

게시일 2026-05-12

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R. Lorch, Yuan Yao, Xiaoxing Ma

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

상상해 보세요. 매우 재능 있지만 경험이 부족한 견습 프로그래머가 있다고 가정합시다. 당신은 그에게 운영체제나 은행 보안 소프트웨어와 같은 치명적인 시스템의 코드를 작성하게 하고, 결정적으로 그 코드가 100% 버그가 없음을 증명하는 수학적 증명을 작성하게 하고 싶어 합니다.

문제는 이 견습생은 코드 작성에는 능숙하지만, 이러한 증명 작성에는 매우 서툴다는 점입니다. 배울 만한 예시가 부족하고, '전문가'(가장 비싸고 강력한 AI 모델) 들은 모든 단일 작업에 고용하기에는 비용이 너무 많이 듭니다.

이 논문은 방대한 양의 자체 생성된 연습 자료를 활용하여, 그 경험이 부족한 견습생을 증명 작성의 대가로 변모시키도록 설계된 교묘한 '훈련 캠프'인 VeruSyn을 소개합니다.

다음은 그들이 어떻게 했는지를 간단한 단계로 분해한 내용입니다:

1. 문제: 연습 교재 부족

수학적 증명의 기반이 되는 형식적 검증 (formal verification) 세계에는 Rust 프로그래밍 언어를 위한 Verus라는 도구가 있습니다. 이는 당신의 코드가 완벽한지 확인하는 엄격한 교사 같은 역할을 합니다.

문제점: 이러한 완벽한 증명과 함께 제공되는 실제 Rust 코드 예시는 매우 드뭅니다. 마치 단 세 곡의 노래만 들어보며 피아노 연주법을 배우려는 것과 같습니다.
결과: 소규모이고 저렴한 AI 모델들은 충분한 예시를 보지 못했기 때문에 이러한 증명을 작성하는 법을 배울 수 없습니다. 오직 가장 비싸고 '초지능' AI 모델만이 이를 수행할 수 있으며, 이를 실행하는 데는 천문학적 비용이 듭니다.

2. 해결책: 'VeruSyn' 훈련 캠프

연구자들은 연습 문제와 해답의 거대한 라이브러리를 생성하는 파이프라인을 구축했습니다. 그들은 기존 교재를 단순히 복사 - 붙여넣기 한 것이 아니라, 새로운 교재를 생산하는 공장을 세웠습니다. 그들은 세 가지 구체적인 전략을 사용했습니다:

전략 A: '자기 학습' 루프 (규모 확장)

수학 문제를 작성하고 즉시 그것을 풀도록 요구받는 학생을 상상해 보세요.

AI 는 Rust 코드와 그 자체의 증명을 동시에 생성하도록 훈련되었습니다.
단점: AI 는 실수를 반복하거나 동일한 문제를 계속 만들어냈습니다.
해결책: 그들은 필터를 구축했습니다. AI 가 엄격한 'Verus 교사'가 검증할 수 없는 증명을 작성하면, 그 오류를 AI 에게 되돌려 주어 '디버깅'하고 수정하도록 요청했습니다. 이를 690 만 개의 고유하고 검증된 프로그램을 얻을 때까지 반복했습니다. 이는 견습생에게 단 세 권이 아닌 수백만 권의 연습 교재가 담긴 도서관을 제공하는 것과 같습니다.

전략 B: '교과서' 접근법 (범위 확장)

'자기 학습' 루프는 간단한 문제를 만드는 데는 훌륭했지만, 실제 시스템에서 발견되는 복잡한 내용은 놓쳤습니다.

해결책: 연구자들은 이 도구를 위한 공식 Verus 튜토리얼(교과서) 을 가져와 '루프 처리 방법'이나 '수학 처리 방법'과 같은 구체적인 수업 단위로 분해했습니다.
그들은 AI 가 교과서의 각 수업에 대해 수천 개의 새로운 예시를 생성하도록 강요했습니다. 이를 통해 견습생이 쉬운 규칙뿐만 아니라 모든 규칙을 학습하도록 보장했습니다.

전략 C: '멘토의 일기' (추론 확장)

수백만 개의 예시가 있더라도 AI 는 매우 어렵고 복잡한 문제를 해결하는 데 어려움을 겪었습니다. 규칙은 알았지만, 어려운 퍼즐을 어떻게 풀어나갈지 몰랐기 때문입니다.

해결책: 그들은 '초전문가' AI(비싼 모델) 를 고용하여 몇 가지 정말 어려운 문제를 풀게 했습니다. 하지만 최종 답변만 저장한 것이 아니라, 전체 사고 과정을 기록했습니다: 저지른 실수, 읽은 오류, 변경된 코드, 그리고 각 단계에서 사용된 추론입니다.
그들은 이러한 '사고 로그'를 새로운 유형의 훈련 데이터로 변환했습니다. 이는 마치 최종 케이크만 보여주는 것이 아니라, 마스터 셰프가 타버린 수플레를 어떻게 단계별로 고쳤는지 보여주는 일기를 견습생에게 주는 것과 같습니다.

3. 결과: 저렴한 대가

이 방대하고 고품질의 데이터셋으로 중형 AI 모델 (Qwen2.5-Coder-32B) 을 훈련시킨 후, 결과는 놀라웠습니다:

성능: 훈련된 모델은 가장 비싼 '초전문가' 상업용 모델과 거의同等하게 증명 작성에 능숙해졌습니다.
비용: 이것이 큰 승리입니다. 비싼 모델은 단일 복잡한 증명 작업을 해결하는 데 약 8.00 달러가 듭니다. 반면, 새로 훈련된 모델은 동일한 작업을 수행하는 데 0.17 달러만 듭니다.
효율성: 일부 테스트에서는 새로운 모델이 몇 번 시도 (디버깅) 할 수 있도록 허용되었을 때, 비용이 50 분의 1 수준인 반면 실제로는 비싼 모델보다 더 나은 성능을 보였습니다.

비유 요약

비싼 AI 모델은 타고난 재능을 지녔지만 훈련과 경쟁을 위해 막대한 급여가 필요한 올림픽 선수라고 생각하세요.
새로운 VeruSyn 접근법은 첨단 스포츠 아카데미와 같습니다.

그들은 평범한 선수 (중형 AI) 를 데려왔습니다.
수백만 개의 연습 드릴이 담긴 도서관을 제공했습니다 (자기 합성).
선수가 규칙서의 모든 구체적인 동작을 연습하도록 했습니다 (튜토리얼 합성).
올림픽 챔피언이 경기 중 내면의 독백을 하는 비디오 테이프를 선수에게 제공했습니다 (에이전트 궤적).

결과? 이 특정 훈련을 받은 평범한 선수는 올림픽 챔피언과 경쟁할 수 있지만, 운영 비용은 그 일부에 불과합니다.

그들이 주장하는 것 (그리고 주장하지 않는 것)

주장: 그들은 690 만 개의 검증된 프로그램으로 구성된 데이터셋을 만들었습니다. 그들은 Rust 시스템에 대한 형식적 증명 생성에 매우 정확한 모델을 훈련시켰습니다. 그들은 이것이 현재 최상위 상업용 모델을 사용하는 것보다 훨씬 저렴함을 증명했습니다.
주장하지 않는 것: 그들은 이것이 전 세계의 모든 소프트웨어 버그를 해결한다고 주장하지 않으며, Rust(특히 Verus 도구를 사용한 경우) 외의 언어에서도 작동한다고 주장하지 않습니다. 그들은 소프트웨어 자체의 더 넓은 사회적 영향이 아니라, 증명을 생성하는 비용과 정확성에 엄격히 초점을 맞춥니다.

기술 요약: 루스트 시스템에서 증명 합성을 위한 비용 절감을 위한 시드 학습 데이터 확장

1. 문제 제기

대규모 언어 모델 (LLM) 이 생성한 코드의 정확성은 보안 및 신뢰성 필수 시스템 소프트웨어의 경우 여전히 큰 과제로 남아 있습니다. LLM 은 강력한 코드 생성 능력을 입증해 왔지만, 안전성, 보안성 또는 기능적 속성을 위반하는 문법적으로 올바른 코드를 자주 생성합니다. 이에 대한 잠재적 해결책은 LLM 에게 코드와 함께 형식적 정확성 증명을 생성하도록 요구하는 것입니다.

그러나 시스템 소프트웨어 (특히 루스트용 최첨단 검증 도구인 Verus를 사용) 에 대한 형식적 증명을 생성하는 것은 표준 코드 생성보다 훨씬 높은 추론 능력을 요구합니다. furthermore, 이 분야는 심각한 데이터 부족에 시달리고 있습니다. 기존 검증된 루스트 시스템은 드물며, 사용 가능한 데이터셋 (예: SAFE, AlphaVerus) 은 규모와 다양성이 제한적입니다. 이전 연구에 따르면 오직 고비용의 대규모 상용 모델 (예: Claude Sonnet 4.5) 만이 이러한 증명을 효과적으로 생성할 수 있는 능력을 갖추고 있으며, 작거나 저렴한 모델은 실패합니다. 이 논문이 다루는 핵심 문제는 다음과 같습니다: 작은 LLM 을 위해 고품질이고 대량의 학습 데이터를 합성함으로써 어떻게 저비용으로 코드 증명을 효과적으로 생성할 수 있는가?

2. 방법론: VeruSyn 파이프라인

저자들은 현재까지 가장 큰 규모의 Verus 검증 프로그램을 생성하도록 설계된 데이터 합성 파이프라인인 VeruSyn을 제안합니다. 이 파이프라인은 이전 합성 노력의 세 가지 특정 한계인 제한된 규모, 좁은 기능 범위, 낮은 추론 복잡성을 해결합니다. VeruSyn 은 세 가지 다른 합성 접근 방식을 반복적이고 조정된 방식으로 통합합니다:

2.1 프로그램 수 확장 (자기 합성)

기존 벤치마크 스위트를 번역하는 데 의존하여 데이터셋 크기를 소스에 의해 제한하는 이전 방법과 달리, VeruSyn 은 자기 합성 (self-synthesis) 전략을 채택합니다.

과정: LLM 을 SAFE 데이터셋으로 미세 조정하여, 기존 소스 프로그램에 의존하지 않고 처음부터 루스트 프로그램과 해당 Verus 명세 및 증명을 직접 생성하도록 합니다.
반복: 이 과정은 SAFE 데이터셋으로 미세 조정된 베이스 모델로 시작하여 초기 프로그램을 생성합니다. 합성이 진행됨에 따라, 새로 생성되고 검증 및 디버깅된 데이터로 모델을 반복적으로 미세 조정하여 생성 능력을 향상시킵니다.
종료: 배치 내 중복 프로그램의 비율이 95% 에 도달할 때 합성을 중단하여 다양성을 보장합니다.

2.2 기능 범위 확장 (튜토리얼 기반 합성)

이전 데이터셋이 단순한 루프 불변식에 치우친 편향을 극복하기 위해, VeruSyn 은 구조화된 지식 소스로 Verus 튜토리얼을 사용합니다.

과정: 전문가들이 Verus 튜토리얼의 모든 장에서 핵심 지식 포인트를 포괄하는 "시드 프로그램"을 수동으로 작성합니다.
합성: 증명 생성 모델이 각 시드에 대해 수천 개의 새로운 프로그램을 생성하도록 프롬프트를 입력하며, 이는 해당 튜토리얼 장에 명시적으로 안내됩니다.
목표: 이는 알고리즘 벤치마크에서는 종종 누락되지만 실제 시스템 검증에 필수적인 다양한 Verus 기능 (예: 양화사, 비선형 산술, 비트 벡터) 을 체계적으로 포괄하도록 보장합니다.

2.3 추론 복잡성 확장 (에이전트 궤적 합성)

긴 추론 체인이 필요한 복잡하고 실제적인 시스템 증명을 처리하기 위해, VeruSyn 은 에이전트 궤적에서 파생된 생각의 사슬 (Chain-of-Thought, CoT) 데이터를 통합합니다.

과정: 최첨단 코딩 에이전트 (Claude Sonnet 4.5 기반) 에게 VeruSAGE-Bench 의 실제 시스템 검증 문제 세트에 대한 증명을 작성하도록 할당합니다.
데이터 수집: 에이전트의 추론, 행동 (파일 읽기, Verus 호출, 오류 분석, 증명 편집) 및 최종 성공 궤적에 대한 완전한 로그를 수집합니다.
통합: 이러한 궤적은 학습 데이터로 변환되어 모델에게 여러 단계에 걸쳐 복잡한 검증 오류를 디버깅하고 추론하는 방법에 대한 예시를 제공합니다.

2.4 부정 방지 및 필터링

파이프라인의 핵심 구성 요소는 "부정" (예: 증명을 단순히 참이 되도록 명세를 수정하거나, 검증을 건너뛰기 위해 무한 루프를 추가하거나, assume 문 사용) 을 방지하기 위한 엄격한 필터링 과정입니다.

메커니즘: 파이프라인은 명세 호환성을 확인하기 위해 tree-sitter 파서를 사용하고, 금지된 키워드 (예: assume) 를 감지하며, 종결을 위해 decreases 절을 강제합니다.
디버깅: 검증되지 않은 프로그램은 오류 보고서와 함께 모델에게 피드백되어 디버깅됩니다. 성공적으로 검증된 쌍만 유지됩니다.

3. 주요 기여

데이터셋 규모: 각각 형식적 명세와 증명을 갖춘 690 만 개의 Verus 검증 루스트 프로그램 합성. 이는 동종 데이터셋 중 가장 큰 규모입니다.
기능 다양성: 이 데이터셋은 20 개의 핵심 포인트 중 12~15 개의 다양한 Verus 지식 포인트를 포괄하여, 의미 있는 4~5 개 포인트만 포괄했던 기존 데이터셋 (SAFE 및 AlphaVerus) 을 크게 능가합니다.
CoT 통합: 실제 시스템 작업에 대한 에이전트 궤적에서 파생된 4,557 개의 긴 CoT 인스턴스 포함.
모델 성능: 상용 모델의 비용의 일부로 경쟁력 있는 증명 합성 능력을 달성하는 미세 조정된 Qwen2.5-Coder-32B-Instruct 모델.

4. 평가 결과

저자들은 VeruSyn 으로 미세 조정된 모델을 두 가지 벤치마크인 VerusBench(150 개 알고리즘 작업) 와 VeruSAGE-Bench(실제 루스트 시스템에서 추출된 849 개 작업, 데이터 유출 방지를 위해 289 개 제외) 에서 평가했습니다.

4.1 정확도

시스템 증명 (VeruSAGE-Bench): 디버깅 없이 VeruSyn 모델은 **39%**의 성공률 (Accuracy@100) 을 달성하여, 원시 Qwen 모델 (10%), SAFE 미세 조정 모델 (6%), AlphaVerus 미세 조정 모델 (11%), 그리고 상용 o4-mini(15%) 를 크게 능가했습니다.
디버깅 포함: 5 회 디버깅 후 VeruSyn 모델은 **49%**의 정확도에 도달했으며, 이는 고비용인 Claude Sonnet 4.5(54%) 에 비해 약간 낮습니다.
알고리즘 증명 (VerusBench): 모델은 디버깅 없이 **75%**의 정확도를 달성하여 Claude Sonnet 4.5(72%) 를 약간 능가했습니다.

4.2 비용 효율성

이 논문은 비용의 극적인 감소를 강조합니다:

작업당 비용: VeruSyn 모델은 작업당 약 $0.17**(디버깅 없이) 및 **$ 0.61(디버깅 포함) 의 비용이 듭니다.
비교: 이는 Claude Sonnet 4.5($8.04, 디버깅 없이) 보다 약 47 배 저렴하며, o4-mini($3.39) 보다도 훨씬 저렴합니다.
절충: 5 회 디버깅을 거친 VeruSyn 모델 ($0.61) 은 디버깅 없이 Claude Sonnet 4.5(46%) 보다 높은 정확도 (49%) 를 달성하여, 우수한 성능을 위해 13 배의 비용 절감을 실현합니다.

4.3 제거 실험

데이터 구성 요소: 자기 합성/튜토리얼 데이터 (1 부) 또는 CoT 데이터 (2 부) 중 하나를 제거하면 실제 시스템 작업에서 성능이 크게 저하되었습니다. 1 부는 알고리즘 작업에 필수적이었으며, 2 부는 복잡한 시스템 증명에 필수적이었습니다.
교사 모델: CoT 생성에 더 강력한 교사 모델 (Claude Sonnet 4.5) 을 사용한 경우 하류 성능이 o4-mini 를 교사 모델로 사용할 때 (15%) 비해 현저히 향상되었습니다 (39%).

5. 중요성 및 주장

이 논문은 VeruSyn이 고품질 대규모 합성 데이터가 형식 검증 분야에서 작고 비용 효율적인 오픈소스 모델과 고비용 상용 모델 간의 격차를 해소할 수 있음을 보여준다고 주장합니다.

비용 - 증명 절충: 이 연구는 비용 효율성에 대한 새로운 벤치마크를 확립하여, 합성 데이터로 미세 조정된 32B 파라미터 모델이 추론 비용의 일부로 4.5 배 더 큰 상용 모델을 능가하거나 동등한 성능을 낼 수 있음을 보여줍니다.
확장성: 이 방법론은 자기 합성 및 튜토리얼 기반 합성이 기존 벤치마크 스위트의 한계를 넘어 확장되어 형식 검증 도구를 위한 "무제한" 학습 데이터 공급을 창출할 수 있음을 입증합니다.
일반화: 결과는 합성된 데이터가 모델에게 문법뿐만 아니라 실제 시스템 소프트웨어 검증을 위해 필요한 복잡한 추론 패턴까지 효과적으로 가르친다는 것을 시사하며, 이는 이전에는 가장 큰 모델에만 독점적인 능력으로 여겨졌습니다.

저자들은 학습 데이터셋이 HuggingFace 에서 제공되며, 시스템 소프트웨어 개발에서 형식 검증의 진입 장벽을 낮추는 것을 목표로 한다고 결론지었습니다.