💻 computer science

Implementing Dependent Type Theory Inhabitation and Unification

이 논문은 185 줄의 Lean 코드로 구현된 종속 타입 이론의 inhabitation 과 unification 문제를 해결하는 새로운 솔버 'Canonical-min'과 성능 최적화를 위한 모나딕 프레임워크, 그리고 DTTBench 벤치마크를 제시합니다.

원저자: Chase Norman, Jeremy Avigad

게시일 2026-03-03

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Chase Norman, Jeremy Avigad

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

1. 배경: 왜 이 일이 어려운가요? (레고와 미로)

현대 수학 증명 프로그램 (Lean 같은 것들) 은 **'의존형 타입 이론 (DTT)'**이라는 복잡한 언어를 사용합니다. 이 언어는 단순히 "이게 맞다"를 확인하는 것을 넘어, **"이런 모양의 레고 조각을 만들어서 이 빈 공간에 딱 맞게 끼워 넣는 것"**을 요구합니다.

문제 1 (인구 문제/Inhabitation): "이 빈 공간 (타입) 에 들어갈 수 있는 레고 조각 (증명) 을 찾아줘."
문제 2 (일치 문제/Unification): "이 두 조각이 정말 같은 모양인지, 혹은 어떻게 변형하면 같아지는지 찾아줘."

기존의 프로그램들은 이 미로를 찾을 때, "가장 유력해 보이는 길만 따라가다가 막히면 포기하는" 방식을 썼습니다. (불완전한 알고리즘) 그래서 진짜 정답이 있는데도 못 찾거나, 엉뚱한 길로 빠지는 경우가 많았습니다.

2. 해결책: Canonical-min (완벽한 미로 탐험가)

저자들은 **"185 줄의 코드"**라는 아주 작은 도구로, 모든 가능한 길을 체계적으로 탐색하는 완벽한 탐험가를 만들었습니다.

핵심 아이디어 1: "미완성된 레고"를 임시로 남겨두기

일반적인 프로그램은 레고 조각을 다 조립해야만 "이게 맞나?"를 확인합니다. 하지만 이 프로그램은 아직 빈칸이 있는 레고를 보고도 멈추지 않습니다.

비유: 요리사가 "소스 맛이 어때?"라고 물을 때, "아직 소스를 안 넣었어!"라고 대답하는 대신, **"소스를 넣으면 이 맛날 거야"**라는 **약속 (제약 조건)**을 적어두고 다음 단계로 넘어갑니다.
이 '약속'들을 모아서 나중에 빈칸이 채워지면 다시 확인합니다.

핵심 아이디어 2: "마법 같은 메모장" (Monad 프레임워크)

이 프로그램은 코드를 두 번 쓸 필요가 없습니다.

확인 모드: "이 레고 조각이 맞는지 확인해."
찾기 모드: "이 빈 공간에 들어갈 레고 조각을 찾아줘."

이 두 가지 기능을 하나의 **'마법 같은 메모장 (Monad)'**으로 묶었습니다.

비유: 같은 요리사가, "요리법대로 따라 해 (확인)"라고 하면 따라 하고, "이 재료로 맛있는 요리 만들어 (찾기)"라고 하면 재료를 뒤적이며 찾아냅니다. 코드는 하나지만, 상황에 따라 역할이 바뀝니다.

핵심 아이디어 3: "에너지 (Entropy) 를 아껴 쓰는 미로 찾기"

미로에서 모든 길을 다 찾아보려면 시간이 무한히 걸립니다. 그래서 저자들은 **'에너지'**라는 개념을 도입했습니다.

처음에는 에너지가 적어서 짧은 길만 봅니다.
못 찾으면 에너지를 조금 더 불려서 더 긴 길을 봅니다.
비유: 미로에서 1 분만 걸어가다가 막히면 돌아옵니다. 2 분, 3 분... 이렇게 점점 더 멀리 가보며 정답을 찾습니다. 이 방식 (점층적 심도 우선 탐색) 을 통해 정답이 있다면 반드시 찾지만, 없으면 빨리 포기할 수 있습니다.

3. 실제 성과: 왜 이것이 대단한가요?

저자들은 이 프로그램으로 DTTBench라는 새로운 시험지를 만들었습니다.

시험 내용: Lean 이라는 유명한 수학 프로그램의 표준 라이브러리에서 뽑은 31 개의 어려운 문제들 (등식, 부등식, 논리, 집합 등).
결과:
- Canonical-min: 31 문제 중 **31 개를 모두 해결 (완벽한 점수)**했습니다.
- 다른 프로그램들 (Twelf, sauto 등): 31 개 중 2~8 개만 해결했습니다. 나머지는 "찾을 수 없다"고 포기하거나, 틀린 답을 내놓았습니다.

예시:

"A=B 이고 B=C 면 A=C 가 성립한다"는 아주 기본적인 수학 원리부터,
"함수가 모든 값을 다 커버할 수 없다"는 칸토어의 대각선 논법 같은 복잡한 증명까지,
이 프로그램은 스스로 정답을 찾아서 레고를 조립해 냈습니다.

4. 결론: 간단한 코드가 만든 혁신

이 논문의 핵심 메시지는 다음과 같습니다.

"복잡한 수학 증명을 자동으로 해결하는 완벽한 도구를 만들려면, 거대한 코드가 필요하지 않다. 오히려 데이터 구조를 똑똑하게 설계하고 (레고 조각을 잘게 쪼개어 관리), 흐름을 잘 조절하면 (에너지 관리), 아주 짧은 코드로도 '완벽한 해결사'를 만들 수 있다."

이 프로그램은 아직 상용화될 만큼 빠르지는 않지만, **"어떻게 하면 완벽하게 증명할 수 있을까?"**에 대한 이론적인 답을 보여주었고, 앞으로 더 발전된 증명 도구들을 만드는 **청사진 (Reference)**이 될 것입니다.

한 줄 요약:
"이 논문은 복잡한 수학 증명 문제를 해결하기 위해, 미완성된 조각을 임시로 남겨두고 나중에 맞추는 방식과 에너지 효율적으로 미로를 찾는 전략을 결합하여, 185 줄의 짧은 코드로 완벽하게 작동하는 증명 로봇을 만들었습니다."

1. 문제 정의 (Problem)

배경: 현대의 대화형 증명 보조 도구 (Interactive Theorem Provers) 들은 의존 타입 이론을 기반으로 합니다. DTT 는 프로그램 합성과 증명 생성에 강력한 표현력을 가지지만, 자동화하기 매우 어렵습니다.
핵심 문제:
- 포함성 (Inhabitation): 주어진 타입을 갖는 식 (expression) 을 찾는 문제입니다. 이는 정리 증명 및 프로그램 합성에 해당하며, DTT 에서는 **결정 불가능 (undecidable)**합니다.
- 통일 (Unification): 항 (term) 의 방정식을 푸는 문제 역시 DTT 에서 결정 불가능합니다.
기존 한계: 기존 DTT 포함성 솔버들은 대부분 불완전 (incomplete) 합니다. 그들은 1 차 패턴 통일 (first-order pattern unification) 을 사용하며, 이는 DTT 의 복잡한 의존성을 완전히 처리하지 못합니다. (Canonical [17] 은 완전한 알고리즘을 개념적으로 구현했으나, 그 구현은 복잡하고 방대합니다.)

2. 방법론 (Methodology)

저자들은 Canonical-min이라는 단순화된 솔버를 개발했습니다. 이는 185 줄의 Lean 코드로 구현되었으며, 다음과 같은 핵심 기술적 접근법을 사용합니다.

A. 데이터 구조 및 표현 (Data Structures)

항 (Terms) 의 분해: 람다 식을 바인딩 (bindings), 헤드 (head), 그리고 스파인 (spine, 인자들의 시퀀스) 으로 분해하여 표현합니다. 이는 표준 인덕티브 정의보다 단일 생성자 (constructor) 를 사용하여 균일성을 높입니다.
de Bruijn 인덱스: 변수 이름을 사용하지 않고 인덱스를 사용하여 $\alpha$ -동치 (alpha-equivalence) 를 처리합니다.
명시적 치환 (Explicit Substitution, ES): 헤드를 해결하고 $\beta$ -축소를 수행하기 위해 블록 단위로 연결된 리스트 형태의 ES 를 사용합니다. 이는 불변 (immutable) 한 메타변수 (metavariable) 와 가변적인 인덱스를 분리하여 효율적인 접근을 가능하게 합니다.
메타변수 (Metavariables): 미해결된 변수를 나타내며, 할당되지 않은 상태에서는 제약 조건 (constraint) 으로 남습니다.

B. 모나딕 프레임워크 (Monadic Framework)

타입 체커를 솔버로 변환: 기존 타입 체커 코드를 수정하지 않고, 모나드 (Monad) 를 적절히 선택하여 솔버로 변환합니다.
제약 조건 (Constraints): 할당되지 않은 메타변수가 발견되면, 타입 체킹을 중단하고 해당 메타변수에 대한 제약 조건을 생성하여 상태에 저장합니다.
계속 (Continuation) 모나드: SearchM 모나드를 사용하여 계산이 일시 중단 (pause) 되었다가 나중에 재개될 수 있도록 합니다. 이는 백트래킹 (backtracking) 검색을 가능하게 합니다.
제약 조건 구조: Constraint 는 멈춘 메타변수 (stuck) 와 그 변수가 해결되었을 때 실행될 지속 함수 (continuation) 를 포함합니다.

C. 검색 알고리즘 (Search)

반복 심화 깊이 우선 검색 (IDDFS): 트리 높이가 아닌 **엔트로피 (entropy)**라는 사용자 정의 파라미터를 사용하여 검색 깊이를 제어합니다.
메타변수 선택 (Metavariable Selection): 다음에 해결할 메타변수를 선택하는 휴리스틱을 사용합니다.
- Rigid Equation: 메타변수가 비메타변수 (rigid term) 와의 방정식을 가지고 있다면 이를 우선시합니다.
- Rightmost: 의존성이 없는 경우 가장 오른쪽의 메타변수를 선택하여 강력한 통일 제약을 생성합니다.
도메인 (Domain) 탐색: 각 메타변수에 대해 유효한 헤드의 할당 (assignment) 을 생성하고, 이를 적용하여 새로운 제약 조건을 평가합니다.

3. 주요 기여 (Key Contributions)

Canonical-min 구현: 185 줄의 Lean 코드로 DTT 의 포함성 및 통일 문제를 해결하는 **완전 (complete) 하고 건전 (sound)**한 솔버를 구현했습니다.
새로운 구현 기법: 기존 타입 체커와 검색 로직을 분리하면서도 모나드를 통해 자연스럽게 통합하는 아키텍처를 제시했습니다. 이는 타입 체커를 솔버로 변환하는 새로운 패러다임을 보여줍니다.
DTTBench 벤치마크: Lean 표준 라이브러리와 Mathlib 에서 추출한 31 개의 DTT 포함성 문제 (동치, 부등식, 논리, 관계, 집합 등) 로 구성된 새로운 벤치마크를 공개했습니다.
성능 및 완전성 입증: 기존 시스템 (Twelf, sauto, mimer) 보다 훨씬 우수한 성능을 보이며, 특히 다른 시스템이 해결하지 못하는 복잡한 의존 타입 문제를 성공적으로 해결했습니다.

4. 결과 (Results)

벤치마크 성능: DTTBench 의 31 개 문제 중 **Canonical-min 은 31 개를 모두 해결 (31/31)**했습니다.
- 비교 대상인 Twelf 는 8 개, sauto 는 6 개, mimer 는 2 개만 해결했습니다.
- 특히 Relation 카테고리 (13 개 문제) 에서 Canonical-min 은 13/13 을 달성한 반면, 다른 시스템은 0/13 을 기록했습니다.
구체적 사례:
- 등식의 전이성 (Transitivity of equality) 증명.
- 자연수 부등식에 대한 귀납적 추론.
- 관계의 전이적 폐포 (transitive closure) 에 대한 증명.
- 칸토어의 대각선 논법 (Cantor's diagonalization argument) 을 통한 비서열성 증명.
이러한 문제들은 모두 다른 시스템으로는 해결되지 않았으며, Canonical-min 만이 완전한 탐색을 통해 증명했습니다.

5. 의의 및 결론 (Significance)

간결함과 효율성: 복잡한 DTT 솔버가 수천 줄이 아닌 185 줄의 코드로 구현 가능함을 보여주었습니다. 이는 알고리즘의 본질을 이해하고 분석하는 데 훌륭한 참조 모델이 됩니다.
확장성: 타입 체커와 검색 로직이 독립적이므로, 이 기법은 서구조 (substructural), 단일 (univalent), 또는 모달 (modal) 타입 이론 등 다양한 언어로 확장 적용 가능합니다.
실용적 가치: 이 작업은 DTT 기반의 정리 증명 및 프로그램 합성 도구 개발을 위한 강력한 기반을 제공하며, 자동 추론 분야에서 완전한 솔버의 실현 가능성을 입증했습니다.

요약하자면, 이 논문은 모나드 기반의 제어 흐름과 효율적인 데이터 구조를 결합하여 DTT 의 결정 불가능한 문제를 완전하게 해결할 수 있음을 보여주었으며, 이를 통해 자동 추론 시스템의 한계를 넓히는 중요한 이정표를 제시했습니다.