Lean on Vampire Proofs (Vampire 증명에 대한 Lean 의존) 기술 요약

이 논문은 자동定理 증명기 (ATP) 인 VAMPIRE가 생성한 증명을 신뢰할 수 있는 형식적 증명 (trusted proofs) 으로 재구성하여, LEAN 상호작용형定理 증명기 (ITP) 에서 검증하는 ongoing efforts 를 다룹니다. 자동화 된 증명 도구의 출력에 대한 사용자 신뢰를 확보하기 위해, VAMPIRE 의 증명을 LEAN 의 커널이 검증할 수 있는 형태로 변환하는 방법론과 그 결과를 제시합니다.

1. 문제 제기 (Problem)

• 신뢰성 부족: VAMPIRE 와 같은 자동定理 증명기 (ATP) 는 복잡한 논리 (1 차 논리, 고차 논리, 이론 확장) 에서 증명을 자동으로 생성하지만, 그 결과물의 정확성을 사용자가 직접 검증하기 어렵습니다.
• 검증의 한계: 기존 증명 검증 방법 (외부 ATP/SMT 솔버를 통한 재증명 또는 ITP 를 통한 단계별 재생성) 은 다음과 같은 한계가 있습니다:
  • SMT 솔버는 양자 제거 (quantifier elimination) 를 검증하지 못함.
  • 기존 증명 표준은 귀납적 증명 (inductive proofs) 을 지원하지 않음.
  • 결합법칙과 교환법칙 (AC) 을 고려한 등식 추론 (equational reasoning modulo AC) 을 ITP 에서 복원하기 매우 어려움.
• ATP 와 증명 검증 간의 긴장: ATP 의 성능 향상 (새로운 추론 규칙 도입 등) 은 증명 검증 도구의 능력을 초과하여, 자동화된 증명의 신뢰성을 확보하는 데 걸림돌이 되고 있습니다.

2. 방법론 (Methodology)

이 연구는 VAMPIRE 의 증명을 LEAN 에서 검증 가능한 형태로 재구성 (Proof Reconstruction) 하는 프레임워크를 제안합니다.

2.1 전체 아키텍처

1. VAMPIRE 실행: VAMPIRE 가 주어진 명제에 대한 증명을 찾으면, 해당 증명 로그를 추출합니다.
2. LEAN 파일 생성: VAMPIRE 의 증명 로그를 기반으로 LEAN 입력 파일을 생성합니다. 이 파일은 다음과 같이 구성됩니다:
   • 전구문 (Preamble): 필요한 심볼 선언.
   • 추론 단계 (Inference Steps): VAMPIRE 의 각 추론 단계를 LEAN 의 정리 (theorem) 로 변환하고, 이를 증명합니다.
   • 최종 증명 (Final Proof): 모든 보조 정리 (lemmas) 를 결합하여 원래 명제가 참임을 증명합니다.
3. 검증: 생성된 LEAN 파일은 LEAN 커널에 의해 검증되어, VAMPIRE 의 증명이 논리적으로 타당한지 확인합니다.

2.2 핵심 기술적 요소

• 전처리 (Preprocessing) 재구성:
  • VAMPIRE 는 CNF(Conjunctive Normal Form) 변환, Skolemization, Tseitin 변환 등을 수행합니다.
  • LEAN 에서 이를 재현하기 위해 simp 전략 (tactic) 을 사용하여 ENNF 및 CNF 변환을 수행합니다.
  • Skolemization: VAMPIRE 의 Skolem 함수 생성 로직을 LEAN 의 Classical.skolem 정리와 커스텀 전략 (symm_match, exists_prenex) 을 사용하여 정확히 매핑합니다.
• 추론 규칙 (Inference Rules) 매핑:
  • VAMPIRE 의 핵심인 Superposition Calculus (Resolution, Factoring, Paramodulation 등) 를 LEAN 정리로 변환합니다.
  • VAMPIRE 가 계산한 최일반 통일자 (MGU) 를 LEAN 의 have 문에 주입하고, grind 전략을 사용하여 구체적인 증명 단계를 재구성합니다.
  • 등식 추론 시 AC(결합/교환) 규칙 적용이 필요한 경우, 이를 처리하는 커스텀 전략을 사용합니다.
• AVATAR 처리:
  • VAMPIRE 의 효율적인 증명을 돕는 AVATAR 프레임워크 (명제 논리 분할 및 SAT 솔버 활용) 를 지원합니다.
  • 명제 레이블을 LEAN 변수로 선언하고, 최종 모순 (SAT refutation) 은 bv_decide 전략을 통해 SAT 솔버의 결과를 LEAN 내에서 검증합니다.

3. 주요 기여 (Key Contributions)

• 신뢰성 있는 증명 생성: VAMPIRE 의 증명을 LEAN 커널이 검증하는 형태로 변환하여, 자동화 된 증명 결과에 대한 높은 수준의 신뢰를 제공합니다.
• 확장 가능한 프레임워크: 1 차 논리 (등식 포함) 를 기반으로 하며, 다중 정렬 (multi-sorted) 논리 등으로의 확장을 계획하고 있습니다.
• LEAN-ATP 통합의 새로운 지평: 기존 Lean-auto 와 달리, VAMPIRE 의 증명 검증에 특화된 전략 (tactics) 을 제공하며, SMT 솔버가 아닌 LEAN 자체에 신뢰를 위임하여 신뢰 컴퓨팅 베이스 (Trusted Computing Base) 를 줄입니다.
• HAMMER 시스템으로서의 비전: 장기적으로 VAMPIRE 를 LEAN 을 위한 강력한 해머 (Hammer) 시스템으로 발전시키는 첫걸음입니다.

4. 실험 결과 (Results)

연구진은 TPTP 라이브러리 (버전 9.2.1) 의 17,603 개 문제 (CNF 및 FOF) 를 사용하여 실험을 수행했습니다.

• 성공률:
  • CNF 문제: 98% 성공률 (3,785/3,860).
  • FOF 문제: 85% 성공률 (3,296/3,897).
• 실패 원인:
  • LEAN 파일이 너무 커서 처리 불가.
  • 복잡한 추론 단계 재구성 실패 또는 특정 VAMPIRE 규칙 미지원.
  • LEAN 전략 타임아웃.
• 성능 분석:
  • 오버헤드: 증명 생성을 위해 VAMPIRE 실행 시 약간의 오버헤드가 발생하지만, 전체 증명 시간에는 큰 영향을 미치지 않습니다.
  • 상관관계: VAMPIRE 의 증명 탐색 시간과 LEAN 의 증명 재구성/검증 시간 사이에는 강한 상관관계가 없으며, 증명 길이가 길어질수록 LEAN 검증 시간이 선형적으로 증가하는 경향이 있습니다.

5. 의의 및 결론 (Significance & Conclusion)

• 신뢰성 확보: 자동定理 증명기의 "블랙박스" 성격을 해소하고, LEAN 의 검증 능력을 통해 증명의 정확성을 보장함으로써, 사이버보안, 소프트웨어 분석, 수학적 증명 등 중요한 분야에서 ATP 사용에 대한 신뢰를 높입니다.
• 기술적 진전: 200 개 이상의 추론 규칙을 가진 VAMPIRE 의 핵심 규칙들을 LEAN 에서 검증 가능하게 매핑하는 데 성공했습니다.
• 미래 작업: 현재는 VAMPIRE 의 모든 추론 규칙을 지원하지는 못하므로, Duper ATP 와 같은 증명 생성 도구를 활용하거나, VAMPIRE 내부 정보를 더 효과적으로 활용하는 전용 전략 개발 등을 통해 효율성과 커버리지를 개선할 예정입니다.

이 논문은 자동화 된 추론과 상호작용형 증명 간의 간극을 메우는 중요한 사례로, 형식적 방법론의 신뢰성과 실용성을 동시에 높이는 방향을 제시합니다.