Finding Connections via Satisfiability Solving

이 논문은 연결 계산법 (connection calculi) 의 증명 검색 구조를 부호화하고 대칭성 깨기를 적용한 SAT 기반 방법을 제안하여 1 차 논리 증명 자동화를 향상시키고, 이를 위해 세 가지 SAT 부호화를 제시하고 이론적 분석을 수행하며 새로운 솔버 upCoP 를 구현하여 실용성을 입증합니다.

핵심

이 논문은 **"컴퓨터가 복잡한 수학 문제를 풀 때, 어떻게 하면 더 똑똑하고 빠르게 실수를 줄일 수 있을까?"**에 대한 새로운 방법을 제안합니다.

기존의 자동 증명 프로그램들은 주로 두 가지 방식으로 문제를 풀었습니다.

1. 쌓아 올리는 방식 (Saturation): 모든 가능한 사실을 하나씩 만들어내며 쌓아 올리는 방법입니다. (비유: 레고 블록을 하나하나 다 만들어서 가장 큰 성을 짓는 것)
2. 목표를 쪼개는 방식 (Subgoal-reduction): 큰 목표를 작은 목표들로 나누고, 하나씩 해결해 나가는 방법입니다. (비비: 미로에서 길을 찾기 위해 갈림길마다 길을 막고 다시 돌아오는 것)

이 논문은 이 두 가지 방식을 섞어서, 특히 '목표를 쪼개는 방식'에서 발생하는 실수 (불필요한 탐색) 를 막아주는 새로운 기술을 개발했습니다.

---

🧩 핵심 아이디어: "미로 찾기 게임의 마스터 가이드"

이 연구의 주인공은 **SAT 솔버 (Boolean Satisfiability Solver)**라는 아주 똑똑한 '미로 찾기 전문가'입니다. 이 전문가의 특징은 다음과 같습니다.

• 기억력이 좋음: "여기서 좌회전하면 벽에 부딪혔던 적이 있어!"라고 기억해서 다시 그 길로 가지 않습니다.
• 원인 분석: "왜 실패했을까?"를 분석해서 "A 와 B 를 동시에 선택하면 안 돼"라는 규칙을 만들어냅니다.

저자들은 이 전문가를 이용해 **연결 계산 (Connection Calculus)**이라는 논리 증명 방법을 더 효율적으로 만들었습니다.

1. 기존 방식의 문제점: "실수 반복"

기존의 '목표 쪼개기' 방식은 미로를 찾을 때, 이미 실패한 길 (벽) 을 다시 다시 시도하는 경우가 많습니다. 예를 들어, "A 길로 가다가 실패했어"라고 했을 때, 다음에는 "A 길 대신 B 길로 가자"라고 해야 하는데, 컴퓨터는 "아니야, A 길의 2 번 버전으로 가자"라고 또다시 시도하며 시간을 낭비합니다.

2. 이 논문의 해결책: "증명 과정을 퍼즐로 만들기"

저자들은 증명 과정을 퍼즐 맞추기로 바꿨습니다.

• 퍼즐 조각: 논리 문장들 (클auses)
• 목표: 모든 조각을 연결해서 빈틈없는 그림 (증명) 을 완성하는 것.

이때 SAT 솔버를 퍼즐의 지휘자로 세웠습니다. 지휘자는 "이 조각을 여기에 붙이면 나중에 막히니까 붙이지 마!"라고 미리 경고하거나, "이 두 조각은 꼭 연결되어야 해!"라고 명령합니다.

---

🛠️ 세 가지 새로운 전략 (방법론)

이 논문은 증명 과정을 SAT 솔버가 이해할 수 있도록 세 가지 다른 방식으로 번역 (인코딩) 했습니다.

1. 첫 번째 시도: "나무 구조의 증명" (Connection Tableaux)

• 비유: 가지를 치면서 올라가는 나무를 그리는 것.
• 문제점: 나무가 너무 커지면, 가지 하나하나를 다 기억해야 해서 컴퓨터가 멍해집니다. (너무 많은 변수가 생김)

2. 두 번째 시도: "격자 구조의 증명" (Matrix Proofs)

• 비유: 나무가 아니라, 레고 블록을 평평하게 쌓아 올리는 것.
• 장점: 가지치기 (나무) 보다는 블록 쌓기 (격자) 가 SAT 솔버가 "어떤 블록을 쓸지" 결정하기 훨씬 쉽습니다. 불필요한 가지를 치는 대신, 필요한 블록들만 딱 맞게 고릅니다.

3. 세 번째 시도: "실패 기록을 활용한 학습" (Unsat Core Refinement)

• 비유: 미로에서 실패했을 때, "왜 실패했는지"를 분석해서 다음에 그 실수를 하지 않도록 지도를 수정하는 것.
• 작동 원리:
  1. 처음에는 블록을 아주 적게 준비합니다.
  2. SAT 솔버가 "증명 못 해!"라고 하면, "어떤 블록이 부족했는지" (Unsat Core) 를 알려줍니다.
  3. 그 부족했던 블록을 더 추가하고 다시 시도합니다.
  4. 이 과정을 반복하면, 결국 필요한 블록만 딱 맞게 모여 증명에 성공합니다.

---

🏆 실제 성과: "UPCoP"라는 새로운 로봇

저자들은 이 방법을 **'UPCoP'**라는 새로운 증명 프로그램으로 구현했습니다.

• 테스트: 수천 개의 논리 문제 (TPTP 데이터베이스) 를 풀게 했습니다.
• 결과: 기존에 유명한 프로그램 (meanCoP) 이 풀지 못했던 179 개의 문제를 UPCoP 가 성공적으로 풀었습니다.
• 이유: UPCoP 는 불필요한 시도를 미리 차단하고, 필요한 부분에만 집중하기 때문에 더 효율적이었습니다.

---

💡 요약: 왜 이것이 중요한가요?

이 논문은 **"컴퓨터가 논리 문제를 풀 때, 단순히 무작위로 시도하는 대신, 실패 경험을 학습해서 똑똑하게 길을 찾게 한다"**는 아이디어를 증명했습니다.

• 기존: "일단 다 해보자! (그리고 실수하면 다시 해보자)"
• 이 논문: "이건 안 돼, 저건 필요해. 실패한 이유는 이거였어. 자, 이제 필요한 것만 모아서 다시 해보자."

이는 인공지능이 복잡한 추론을 할 때, 불필요한 계산 시간을 줄이고 더 정확한 결론을 내는 데 큰 도움이 될 것입니다. 마치 미로 찾기 게임에서 실수한 길을 표시해두고, 가장 빠른 길만 찾아주는 GPS 가 생긴 것과 같습니다.

기술 요약

1. 문제 정의 (Problem)

자동 증명기 (Automated Theorem Provers) 는 주로 두 가지 전략 중 하나를 사용합니다:

1. 순서 기반 포화 (Ordering-based Saturation): Vampire, E, Spass 등. 기존 공리 집합에서 새로운 사실을 계속 추론하여 검색 공간을 확장합니다.
2. 부분 증명 기반 하위 목표 축소 (Subgoal-reduction): Setheo, leanCoP 등. 부분 증명을 조작하고 필요시 백트래킹 (Backtracking) 을 수행합니다.

기존 방법의 한계:

• 하위 목표 축소 방식의 비효율성: 검색 공간 내의 중복되거나 쓸모없는 공리 (redundant formulas) 를 반복적으로 탐색할 수 있습니다. 이를 방지하기 위해 "어디까지 탐색했는지"를 기억하는 전역적 정제 (Global Refinement) 가 필요하지만, 이는 비선형적인 명제 논리 구조를 포함하여 기존 방법론으로 처리하기 어렵습니다.
• SAT 솔버 활용의 부재: 기존 SAT 솔버는 주로 1 차 논리를 명제 논리로 축소 (Grounding) 하여 불만족성을 증명하는 데 사용되었습니다. 즉, 증명 과정 자체의 구조를 SAT 문제의 모델로 직접 인코딩하는 시도는 드뭅니다.

이 논문은 이러한 한계를 극복하고, **대칭성 깨기 (Symmetry Breaking)**와 결합된 SAT 기반 방법을 통해 연결 계산법의 자동화를 한 단계 더 발전시키는 것을 목표로 합니다.

2. 방법론 (Methodology)

저자들은 연결 증명 (Connection Proofs) 의 존재를 SAT 문제로 인코딩하는 세 가지 다른 방식을 제시했습니다.

A. 연결 테이블루 인코딩 (Encoding Connection Tableaux, $E_T$)

• 개념: 연결 테이블루의 구조를 직접 SAT 변수로 매핑합니다. 리터럴이 테이블루의 잎 (leaf) 이 되는지, 확장 (Extension) 또는 축소 (Reduction) 규칙이 적용되는지를 변수로 표현합니다.
• 문제점: 확장 규칙을 적용할 때마다 새로운 클로즈 (Clause) 인스턴스가 생성되어 SAT 변수의 수가 급격히 증가합니다. 이로 인해 솔버가 활용할 수 있는 명제 논리 구조가 약화되고, leanCoP 와 같은 기존 시스템이 효율적으로 수행하던 탐색을 SAT 솔버의 오버헤드와 함께 반복하는 '파괴적인 (Pathological)' 행동을 보입니다.

B. 행렬 증명 인코딩 (Encoding Matrix Proofs, $E_M$)

• 개념: 테이블루의 계층적 구조 대신, 행렬 (Matrix) 형태의 표현을 사용합니다. 행렬은 입력 클로즈의 집합이며, 모든 리터럴이 다른 클로즈의 리터럴과 연결되어 있어야 합니다 (Fully Connected).
• 장점: 테이블루와 달리 트리가 아닌 행렬 구조를 사용하므로, 하나의 행렬 증명이 여러 테이블루 증문에 대응될 수 있습니다. 이는 SAT 솔버가 처리하기에 더 적합한 조합적 문제 (Combinatorial Problem) 로 변환됩니다.
• 작동 원리:
  1. 선택자 (Selectors): 각 클로즈가 행렬에 포함되는지 여부를 결정하는 변수를 도입합니다.
  2. 전체 연결성 제약: 선택된 모든 리터럴이 다른 클로즈의 리터럴과 연결되도록 강제합니다.
  3. 스패닝 연결 (Spanning Connections): 열린 경로 (Open Path) 가 없도록 하여 증명이 완성되었음을 확인합니다.

C. Unsat Core 를 통한 반복 심화 (Iterative Deepening via Unsat Core, $E_U$)

• 문제: $E_M$ 방식은 행렬의 크기 (클로즈 수) 를 미리 정해야 하므로, 불필요한 클로즈 복사본을 과도하게 생성할 수 있습니다.
• 해결책: Abstraction-Refinement 접근법을 사용합니다.
  • 각 클로즈의 필요 개수 (Multiplicity, $\mu$) 를 초기화하고, SAT 솔버가 Unsat Core(불일치를 유발하는 가정들의 부분집합) 를 반환하면, 해당 클로즈의 복사본 수를 증가시킵니다.
  • 이를 통해 필요한 경우에만 클로즈 인스턴스를 동적으로 생성하여 검색 공간을 최적화합니다.

D. 중복 제거 및 대칭성 깨기 (Redundancy Elimination)

• 다중성 대칭성 (Multiplicity Symmetry): 동일한 클로즈의 복사본 순서를 고정하여 ($C_i$가 선택되려면 $C_{i-1}$도 선택되어야 함) 불필요한 탐색을 줄입니다.
• 인스턴스 대칭성 (Instance Symmetry): 클로즈 간의 포함 관계 (Subsumption) 를 고려하여 더 구체적인 클로즈만 선택되도록 제한합니다.
• 치환 대칭성 (Substitution Symmetry): 동일한 클로즈 복사본에 적용된 치환 (Substitution) 에 순서를 부여하여 대칭적인 해를 제거합니다.

3. 주요 기여 (Key Contributions)

1. SAT 기반 연결 계산법 인코딩: 연결 테이블루, 행렬 표현, Unsat Core 기반 반복 심화를 통해 1 차 논리 연결 증명을 명제 논리 문제로 성공적으로 인코딩했습니다.
2. 이론적 검증: 제안된 인코딩들의 건전성 (Soundness), 완전성 (Completeness), **종결성 (Termination)**을 수학적으로 증명했습니다. 특히 행렬 인코딩의 복잡도 클래스가 $\Sigma^P_2$임을 보였습니다.
3. 최적화 기법: 대칭성 깨기와 중복 제거 기법을 도입하여 SAT 솔버의 검색 공간을 효율적으로 축소했습니다.
4. 새로운 솔버 UPCoP 구현: CaDiCaL(SAT) 과 Z3(SMT) 솔버를 백엔드로 사용하는 프로토타입 솔버 UPCoP를 구현하고 TPTP 벤치마크를 통해 평가했습니다.

4. 실험 결과 (Results)

• 평가 환경: TPTP 8.2.0 저장소의 6,468 개의 증명 가능한 1 차 논리 문제를 사용했습니다. (타임아웃 30 초, 메모리 16GB)
• 성능 비교:
  • 기존 최첨단 연결 솔버인 meanCoP와 비교했습니다.
  • UPCoP 는 meanCoP 보다 전체적으로 더 적은 문제를 해결했지만, meanCoP 가 해결하지 못한 179 개의 문제를 성공적으로 해결했습니다.
  • 특히, meanCoP 가 생성하는 테이블루 형태의 증명보다 UPCoP 가 찾은 행렬 형태의 증명이 더 작거나 효율적인 경우가 많았습니다.
• 인코딩별 특징:
  • $E_M$: 작고 비-트리 형태의 증명에 빠릅니다.
  • $E_U$: 중복된 연결 불가능한 클로즈가 많은 대규모 문제에 적합합니다.
  • $E_H$(Hybrid): 입력 클로즈의 대부분을 소량씩 사용하는 증명에 효과적입니다.

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

• 증명 구조의 직접적 인코딩: 기존에 1 차 논리를 명제 논리로 축소 (Grounding) 하던 방식과 달리, 증명 탐색 과정 자체를 SAT 모델로 표현하여 전역 정보 (Global Information) 를 효과적으로 관리하고 정제할 수 있음을 보였습니다.
• 새로운 가능성 제시: SAT/SMT 솔버의 강력한 학습 (Learning) 과 설명 (Explanation, Unsat Core) 기능을 1 차 논리 증명의 전역적 정제에 활용함으로써, 기존 자동 증명기가 접근하지 못했던 문제들을 해결할 수 있는 가능성을 열었습니다.
• 향후 과제: SAT 솔버의 내부 휴리스틱이 1 차 논리 증명 탐색에 항상 최적은 아니므로, UPCoP 의 성능 향상을 위해 커스텀된 충돌 학습 (Conflict Learning) 및 변수 선택 전략의 개발이 필요함을 지적했습니다. (이는 후속 연구인 hopCoP 로 이어짐)

이 논문은 자동 증명 분야에서 SAT/SMT 기술과 연결 계산법을 융합한 새로운 패러다임을 제시하며, 특히 복잡한 논리 구조를 가진 문제들에 대한 자동 증명 능력을 확장하는 데 중요한 기여를 했습니다.