논문 개요: Cobblestone

이 논문은 형식적 검증 (Formal Verification) 도구인 Coq 에서 증명 (Proof) 을 자동화하기 위한 새로운 접근법인 Cobblestone을 제안합니다. 기존의 대규모 언어 모델 (LLM) 기반 증명 생성 도구가 가진 한계를 극복하고, LLM 의 고수준 계획 능력과 국소적 탐색의 장점을 결합한 분할 정복 (Divide-and-Conquer) 전략을 도입했습니다.

1. 문제 정의 (Problem)

• 형식적 검증의 비용: Coq 나 Lean 과 같은 증명 보조기 (Proof Assistants) 를 사용한 형식적 검증은 소프트웨어의 결함을 수학적으로 증명하여 높은 신뢰성을 보장하지만, 증명을 작성하는 데 막대한 전문 지식과 수동 노력이 필요합니다.
• 기존 자동화 도구의 한계:
  • 전체 증명 생성 (Whole-proof generation): LLM 에게 전체 증명을 한 번에 생성하게 하는 방식은 고수준의 추론이 필요하며, 중간 상태 (Intermediate state) 에 대한 접근이 부족하여 실패 시 전체를 다시 시도해야 하는 비효율이 발생합니다.
  • 전술 단위 탐색 (Tactic-by-tactic search): 한 단계씩 증명을 생성하는 방식은 국소적 상태에 의존하지만, 고수준의 증명 계획을 고려하지 않아 복잡한 검색 공간에서 실패하기 쉽습니다.
  • 기존 ML/LLM 도구: 기존 도구들은 원하는 속성의 약 1/3 만 증명할 수 있으며, 데이터 누출 (Training data leakage) 문제나 LLM 의 불완전한 추론 능력으로 인해 한계가 명확합니다.

2. 방법론 (Methodology)

Cobblestone 은 전체 증명을 한 번에 생성하거나 전술 단위로 나누는 극단적인 접근 사이의 중간 지점을 차지합니다. 핵심 아이디어는 **전체 증명 시도의 트리 구조를 활용하여 유효한 부분 증명과 실패한 부분을 국소화 (Localize)**하고, 실패한 부분에 대해 재귀적으로 해결책을 찾는 것입니다.

주요 구성 요소:

1. 분할 정복 알고리즘 (Divide-and-Conquer):

   • Cobblestone 은 먼저 전체 목표를 증명하려 시도합니다.
   • 실패할 경우, 생성된 증명 스크립트를 분석하여 **작동하는 부분 (Working parts)**과 **실패한 부분 (Broken parts)**으로 나눕니다.
   • 작동하는 부분은 유지하고, 실패한 부분 (미해결 하위 목표) 에 대해 재귀적으로 Cobblestone 을 호출하여 해결합니다.
   • 이 과정을 통해 복잡한 증명을 더 간단한 하위 목표로 분해하여 해결 확률을 높입니다.

2. 안전 모드 실행 (Fail-Safe Mode):

   • LLM 이 생성한 증명 스크립트는 오류가 있을 수 있습니다. 기존 방식은 첫 번째 오류에서 실행이 중단되어 그 이후의 올바른 코드를 잃어버립니다.
   • Cobblestone 은 Fail-Safe Mode를 도입하여 증명 스크립트를 실행합니다. 오류가 발생하면 해당 전술과 이후 부분을 admit (임시 증명) 으로 대체하고, 오류가 발생한 가장 깊은 중첩 하위 증명 (Subproof) 만을 "진행 중 (In progress)"으로 표시합니다.
   • 이를 통해 오류가 발생한 지점 이전의 올바른 부분 증명을 보존하고, 재귀 호출을 통해 해당 부분만 재시도할 수 있게 합니다.

3. CoqHammer 통합:

   • LLM 만 의존하지 않고, SMT 솔버 기반의 자동 증명 도구인 CoqHammer를 활용합니다.
   • 초기 시도뿐만 아니라, 재귀 호출 과정에서 생성된 하위 목표에 대해 CoqHammer 를 적용하여 증명을 성공시킬 확률을 높입니다.

4. LLM 샘플링 전략:

   • 전체 증명 스크립트를 생성하기 위해 GPT-4 와 같은 LLM 을 사용합니다.
   • 컨텍스트 정보 (이전 증명된 정리 등) 와 체인 오브 씽킹 (Chain-of-Thought) 유무에 따라 4 가지 변형으로 프롬프트를 생성하여 다양한 증명을 샘플링하고, 그중 가장 유효한 것을 선택합니다.

5. 외부 입력 활용 (Oracle):

   • 완전 자동화 모드 외에도, 사용자가 또는 다른 도구로부터 **관련 정리 (Relevant lemmas)**나 **증명 구조 계획 (Proof structure)**을 입력받아 성능을 향상시킬 수 있도록 설계되었습니다.

3. 주요 기여 (Key Contributions)

1. Cobblestone 도구 개발: LLM 기반의 분할 정복 증명 생성 접근법을 최초로 제안했습니다. 이는 전체 증명 생성과 전술 단위 탐색 사이의 중간 전략으로, 부분적 성공을 활용하여 전체 증명을 완성합니다.
2. Fail-Safe Mode 도입: 증명 스크립트 실행 시 오류를 국소화하고, 오류가 발생한 부분만 재시도하도록 하여 기존 LLM 기반 도구의 실패를 극복하는 새로운 메커니즘을 제시했습니다.
3. 광범위한 평가 및 비교: CoqGym, coq-wigderson, coq-bb5, PnVRocqLib 등 4 개의 벤치마크에서 기존 비-LLM 도구 (Proverbot9001, CoqHammer 등) 와 최신 LLM 기반 도구 (PALM, Rango 등) 와 비교 평가했습니다.
4. 재현성 보장: 모든 코드, 실험 스크립트, 데이터를 공개하여 연구의 재현성을 보장했습니다.

4. 실험 결과 (Results)

• 성능 향상:
  • CoqGym100: Cobblestone 은 48% 의 정리를 증명하여, 기존 비-LLM 도구들의 합 (33%) 보다 우세하며, 단일 실행 PALM(34%) 보다도 높은 성능을 보였습니다.
  • Wigderson100 (GPT-4 학습 데이터 이후 프로젝트): 38% 증명 성공률을 기록하여, 기존 도구들 (CoqHammer 27%, Proverbot9001 10%) 을 크게 능가했습니다.
  • 상호 보완성: Cobblestone 은 다른 LLM 기반 도구 (PALM, Rango) 가 증명하지 못하는 정리들을 증명하여, 도구들을 결합했을 때 전체 증명률이 크게 향상됨을 보였습니다 (예: CoqGym100 에서 Cobblestone + PALM 은 61% 증명).
• 비용 및 시간:
  • 평균 실행 비용: $1.25
  • 평균 실행 시간: 14.7 분
  • 이는 고비용의 LLM 사용에도 불구하고 효율적인 분할 정복 전략 덕분에 달성된 수치입니다.
• 외부 입력의 효과:
  • 완벽한 전제 (Perfect premises) 나 증명 분해 (Perfect decomposition) 정보를 오라클로 제공받을 경우, CoqGym100 에서 **58%**까지 증명 성공률을 높일 수 있었습니다.
• 모델 일반화: GPT-4 외에도 GPT-3.5-turbo 와 Claude 3 Opus 와 같은 다른 LLM 모델에서도 효과적으로 작동함을 확인했습니다.

5. 의의 및 결론 (Significance)

• 자동화 형식 검증의 새로운 패러다임: LLM 의 추론 능력을 활용하면서도, LLM 의 불완전성을 보완하기 위해 증명의 트리 구조를 활용하고 재귀적으로 문제를 분해하는 접근법은 형식적 검증 자동화의 새로운 방향을 제시합니다.
• 실용성: 상대적으로 낮은 비용과 시간으로 기존 도구들이 증명하지 못했던 복잡한 정리들을 해결할 수 있음을 입증했습니다.
• 인간 - AI 협업 가능성: 외부 입력 (사용자의 힌트나 다른 도구의 결과) 을 쉽게 통합할 수 있어, 인간 엔지니어나 다른 자동화 도구와의 협업 (Interactive/Semi-automated verification) 을 통한 증명 성공률 향상의 가능성을 보여주었습니다.

결론적으로, Cobblestone 은 LLM 기반의 형식적 증명 생성 분야에서 부분적 성공을 활용하고 오류를 국소화함으로써 기존 방법론들의 한계를 극복하고, 더 높은 증명 성공률과 효율성을 달성한 획기적인 도구입니다.