Case Study: Saturations as Explicit Models in Equational Theories

논문 요약: 등식 이론에서의 포화 (Saturation) 를 명시적 모델로 활용

1. 연구 배경 및 문제 제기 (Problem)

• ATP 의 한계: 자동화 정리 증명기 (ATP) 는 가설을 반증할 때 '포화 (saturation)'된 절 (clause) 집합을 생성하여 모순을 유도하거나, 모순이 없음을 보여줍니다. 그러나 생성된 포화 집합은 불투명한 '증명서'에 불과하며, 인간이 이해하거나 검증하기 어렵습니다.
• 명시적 모델의 부재: 특히 반증 (counter-example) 이 필요한 경우, ATP 는 명시적인 모델을 제공하지 못합니다. 유한 모델 빌더 (Finite Model Builder, FMB) 를 사용할 수 있지만, 많은 대수적 구조의 경우 반례가 무한한 모델로만 존재하거나, 유한 모델의 크기가 너무 커서 (보통 도메인 크기 20 이상) 계산이 불가능한 경우가 많습니다.
• ETP 의 필요성: 테런스 타오 (Terence Tao) 가 제안한 '등식 이론 프로젝트 (Equational Theories Project, ETP)'는 2 천만 개 이상의 함축 (implication) 관계를 분류하는 대규모 협업 프로젝트입니다. 여기서 수학적 함축이 성립하지 않을 때, 왜 성립하지 않는지에 대한 명확한 반례 (모델) 가 필요했으나, 기존 ATP 는 이를 제공하지 못했습니다.

2. 방법론 (Methodology)

저자들은 **단위 등식 조각 (Unit Equational Fragment)**에 초점을 맞춰, ATP 의 포화 집합을 명시적인 모델로 변환하는 방법을 제시합니다.

• 단위 등식 조각 (Unit Equational Fragment): 모든 변수가 보편 양화 (universally quantified) 된 등식과 기본 부등식 (ground disequations) 만을 허용하는 논리 조각입니다. 이는 대수적 구조를 표현하기에 강력하며, 호른 절 (Horn fragment) 등을 효율적으로 포함합니다.
• 포화 집합을 재작성 시스템으로 해석:
  • 포화 집합 $E$와 내부 항 순서 (term ordering) $\prec$가 주어졌을 때, 이를 **수렴하는 재작성 시스템 (convergent rewrite system)**으로 해석합니다.
  • 모델 구성:
    1. 도메인: 시그니처의 모든 기본 항 (ground terms) 으로 구성된 헤르브란드 우주 (Herbrand universe).
    2. 동치 관계: 두 항 $s, t$가 동치인 것은 $E$에 의해 재작성된 **정규형 (normal form)**이 동일한 경우 ($\lfloor s \rfloor = \lfloor t \rfloor$) 로 정의합니다.
    3. 정규화 함수: 항을 $E$의 규칙에 따라 더 이상 재작성할 수 없을 때까지 반복하여 정규형을 계산합니다.
  • 이 모델은 무한할 수 있지만, 기본 항 (ground terms) 에 대해서는 계산 가능하고 결정적입니다.
• 구현: 이 방법을 Vampire와 E라는 두 가지 주요 ATP 에 구현하여, 포화 상태에 도달했을 때 명시적인 재작성 시스템 (모델) 을 출력하도록 수정했습니다.

3. 주요 기여 (Key Contributions)

1. 명시적 무한 모델 생성: ATP 의 포화 집합을 수학적 모델 (특히 무한 반례) 로 직접 변환하는 완전한 구성 방법을 제시했습니다. 이는 기존에 ATP 사용자들에게 잘 알려지지 않았던 이론적 사실을 실용화한 것입니다.
2. 검증 가능한 증명서 (Certificates) 생성: 생성된 재작성 시스템이 실제로 유효한 모델인지 확인하기 위해, CSI(confluence checker)와 TTT2(termination prover) 같은 검증 도구를 활용했습니다. 이 도구들은 CeTA를 통해 Isabelle/HOL 기반의 IsaFoR 라이브러리를 사용하여 결과를 검증합니다.
3. ETP 적용 및 확장: ETP 의 304 개의 문제 (유한 모델 빌더로 해결되지 않은 것들) 에 이 방법을 적용하여, 그 중 196 개는 유한 반례가 없음을 확인하고, 나머지 108 개를 포함한 총 261 개의 검증된 무한 반례를 생성했습니다.

4. 실험 결과 (Results)

• 데이터: ETP 의 2200 만 개 중 Vampire 로 해결되지 않은 304 개의 문제 (유한 모델 빌더 실패) 를 대상으로 실험했습니다.
• 성공률:
  • 304 개 중 261 개의 포화 집합은 사전 정렬된 (pre-ordered, $l \succ r$) 등식으로 구성되어 있어, 자동으로 재작성 시스템으로 변환 가능했습니다.
  • 이 261 개의 시스템은 CSI 와 TTT2 를 통해 **결합성 (confluence)**과 **종료성 (termination)**이 검증되었으며, CeTA 를 통해 독립적으로 검증 가능한 증명서를 생성했습니다.
  • 나머지 43 개는 등식의 방향이 정렬되지 않아 자동 검증이 어렵지만, 여전히 모델 구성은 가능합니다.
• 구체적 사례:
  • 예: 결합법칙이 교환법칙을 함의하는지 여부 (118 번과 274 번 등식 간의 함축) 는 반례가 존재하며, 이는 유한 모델이 아닌 무한 모델로만 표현됩니다. 생성된 재작성 시스템 (Fig. 1) 은 이 무한 반례를 명확하게 보여줍니다.
  • 일부 경우 (예: 477 번과 1426 번) 는 원래 문제 자체가 이미 포화 상태였으며, 추가적인 파생 규칙 없이도 모델이 구성되었습니다.

5. 의의 및 향후 과제 (Significance & Future Work)

• 신뢰성 확보: ATP 의 내부 상태 (포화 집합) 를 외부 검증 도구로 검증 가능한 모델로 변환함으로써, ATP 의 출력에 대한 신뢰도를 획기적으로 높였습니다. 이는 수학적 연구나 소프트웨어 검증 분야에서 ATP 를 사용할 때 중요한 '검증 가능성 (verifiability)' 문제를 해결합니다.
• 수학자와의 협업: ATP 의 '블랙박스' 출력을 수학적 직관으로 이해할 수 있는 명시적 모델로 변환하여, 수학적 분류 작업 (ETP 등) 에 ATP 를 더 효과적으로 활용할 수 있게 했습니다.
• 향후 과제:
  • 단위 등식 조각을 넘어 더 풍부한 절 논리 (clausal logic) 로의 확장 (예: 호른 절, 조건부 재작성 규칙).
  • 생성된 수렴 재작성 시스템으로부터 (가능하다면) 명시적인 유한 모델을 추출할 수 있는지 연구.
  • TSTP (Theorem Proving Solution Format) 와 같은 표준 형식을 통해 생성된 모델을 보고하는 방식의 표준화.

결론적으로, 이 논문은 자동화 정리 증명기의 '포화' 상태를 단순한 계산 결과물이 아닌, 검증 가능한 명시적 (무한) 모델로 해석하는 새로운 패러다임을 제시하며, 대규모 수학 프로젝트에서 ATP 의 실용성과 신뢰성을 크게 향상시켰습니다.