6.17 자동 정리 증명(Automated Theorem Proving)의 범위와 제약

1. 자동 정리 증명의 정의와 역사적 기원

자동 정리 증명(Automated Theorem Proving, ATP)은 주어진 형식 체계 내에서 목표 명제의 증명을 기계적 알고리즘에 의해 자동으로 탐색하고 구성하는 분야이다. ATP의 이론적 기원은 라이프니츠의 보편적 연산(calculus ratiocinator) 구상과 힐베르트의 형식주의 프로그램(formalist program)에 있으며, 이 프로그램은 수학적 추론의 완전한 기계화를 목표로 하였다.

최초의 실질적 ATP 시스템은 Newell, Shaw, Simon이 1956년에 개발한 Logic Theorist이다. 이 프로그램은 화이트헤드(Whitehead)와 러셀(Russell)의 Principia Mathematica에 수록된 정리 중 38개를 자동으로 증명하였다. 이후 1967년 Robinson이 제안한 분해 원리(resolution principle)는 1차 술어 논리(first-order predicate logic)에 대한 반증 완전(refutation-complete) 절차를 제공하였으며, 이는 현대 ATP 시스템의 핵심 기반이 되었다.

2. 차 술어 논리에서의 결정 가능성과 반결정 가능성

ATP의 이론적 범위를 규정하는 핵심 결과는 처치(Church, 1936)와 튜링(Turing, 1936)의 결정 불가능성 정리이다. 1차 술어 논리의 유효성 판정 문제(validity problem)—임의의 1차 논리 공식이 논리적으로 유효한지 판정하는 문제—는 결정 불가능(undecidable)하다. 즉, 임의의 1차 논리 공식을 입력으로 받아 유한 시간 내에 유효 여부를 판정하는 알고리즘은 존재하지 않는다.

그러나 1차 술어 논리는 반결정 가능(semi-decidable)하다. 괴델의 완전성 정리(completeness theorem, 1930)에 의해, 1차 술어 논리에서 논리적으로 유효한 모든 공식은 증명 가능하다. 따라서 유효한 공식에 대해서는 체계적 탐색을 통해 유한 시간 내에 증명을 찾을 수 있다. 반면, 유효하지 않은 공식에 대해서는 탐색이 영원히 종료되지 않을 수 있다.

이 비대칭성이 ATP의 근본적 한계를 규정한다. ATP 시스템은 정리(유효한 공식)에 대해서는 원리적으로 증명을 찾을 수 있으나, 비정리에 대해서는 “증명 불가능“이라는 판정을 유한 시간 내에 내릴 수 없는 경우가 존재한다.

3. 현대 ATP 시스템의 주요 방법론

현대 ATP 시스템은 여러 핵심 기법을 결합하여 증명 탐색의 효율성을 극대화한다.

**분해 기반 방법(Resolution-based methods)**은 증명하고자 하는 명제의 부정을 절(clause) 형태로 변환한 후, 분해 규칙을 반복 적용하여 공절(empty clause, \square)을 도출함으로써 원래 명제를 반증법적으로 증명한다. E 증명기(Schulz, 2002)와 Vampire(Riazanov and Voronkov, 2002)는 이 접근의 대표적 구현체이다.

**등식 추론(Equational reasoning)**은 크누스-벤딕스 완료(Knuth-Bendix completion) 절차와 재작성 규칙(rewriting rules)을 활용하여 등식 이론에서의 증명을 수행한다. 초분해(superposition) 미적분은 등식 추론과 분해를 통합한 현대적 프레임워크이다.

**타블로 방법(Tableau method)**은 목표 공식의 의미론적 분석을 기반으로 체계적 반례 탐색을 수행한다. 공식을 분해하여 모든 가능한 모델을 열거하고, 모든 분기(branch)가 모순으로 닫히면 원래 공식의 유효성이 확인된다.

**SMT 풀기(Satisfiability Modulo Theories)**는 명제 논리의 만족 가능성 판정(SAT solving)을 배경 이론—정수 산술, 실수 산술, 배열 이론, 비트벡터 이론 등—으로 확장한다. Z3(de Moura and Bjørner, 2008)는 가장 널리 사용되는 SMT 풀기이며, 소프트웨어 검증과 프로그램 분석에서 핵심적 도구로 활용된다.

4. 불완전성 정리에 의한 ATP의 원리적 한계

괴델의 제1 불완전성 정리는 ATP의 원리적 한계를 직접적으로 설정한다. 페아노 산술(Peano arithmetic, PA)을 포함하는 형식 체계 \mathcal{F}에서 작동하는 ATP 시스템을 생각하자. 불완전성 정리에 의해 \mathcal{F}에는 \mathcal{F} 내에서 증명도 반증도 불가능한 명제 G가 존재한다. ATP 시스템이 G의 증명을 탐색하면, 이 탐색은 영원히 종료되지 않는다. 또한 \neg G의 증명 탐색도 동일하게 종료되지 않는다.

이 한계는 ATP 시스템의 구현상 결함이 아니라, 수학적 추론 자체의 근본적 제약이다. 어떤 알고리즘적 개선이나 하드웨어 향상으로도 극복할 수 없으며, 이는 ATP의 원리적 완전성(completeness)이 달성 불가능함을 의미한다. 구체적으로, PA에서의 괴델 문장 G_{\text{PA}}, 페리스-해링턴 정리(Paris-Harrington theorem), 굿스타인 정리(Goodstein’s theorem) 등은 PA에서 증명 불가능하지만 참인 명제의 실례이다.

제2 불완전성 정리는 추가적 제약을 부과한다. \mathcal{F}가 자신의 무모순성 \text{Con}(\mathcal{F})를 증명할 수 없으므로, ATP 시스템은 자신이 작동하는 형식 체계의 건전성(soundness)을 해당 체계 내에서 검증할 수 없다. 이는 ATP 시스템의 자기 검증(self-verification) 능력에 본질적 한계가 있음을 의미한다.

5. 계산 복잡도에 의한 실천적 제약

불완전성 정리가 설정하는 원리적 한계 외에, ATP는 계산 복잡도에 의한 실천적 제약에도 직면한다.

명제 논리의 만족 가능성 문제(SAT)는 NP-완전(NP-complete)이다. 현대 SAT 풀기는 충돌 주도 절 학습(conflict-driven clause learning, CDCL) 등의 기법을 통해 실용적 규모의 문제를 처리하나, 최악의 경우(worst case) 시간 복잡도는 입력 크기에 대해 지수적이다.

1차 술어 논리의 증명 탐색은 더 심각한 복잡도 문제를 야기한다. 탐색 공간은 양화사(quantifier)에 의한 항(term)의 인스턴스화로 인해 폭발적으로 증가하며, 적절한 인스턴스화 선택은 증명 탐색의 효율에 결정적 영향을 미친다. 고차 논리(higher-order logic)에서의 ATP는 더욱 복잡하며, 유니피케이션(unification) 자체가 결정 불가능해진다.

이러한 복잡도 제약으로 인해, 현재의 ATP 시스템은 수학적으로 비자명(nontrivial)한 정리의 자동 증명에서 인간 수학자의 능력에 크게 미치지 못한다. TPTP(Thousands of Problems for Theorem Provers) 라이브러리의 문제 중 상당수는 현재의 ATP 시스템으로 풀리지 않으며, 그 비율은 난이도가 높아질수록 급격히 증가한다.

6. 대화형 정리 증명과 ATP의 상보적 관계

대화형 정리 증명기(interactive theorem prover, ITP)—Coq(Bertot and Castéran, 2004), Isabelle/HOL(Nipkow et al., 2002), Lean(de Moura et al., 2015)—는 ATP의 한계를 보완하는 접근이다. ITP에서 인간 사용자는 증명의 전략적 방향을 지시하고, 시스템은 각 단계의 형식적 정확성을 검증한다. ATP가 자동으로 처리할 수 있는 보조 목표(subgoal)는 자동화되고, 인간의 직관이 필요한 핵심 전략적 판단은 사용자에게 위임된다.

이 상보적 구조에서 ATP는 전술(tactic)의 형태로 ITP에 통합된다. 예를 들어, Isabelle의 sledgehammer 전술은 외부 ATP 시스템(E, Vampire, Z3 등)을 호출하여 현재 목표의 자동 증명을 시도한다. Gonthier 등(2013)의 4색 정리(four color theorem) 형식적 증명과 Hales 등(2017)의 케플러 추측(Kepler conjecture) 형식적 증명(“A Formal Proof of the Kepler Conjecture”)은 ITP와 ATP의 결합이 대규모 수학적 증명의 기계적 검증을 가능하게 함을 보여 주는 실례이다.

7. 결정 가능한 부분 이론에서의 ATP

불완전성 정리의 제약에도 불구하고, 특정 제한된 이론에서는 완전한 결정 절차가 존재한다.

프레스버거 산술(Presburger arithmetic)—곱셈 없는 자연수의 덧셈 이론—은 결정 가능하다. 타르스키(Tarski, 1951)는 실폐쇄체(real closed field)의 1차 이론이 결정 가능함을 증명하였으며, 이 결과에 기반한 원통 대수적 분해(cylindrical algebraic decomposition, CAD) 알고리즘은 실수 부등식 체계의 만족 가능성을 결정한다. 이 영역에서 ATP는 원리적으로 완전하다.

그러나 이 결정 가능한 이론들은 표현력에서 제한적이다. 불완전성 정리의 전제 조건—특히 곱셈을 포함하는 산술의 부호화 능력—을 충족하지 않기 때문에 불완전성 정리가 적용되지 않는 것이다. 표현력과 결정 가능성 사이의 이 교환 관계(trade-off)는 형식 체계 설계의 근본적 긴장을 반영한다.

8. 기계 학습과 ATP의 융합

최근 ATP 연구에서는 기계 학습 기법을 활용하여 증명 탐색의 효율을 향상시키려는 시도가 활발하다. 기계 학습은 증명 탐색의 방향을 안내하는 휴리스틱(heuristic)을 학습하는 데 활용되며, 이는 탐색 공간의 조합적 폭발을 완화하는 데 기여한다.

Bansal 등(2019)의 연구(“HOList: An Environment for Machine Learning of Higher-Order Logic Theorem Proving”)는 고차 논리 정리 증명에서 전제 선택(premise selection)과 전술 선택(tactic selection)에 신경망을 적용하였다. Polu와 Sutskever(2020)의 연구(“Generative Language Modeling for Automated Theorem Proving”)는 GPT 기반 언어 모델을 Metamath 형식 체계의 증명 생성에 적용하여, 이전에 자동으로 증명되지 않던 정리의 증명을 발견하였다.

그러나 기계 학습의 도입은 불완전성 정리에 의한 원리적 한계를 변경하지 않는다. 기계 학습은 증명 탐색의 효율을 향상시킬 수 있으나, 형식 체계 내에서 증명 불가능한 명제에 대해서는 어떠한 탐색 전략도 증명을 찾을 수 없다. 기계 학습이 제공하는 것은 탐색 공간 내의 유망한 방향에 대한 확률적 추정이며, 이는 탐색의 실천적 효율을 개선하나 원리적 한계를 넘어서지 못한다.

9. ATP의 범위와 제약에 대한 종합적 평가

ATP의 범위와 제약은 다음과 같이 요약된다. ATP는 형식 체계 내에서 증명 가능한 정리에 대해 원리적으로 증명을 찾을 수 있다(반결정 가능성). 그러나 불완전성 정리에 의해 모든 참인 명제를 증명할 수는 없으며(불완전성), 계산 복잡도에 의해 증명 가능한 정리에 대해서도 실용적 시간 내에 증명을 찾지 못하는 경우가 빈번하다(실천적 제약).

이 삼중의 제약 구조—반결정 가능성에 의한 종료 불보장, 불완전성에 의한 원리적 한계, 계산 복잡도에 의한 실천적 한계—는 ATP가 수학적 추론의 완전한 자동화에 원리적으로 도달할 수 없음을 확립한다. ATP는 수학적 추론의 강력한 보조 도구이지, 인간 수학자를 완전히 대체하는 체계가 아니다. 이 인식은 인공지능의 형식적 추론 능력에 대한 현실적 기대를 설정하는 데 필수적이다.