Twitch: Learning Abstractions for Equational Theorem Proving

이 논문은 자동 추론에서 인간이 제공하는 지침 없이도 관련 증명에서 반복적으로 나타나는 흥미로운 항 패턴(추상화) 을 자동으로 발견하는 도구 'Twitch'를 제안하고, 이를 등식 정리 증명기 Twee 에 통합하여 TPTP 의 단위 등식 문제 해결 성능과 속도를 크게 향상시켰음을 보여줍니다.

핵심

1. 문제 상황: "너무 많은 재료, 너무 많은 시도"

자동 증명기 (이 논문에서는 Twee라는 프로그램) 는 수학 문제를 풀 때, 마치 거대한 창고에서 재료를 찾아 요리를 하듯 수많은 조합을 시도합니다.

• 상황: 수백만 개의 가능한 조합 (critical pairs) 이 있지만, 그중에서 진짜 맛있는 요리 (증명) 에 필요한 몇 가지만 골라야 합니다.
• 문제: 컴퓨터는 모든 재료를 다 확인하려다 보니 시간이 너무 오래 걸립니다. 보통은 "재료가 얼마나 큰지" 같은 단순한 기준으로만 골라내는데, 이렇게 하면 어려운 요리는 절대 완성할 수 없습니다.

2. 해결책: "Twitch"와 "Stitch"의 등장

이 논문은 **"어떤 재료 조합이 자주 나오는지 알아서, 그걸 '약자 (Abstraction)'로 만들어주자"**는 아이디어를 제시합니다.

• Stitch (바느질 도구): 원래는 프로그래밍 코드에서 반복되는 패턴을 찾아내어 새로운 함수로 만드는 도구입니다. 이 논문에서는 이를 증명 과정에 적용했습니다.
• Twitch (새로운 요리사): Stitch 를 이용해 증명 과정에서 자주 등장하는 복잡한 식 (예: f(x, x)) 을 찾아내고, 이를 g(x)처럼 짧은 이름으로 바꿔주는 역할을 합니다.

비유:
만약 요리 레시피에 "감자를 껍질 벗기고, 껍질 벗긴 감자를 다지고, 다진 감자를 기름에 볶고..."라는 문장이 100 번 반복된다면, 우리는 이를 **"감자 준비"**라는 하나의 단계로 묶을 수 있습니다.
Twitch 는 이 **"감자 준비"**라는 패턴을 자동으로 찾아내서, 컴퓨터가 복잡한 과정을 한 번에 인식하게 해줍니다.

3. Twitch 가 어떻게 배우는가? (두 가지 방법)

Twitch 는 증명을 돕기 위해 두 가지 방식으로 '약자'를 배웁니다.

① 실패한 시도를 분석하기 (Partial Proof Abstractions)

• 상황: 컴퓨터가 어려운 문제를 풀다가 지쳐서 (시간 초과) 포기했을 때, 그 과정에서 무엇을 시도했는지 살펴봅니다.
• 방법: "아, 이 문제는 풀지 못했지만, 중간에 이 복잡한 식이 계속 나왔구나! 이걸 '약자'로 만들어서 다시 시도해보자"라고 생각합니다.
• 비유: 실패한 요리 영상을 보고 "아, 이 재료를 섞는 과정이 자꾸 꼬였네. 이걸 '특제 소스'라고 이름 붙여서 다음에 미리 준비해두자"라고 배우는 것입니다.

② 쉬운 문제에서 배우기 (Domain Abstractions)

• 상황: 같은 분야의 쉬운 문제들 (예: 쉬운 대수학 문제) 을 먼저 풀어봅니다.
• 방법: 쉬운 문제들을 풀 때 자주 등장하는 패턴을 찾아내어, 이를 '약자'로 저장해 둡니다. 그리고 이제 어려운 문제를 풀 때 이 저장된 약자를 참고합니다.
• 비유: "이 분야의 쉬운 요리들에는 항상 '마늘 다지기'가 필요했어. 이제 어려운 요리도 만들 때 '마늘 다지기'를 미리 준비해두면 훨씬 빠르겠지?"라고 생각하는 것입니다. (이를 '커리큘럼 학습'이라고도 합니다.)

4. 결과가 어땠을까요?

연구팀은 이 방법을 실제 수학 문제 (TPTP 라는 문제집) 에 적용해 보았습니다.

• 성공: 이전에 컴퓨터가 풀지 못했던 어려운 문제 12 개를 성공적으로 풀었습니다.
• 속도: 문제를 푸는 속도가 빨라졌습니다. 어떤 문제는 250 초 걸리던 것이 10 초 만에 해결되기도 했습니다.
• 핵심: 단순히 새로운 규칙을 추가하는 것이 아니라, 컴퓨터가 **"어떤 패턴을 중요하게 생각해야 할지"**를 가르쳐주어, 불필요한 시도를 줄여주었습니다.

5. 왜 이것이 중요한가요?

기존에는 수학자가 직접 "이런 패턴이 중요해!"라고 컴퓨터에 알려줘야 했습니다. 하지만 Twitch 는 컴퓨터 스스로 "어떤 패턴이 자주 나오는지"를 찾아내고, 그것을 활용하는 법을 배웁니다.

이는 마치 초보 요리사가 스스로 레시피를 분석해서 '핵심 비법'을 찾아내고, 그 비법을 이용해 더 어려운 요리를 척척 해내는 것과 같습니다.

요약

• 무엇인가? 수학 증명 프로그램을 더 똑똑하게 만드는 도구 Twitch.
• 어떻게? 증명 과정에서 반복되는 복잡한 패턴을 찾아내어 **짧은 약자 (Abstraction)**로 만들어준다.
• 어디서 배워? 실패한 시도나 쉬운 문제들을 분석해서 배운다.
• 결과? 증명 속도가 빨라지고, 이전에 풀지 못했던 어려운 문제도 해결된다.

이 연구는 인공지능이 복잡한 논리 문제를 해결할 때, 인간의 도움 없이 스스로 '핵심 패턴'을 발견하고 학습할 수 있음을 보여주는 중요한 발걸음입니다.

기술 요약

1. 문제 정의 (Problem)

자동화 된 정리 증명기 (Automated Theorem Provers, ATP) 는 방대한 검색 공간 (search space) 을 탐색해야 합니다. 특히 등식 정리 증명 (Equational Theorem Proving) 에서, 증명기는 수백만 개의 '크리티컬 페어 (critical pairs)'를 고려해야 하지만, 최종 증명에 실제로 사용되는 것은 그중 극히 일부에 불과합니다.

• 핵심 난제: 어떤 크리티컬 페어가 유용한지 식별하는 것이 필수적이지만, 현재 Twee 와 같은 증명기의 휴리스틱은 주로 식의 크기 (size) 에만 의존하여 단순합니다.
• 기존 접근법의 한계: Otter 등의 도구에서 인간이 '흥미로운 항 (term) 의 형태'를 수동으로 지정하여 증명을 유도하는 방식 (Weighting, Resonance, Hint 전략) 이 있지만, 이는 인간의 개입이 필요하며 자동화되지 않았습니다.
• 목표: 인간 개입 없이 증명 과정에서 반복적으로 나타나는 흥미로운 항 패턴 (Abstractions) 을 자동으로 발견하고, 이를 활용하여 증명 효율을 높이는 것입니다.

2. 방법론 (Methodology)

이 논문은 Twitch라는 도구를 제안하며, 이는 프로그램 합성 (Program Synthesis) 분야에서 재사용 가능한 라이브러리 함수를 발견하기 위해 개발된 Stitch 도구를 등식 증명에 적용한 것입니다.

A. Abstraction (추상화) 의 정의

증명 내의 반복되는 항 패턴을 새로운 함수 정의 (약어) 로 압축하는 것을 의미합니다.

• 예시: $f(x, x)$와 같은 패턴이 증명에서 반복된다면, 이를 $g(x) := f(x, x)$로 정의하여 압축합니다.
• Stitch 의 역할: 입력된 항들의 집합을 받아, 가장 효율적으로 압축할 수 있는 함수 정의 (최대 압축성) 를 찾아냅니다.

B. Twitch 의 두 가지 작동 모드

Twitch 는 두 가지 방식으로 추상화를 생성합니다.

1. 부분 증명 추상화 (Partial Proof Abstractions):

   • 상황: 증명하려는 문제 ($P_h$) 가 실패하거나 타임아웃되었을 때.
   • 과정:
     1. Twee 로 $P_h$를 일정 시간 실행하여 실패한 증명 시도를 얻음.
     2. 도출된 보조 정리 (lemmas) 중 '흥미로운' 것들을 선별 (점수 $s(l=r) = \frac{\text{증명 내 항의 총 크기}}{\text{정리 자체의 크기}^2}$ 사용).
     3. 선정된 정리의 증명에 포함된 항들을 Stitch 에 입력하여 패턴을 추출.
     4. 추출된 추상화를 사용하여 Twee 를 재실행.

2. 도메인 추상화 (Domain Abstractions):

   • 상황: 특정 도메인 (예: 군론, 격자론) 내에서 이미 해결된 쉬운 문제들이 있을 때.
   • 과정 (커리큘럼 학습 아이디어):
     1. 쉬운 문제들의 증명에서 지역적 (local) 추상화를 Stitch 로 추출.
     2. 각 추상화가 해당 문제의 증명 속도를 높이는지 (Speedup) 검증.
     3. 검증된 좋은 추상화들을 집합으로 모은 후, 다시 Stitch 를 실행하여 공통된 고수준 도메인 추상화를 생성.
     4. 이 도메인 추상화를 어려운 문제 ($P_h$) 에 적용.

C. Twee 에의 통합 (Supporting Abstractions in Twee)

새로운 공리 (axiom) 를 추가하여 검색 공간을 확장하는 대신, 휴리스틱 점수 (Weight) 를 조정하는 방식으로 구현했습니다.

• 방식: 크리티컬 페어 내의 항이 추출된 추상화 패턴과 일치하면, 해당 항의 가중치 (weight) 를 감소시킵니다.
• 효과: 가중치가 낮아진 항은 증명기가 더 자주 선택하게 되며, 이는 검색 공간을 확장하지 않으면서도 유용한 추론을 선호하게 만듭니다.
• 장점: 새로운 공리를 추가할 때 발생하는 불필요한 추론 (search space explosion) 을 방지하면서도, 많은 수의 추상화를 적용할 수 있습니다.

3. 주요 기여 (Key Contributions)

1. 자동 추상화 생성 방법론: 실패한 증명 시도나 관련 문제들의 증명에서 반복되는 패턴을 자동으로 발견하여 추상화를 생성하는 새로운 방법 제시.
2. Stitch 와 Twee 의 통합: 프로그램 합성 도구인 Stitch 를 등식 정리 증명에 적용하고, 이를 Twee 증명기의 휴리스틱에 통합한 Twitch 시스템 구현.
3. 성능 향상 및 난제 해결: TPTP (Theorem Proving Problem) 벤치마크에서 기존 Twee 가 해결하지 못했던 난제 (Rating 1.0) 를 해결하고, 일반적인 문제들의 실행 시간을 획기적으로 단축.
4. 개념적 확장: 단순한 공리 추가가 아닌, 검색 휴리스틱을 수정하는 방식으로 추상화를 활용하는 접근법의 유효성 입증.

4. 실험 결과 (Results)

TPTP v9.2.1 의 Unit Equality (UEQ) 문제 세트를 대상으로 실험을 수행했습니다.

• 난제 해결 (Hard Problems):
  • TPTP Rating 0.9 이상 (90% 의 ATP 가 300 초 내 해결 불가) 이면서 기존 Twee 가 1000 초 내 해결하지 못했던 70 개의 난제 중 18 개를 성공적으로 해결했습니다.
  • 특히 LAT075-1 (Sheffer stroke 관련 격자론 문제) 의 경우, 도메인 추상화를 적용하여 실행 시간을 약 250 초에서 32 초로 단축했습니다.
• 실행 시간 단축 (Runtime Improvements):
  • 도메인 추상화 + 목표 평탄화 (Goal Flattening): 기존 Twee 보다 약 25 개 더 많은 문제를 300 초 내에 해결했으며, 기존에 해결 가능했던 문제들의 실행 시간을 약 2 배 단축했습니다.
  • 부분 증명 추상화: 사전 처리가 필요 없어 유연하지만, 도메인 추상화보다는 효과가 다소 낮았습니다.
• 추상화 vs 정의 공리 (Abstractions vs Axioms):
  • 추출된 패턴을 '정의 공리'로 추가하는 방식보다, **Twee 의 추상화 메커니즘 (가중치 감소)**으로 적용하는 방식이 더 많은 문제를 해결하고 타임아웃을 줄이는 데 효과적이었습니다. (공리 추가는 검색 공간을 과도하게 확장할 위험이 있음)

5. 의의 및 결론 (Significance)

• 자동화된 구조 기반 학습: 인간의 개입 없이 증명 데이터에서 의미 있는 수학적 구조 (예: 논리 연산의 부등식, 분배법칙 패턴 등) 를 자동으로 추출하여 증명 전략을 개선할 수 있음을 보였습니다.
• 해석 가능한 가이드: 통계적 모델 (ENIGMA 등) 과 달리, 추출된 추상화는 명시적인 문법적 패턴 (syntactic abstractions) 이므로 인간이 이해하고 해석하기 쉽습니다. 이는 수학 연구 도구로서의 ATP 의 가치를 높입니다.
• 미래 연구 방향: 단순한 패턴 추출을 넘어, 증명 스케치 (Proof Sketches) 생성이나 더 정교한 도메인 구성, 그리고 LLM 을 활용한 추상화 제안 등으로 발전할 가능성이 큽니다.

요약하자면, Twitch 는 기존 증명기의 단순한 휴리스틱을 보완하기 위해, 증명 과정의 '반복되는 패턴'을 자동으로 학습하여 증명의 방향을 유도하는 새로운 패러다임을 제시한 연구입니다.