클린룸 소프트웨어 공학은 코드를 컴파일하기 전에 그 정당성을 증명할 것을 요구한다. 그것은 고귀하게 들리지만, 열 개의 정수를 정렬하는 함수를 위해 루프 불변식을 세 시간 동안 작성하다 본다면 상황이 달라진다.

병목 지점은 증명 자체가 아니다. 상용구이다. 검증 조건을 생성하고, 루프에 불변식을 주석으로 다는 것, 그리고 Dafny, Why3, 또는 Z3용으로 어설션을 형식화하는 것은 지루하고, 오류가 발생하기 쉬우며, 전혀 재미없다. LLM은 이런 부분에서 놀라울 정도로 능숙하다. 하지만 실제 증명은 잘하지 못한다. 이 둘의 차이를 이해하는 것이 자동화를 유용하게 만드는 것이지, 위험하게 만드는 것이 아니다.

수동 증명 의무가 개발 속도를 죽이는 이유

클린룸에서 사양을 바탕으로 코드를 작성한 뒤, 구현이 사양과 일치함을 증명하기 위해 검증 조건(Verification Conditions, VCs)을 생성한다. 모든 루프에는 불변식이 필요하다. 모든 함수에는 전제조건과 후제조건이 필요하다. 모든 데이터 정제에는 추상화 함수가 필요하다.

소프트웨어를 출시하려는 팀에게 이것은 세금과 같다. 시니어 엔지니어가 주석과 VC 골격에 40%의 시간을 쓰고, 실제 논리적 추론에 60%의 시간을 쓸 수도 있다. 골격은 깊은 통찰을 요구하지 않는다. 인내심과 사용하는 검증기의 문법에 대한 익숙함을 요구할 뿐이다.

이것이 바로 LLM이 탁월한 패턴 매칭 작업의 유형이다. LLM은 수천 개의 루프 불변식, Dafny 메서드, SMT-LIB 파일을 보았다. 그들은 구조적으로 유효한 주석을 생성할 수 있으며, 그것은 출발점으로서 충분할 만큼 그럴듯하다.

”LLM으로 형식적 증명 자동화하기”의 실제 의미

정확히 말하자. LLM이 코드의 정당성을 증명하지는 않는다. Z3, CVC5, Dafny 검증기 같은 증명 해결기가 코드의 정당성을 증명한다. LLM은 의사코드와 해결기 사이에 놓인 인간의 노동을 자동화한다.

워크플로우는 다음과 같다:

  1. 구현과 사양을 작성한다.
  2. LLM이 후보 주석을 생성한다: 불변식, 전제조건, 후제조건, 고스트 변수.
  3. 주석이 달린 코드를 검증기에 입력한다.
  4. 검증기가 증명을 수용하거나, 반례로 거부하거나, 시간 초과가 발생한다.
  5. 증명이 실패하면 실패 원인을 검토하고 LLM에게 주석을 개선하라고 프롬프트한다.

LLM은 매우 빠르고 매우 자신감 넘치는 인턴으로, 인터넷에 있는 모든 검증 도구의 문법을 알고 있다. 그것은 완벽해 보이지만 즉시 실패하는 불변식을 기꺼이 환각으로 생성할 것이다. 괜찮다. 해결기가 환각을 잡아낸다. 가치는 백지에서 시작하는 문제를 건 넘는 데 있다.

LLM이 검증기가 확인할 수 있는 주석을 생성하는 방법

비결은 프롬프트에 있다. LLM에게 “이 함수의 정당성을 증명해줘”라고 요청하지 않는다. 특정한 형식의 특정한 결과물을 만들라고 요청한다.

예를 들어, 배열의 합을 계산하는 Python 스타일 함수가 있다면, 다음과 같이 LLM에 프롬프트한다:

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

LLM은 forall k :: 0 <= k < i ==> arr[k] is accounted for in result와 같은 루프 불변식을 포함한 Dafny 코드를 반환한다. 첫 시도에 정확한 문법을 맞추지 못할 수도 있다. 하지만 구조는 맞추며, 이것만으로도 열 분의 타이핑을 절약할 수 있다.

더 많은 제어가 필요하다면 SMT-LIB를 직접 프롬프트할 수 있다. 이것은 Dafny 같은 고수준 언어 대신 사용자 정의 검증 파이프라인을 구축할 때 유용하다.

실제 예제: Python과 Z3로 루프 불변식 자동화하기

다음은 완전하고 실행 가능한 예제다. Python을 사용해 LLM(OpenAI API)에게 간단한 배열 합 함수에 대한 루프 불변식을 생성하도록 요청한 뒤, Z3로 검증한다.

먼저 의존성을 설치한다:

pip install z3-solver openai

그런 다음 스크립트를 실행한다:

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

이 스크립트는 한 번에 함수를 검증하지 않는다. 그것이 핵심이다. LLM은 후보 불변식을 제공한다. Z3는 그것이 성립하는지 알려준다. 이 과정을 반복한다.

실무에서는 LLM 기반 검증 파이프라인을 구축하는 팀이 이 루프를 스크립트로 감싼다. 실패한 VC를 LLM에 다시 보내고, 새로운 주석을 파싱하고, 검증기를 실행하고, 오류 메시지를 개선 프롬프트로 다시 전달한다.

이것은 완전히 자율적인 검증이 아니다. 매우 빠른 타이핑 보조원이 있는 인간-인-더-루프 검증이다.

한계점: 환각 vs. 실제 오류

LLM은 너무 약한 불변식을 생성할 것이다. 해결기에 필요한 변수를 언급하는 것을 잊을 것이다. 더 이상 컴파일되지 않는 2019년 Dafny 문법을 생성할 것이다. 실제로 루프가 i < n && s == partial_sum(arr, i)를 요구할 때, i <= n만으로 충분하다고 자신감 있게 말할 것이다.

이것들 중 어느 것도 대재앙은 아니다. 해결기가 거부한다. 오류를 읽고, 다시 프롬프트한다.

진정한 위험은 반대의 경우다. LLM이 너무 강한 불변식을 생성하면, 해결기가 의도했던 것보다 더 엄격한 사양에 대해 프로그램의 정당성을 증명할 수도 있다. sum_array가 모든 배열에 대해 작동함을 증명했다고 생각하지만, 실제로는 모든 요소가 양수인 배열에 대해서만 작동함을 증명한 것이다. LLM이 그럴듯해 보이는 추가 항을 넣었기 때문이다.

생성된 사양은 항상 검토하라. LLM이 상용구를 작성한다. 논리는 당신의 것이다.

기계를 신뢰할 때와 수작업으로 작성할 때

LLM 자동화를 다음에 사용하라:

  • 전제조건과 후제조건이 명확한 간단한 함수에 대한 VC 골격 작성.
  • 증명 언어 간 문법 변환. Dafny 사양을 Why3나 SMT-LIB로 변환하는 것은 기계적이고 오류가 발생하기 쉽다. LLM은 이 부분에서 탁월하다.
  • 데이터 정제 증명을 위한 고스트 변수 생성. 패턴이 반복적이다.

LLM 자동화를 다음에 사용하지 말라:

  • 미묘한 사양 버그가 증명이 없는 것보다 더 나쁜 보안에 중요한 증명.
  • 복잡한 시간 논리나 활성 속성. LLM의 학습 데이터가 이 부분은 더 부족하고, 환각이 통과할 가능성이 더 높다.
  • 학습 데이터에 없는 새로운 알고리즘. 새로운 합의 프로토콜을 발명했다면, LLM은 어떤 불변식이 필요한지 전혀 모른다.

자주 묻는 질문

클린룸 공학에서 검증 조건이란 무엇인가?

검증 조건은 코드와 그 사양에서 생성된 논리식이다. 이 공식이 유효하다면, 코드는 사양을 올바르게 구현한 것이다. 클린룸에서는 이것들이 일반적으로 컴파일 전에 생성되며, 증명 보조기나 자동화된 해결기를 사용해 해소된다.

LLM이 Coq나 Isabelle 같은 증명 보조기를 대체할 수 있는가?

아니다. LLM은 증명 보조기가 검증할 수 있는 코드와 주석을 생성한다. 실제 증명 단계를 수행하지는 않는다. 증명이 유효한지에 대한 권한은 여전히 증명 보조기에 있다.

형식 검증 주석 생성에 가장 적합한 LLM은 무엇인가?

GPT-4o와 Claude 3.5 Sonnet은 Dafny와 SMT-LIB 문법 모두에서 잘 수행한다. 더 작은 모델은 증명 해결기가 요구하는 정밀한 문법에서 어려움을 겪는 경우가 많다. 환각적인 창작을 줄이기 위해 temperature를 낮게(0.1-0.2) 설정하라.

LLM이 잘못된 사양을 생성하는 것을 어떻게 방지하는가?

방지할 수 없다. LLM의 출력을 초안으로 취급하라. 생성된 주석을 항상 검증기를 통해 실행하라. 생성된 전제조건과 후제조건이 의도와 일치하는지 항상 읽어보라. 검증이 성공했다고 해서 사양이 올바르다고 가정해서는 안 된다.

지루한 부분부터 시작하라

당신의 팀이 클린룸이나 올바름-에-의한-구축 작업을 하고 있다면, 가장 가치 높은 자동화는 웅장한 AI 정리 증명기가 아니다. 루프 불변식을 생성하고 SMT-LIB를 형식화해 당신이 직접 하지 않아도 되게 해주는 스크립트이다.

codebase에서 가장 지루한 주석 패턴 다섯 가지를 고른다. 각각에 대한 프롬프트 템플릿을 작성한다. LLM에 입력하고, 출력을 검증하고, 통과한 것을 커밋한다. 끝이다. API 호출 한 번의 비용으로 검증 시간의 40%를 되찾은 것이다.

어려운 증명은 여전히 당신의 것이다. 하지만 적어도 백지부터 타이핑하지는 않을 것이다.