올바른 코드와 검증된 프로그램 사이의 간극

LLM은 컴파일되고 cargo test까지 통과하는 Rust 코드를 작성할 수 있다. 하지만 모든 가능한 입력에 대해 코드가 올바르다는 형식적 증명을 믿을 수 있게 작성하는 것은 아직 불가능하다.

문제는 Rust 문법이 아니다. 형식적 검증에서는 무엇을 증명할지 명시하고, 증명을 성립시키는 불변 조건을 찾으며, 이 둘을 검증기가 받아들이는 언어로 표현해야 한다. LLM은 소스 코드로 학습되지, 증명 행위 자체로 학습되지 않는다. 정리는 보지만, 성공한 증명에 앞선 수십 번의 실패 시도는 거의 보지 못한다.

재귀적 이진 탐색을 GPT-4에 붙여넣고 “이것을 증명해줘”라고 부탁하면, 증명처럼 보이는 것이 돌아온다. 루프 불변 조건과 전제 조건을 언급한다. 하지만 Dafny 문법을 섞거나, 존재하지 않는 보조 정리를 인용하거나, 사후 조건을 도출하기에는 너무 약한 불변 조건을 단언할 가능성이 크다. 검증해 보기 전까지는 올바른 것처럼 보인다.

Rust 형식적 검증이 실제로 어떻게 보이는가

Rust에는 여러 검증 도구가 있다. Kani은 함수의 가능한 모든 상태를 일정 한도 내에서 철저히 탐색하는 model checker다. Prusti와 Creusot은 Rust를 논리식으로 변환해 SMT solver에 성질 증명을 요청하는 연역 검증기다. 모두 특정 문법의 주석이 필요하다.

다음은 단순한 함수와 Creusot에서의 실제 연역 증명 예시다:

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot는 전제 조건 a.len() > 0이 사후 조건 result == a[0]을 보장하는지 검증한다. 논리가 단순해서 자명하다. 이제 난이도를 높여 보자:

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

불변 조건이 어려운 부분이다. 사람은 매 반복마다 무엇이 참으로 남는지 생각하며 작성한다. LLM은 학습 데이터에 그 패턴이 나타난다는 이유로 s == i * (i - 1) / 2를 추측하거나, 불변 조건을 아예 생략해서 solver가 실패하게 만들 수도 있다.

LLM에게 증명을 요청하면 무슨 일이 일어나는가

이것을 여러 모델로 테스트했다. 프롬프트는 “Creusot을 사용해 n의 계승을 계산하는, 완전한 전제 조건·사후 조건·루프 불변 조건을 갖춘 검증된 Rust 함수를 작성하라”였다.

응답은 세 가지 범주로 나뉘었다.

첫째, 겉보기에는 그럴듯하지만 잘못된 문법을 사용한 주석을 출력한 모델이 있다. #[requires(...)] 대신 #[precondition(...)]을 쓰거나, Prusti 문법과 Creusot 문법을 섞었다. 코드는 파싱조차 되지 않는다.

둘째, 문법적으로는 올바르지만 불변 조건이 너무 약한 주석을 출력한 모델이 있다. 계승 함수에는 res == fact(i) 같은 불변 조건이 필요하다. 모델은 종종 res >= i를 쓴다. 이것은 참이지만 사후 조건 증명에는 소용없다. Creusot이 목표를 도출할 수 없다고 보고하면, LLM에는 이를 고칠 메커니즘이 없다.

셋째, 불변 조건 자체는 맞았지만 보조 보조 정리를 환각으로 지어낸 응답도 있다. Creusot 표준 라이브러리에 존재하지 않는 math::fact 함수를 인용했다. 이 논리적 정의를 직접 구축하지 않으면 증명은 성립하지 않는다.

어떤 모델도 첫 시도에 검증을 통과하는 증명을 출력하지 않았다.

검증 워크플로에서 LLM이 실제로 도움이 되는 곳

이것이 LLM이 형식적 검증에 쓸모없다는 뜻은 아니다. 올바른 용도로 사용해야 한다는 뜻이다.

정형화된 코드 생성에는 능숙하다. 함수 시그니처가 주어지면, LLM은 보통 자명한 계약을 담아내는 #[requires] 절과 #[ensures] 절을 출력할 수 있다. fn divide(a: i32, b: i32) -> i32 함수에 대해, 올바르게 #[requires(b != 0)]와 #[ensures(result * b == a)]를 제안한다. 이것은 깊은 통찰은 아니지만, 타수를 아낄 수 있다.

검증기 오류 설명에도 제법 쓸만하다. Creusot이 “cannot prove loop invariant”이라고 보고하면, 그 오류 메시지를 LLM에 붙여넣으면 불변 조건이 무엇을 해야 하는지에 대한 유용한 설명을 얻는 경우가 많다. 정확한 불변 조건을 제안하지는 않지만, 탐색 공간을 좁힐 수 있다.

검증 언어 간 번역에도 유용하다. Dafny 증명을 Prusti로 포팅하고 싶을 때, LLM은 문법 대응의 상당 부분을 처리할 수 있다. 근본 논리는 같다. 이것이 바로 LLM이 뛰어나는 패턴 인식 작업이다.

근본적 한계: 증명은 탐색이지 보완이 아니다

증명을 작성하는 것은 웹 서버를 작성하는 것과 다르다. 웹 서버를 작성할 때는 올바른 답이 여러 개 있다. 증명을 작성할 때는 정답이 단 하나, 혹은 극소수의 군뿐이고 나머지는 모두 틀리다.

LLM은 다음 토큰 예측기다. 문맥을 고려해 가장 그럴듯한 후속을 생성한다. 증명 단계는 가장 그럴듯한 후속이 아니다. 증명 의무를 닫는 단계이며, 이는 20번째나 2000번째로 그럴듯한 선택지일 수도 있다.

정렬 함수가 입력의 순열을 반환함을 증명하는 것을 생각해 보자. 핵심 통찰은 보통 다중 집합을 정의하거나 출현 횟수를 세는 것이다. LLM은 길이를 비교하자고 제안할 수 있다. 이것은 필요하지만 충분하지 않다. 길이가 같다고 해서 순열임을 의미하지 않음을 인식하고, 계산 불변 조건을 도입하는 것은 사람의 몫이다.

Kani을 이용한 model checking은 불변 조건을 필요로 하지 않으므로 이런 문제의 일부를 피한다. LLM은 kani::proof 하네스를 유닛 테스트처럼 보이므로 더 안정적으로 생성할 수 있다. 하지만 Kani은 한정 검증에만 쓸 수 있다. 무한 증명이 필요하다면, 여전히 사람이 필요하다.

둘 다 사용하는 실용적인 워크플로

오늘 Rust를 검증하고 싶다면, 여기 실제로 작동하는 워크플로가 있다.

먼저 평소처럼 코드를 작성한다. cargo test를 실행한다. 그 다음 계약을 추가한다. LLM을 사용해 함수 시그니처에서 #[requires] 절과 #[ensures] 절을 생성한다. 주의 깊게 검토한다. 모델은 쉬운 것은 맞추고 어려운 것은 미묘하게 틀린다.

검증기를 실행한다. 최소한 하나의 루프에서 실패할 것이다. 오류 메시지를 가져와 어떤 불변 조건이 빠졌는지 LLM에게 설명하라고 한다. 그 설명을 답이 아닌 출발점으로 삼아, 불변 조건은 직접 작성한다.

반복한다. 검증기는 불변 조건이 충분히 강한지 알려준다. LLM은 알려주지 않는다. 모델을 문법은 알지만 증명을 완성한 적 없는 페어 프로그래머로 대하라.

이 질문에 대한 정직한 답변

LLM이 Rust의 형식적 증명을 작성할 수 있는가? 아니다. 아직은 안 된다. 논리를 이해한 사람 없이는 불가능하다.

골격 작성, 오류 설명, 도구 간 번역은 할 수 있다. 하지만 증명을 성립시키는 불변 조건이나 보조 정리, 귀납법 가설을 찾는 것은 여전히 사람의 능력이다.

분리 논리나 Hoare triple 학습을 건너뛸 수 있는 도구를 찾는다면, LLM은 그것이 아니다. 문법과 정형화된 코드를 처리해 자신은 논리에 집중할 수 있도록 학습 곡선을 완만하게 만드는 도구를 찾는다면, LLM은 시도해 볼 만하다.

불변 조건 없이 한정 검사를 원한다면 Kani부터 시작하라. 무한 증명이 필요해지면 Creusot이나 Prusti로 넘어가라. 문법을 맞추는 데 LLM을 쓰되, 증명은 직접 쓸 각오를 하라.

자주 묻는 질문

Rust에서 형식적 검증이란 무엇인가?

형식적 검증은 수학적 논리를 사용해 프로그램이 모든 가능한 입력에 대해 명세를 만족함을 증명하는 방법이다. Rust에서는 Kani, Prusti, Creusot 같은 도구가 함수에 주석을 추가해 전제 조건·사후 조건·불변 조건을 기술한다. 검증기가 이 성질들이 성립하는지 검증한다.

ChatGPT가 Kani 증명을 작성할 수 있는가?

ChatGPT는 #[kani::proof] 속성을 가진 유닛 테스트 같은 Kani 증명 하네스를 작성할 수 있다. 이 하네스는 루프 불변 조건을 필요로 하지 않아 연역 증명보다 생성하기 쉽다. 다만, 가정과 단언을 포함한 복잡한 하네스는 여전히 사람의 검토가 필요하다.

Kani와 Creusot의 차이는 무엇인가?

Kani은 한정 model checker다. 한도 내의 모든 가능한 실행 경로를 탐색해 패닉이나 단언 위반을 검출한다. Creusot은 연역 검증기다. Rust를 논리식으로 변환해 SMT solver를 사용해 모든 입력에 대한 성질을 증명한다. 무한 루프도 포함해 다룰 수 있지만, 사용자가 제공한 불변 조건이 필요하다.

왜 LLM은 루프 불변 조건에 어려움을 겪는가?

루프 불변 조건은 반복을 통해 무엇이 참으로 남는지 추론해야 하며, 이는 귀납적 추론의 한 형태다. LLM은 그럴듯한 텍스트 후속을 예측하도록 학습되지, 증명 의무를 닫는 정확한 논리적 서술을 탐색하도록 학습되지 않는다. 올바른 불변 조건은 종종 가장 그럴듯한 다음 토큰이 아니다.