이 논문은 **"Agda(아그다)"**와 **"Vampire(뱀파이어)"**라는 두 개의 완전히 다른 세계의 소프트웨어가 만나서, 서로의 힘을 합쳐 어려운 수학 문제를 해결하는 방법을 소개합니다.
이 내용을 일상적인 언어와 비유로 쉽게 설명해 드릴게요.
1. 두 주인공: 꼼꼼한 건축가 vs. 빠른 해커
이 이야기에는 두 명의 주인공이 나옵니다.
Agda (아그다): "완벽주의 건축가"
아그다는 소프트웨어나 수학 증명을 할 때, 절대 실수를許하지 않는 건축가입니다. 모든 단계가 논리적으로 완벽해야만 "이건 안전하다"라고 인정해 줍니다.
하지만 이 건축가는 너무 꼼꼼해서, 아주 사소한 문제 (예: "이 벽돌이 저 벽돌과 똑같은가?") 를 증명하는 데도 몇 시간씩 걸릴 때가 많습니다. 마치 매번 모든 나사를 다시 조이는 것과 같습니다.
Vampire (뱀파이어): "빠른 해커"
뱀파이어는 수천 개의 문제를 순식간에 해결할 수 있는 초고속 자동화 도구입니다. 논리적으로 "정답"을 찾아내는 데는 천재적이지만, 아그다처럼 "왜 그런지"에 대한 상세한 설명이나 증명 과정을 꼼꼼하게 기록하지는 않습니다.
또한, 뱀파이어는 고전적인 논리 (예: "아니면 아니면" 같은 방식) 를 사용하는데, 아그다는 "구체적인 증거"를 요구하는 방식 (구성적 논리) 을 씁니다. 서로 언어가 달라서 대화도 안 됩니다.
2. 문제: 서로 통하지 않는 두 세계
연구자들은 아그다 건축가가 지은 건물의 약한 부분 (증명이 필요한 작은 문제들) 을 뱀파이어 해커에게 맡기고 싶었습니다.
하지만 문제는: 뱀파이어가 찾아낸 답을 아그다 건축가가 받아주지 않았습니다. "너는 답만 알려줬지, 어떻게 그 답에 도달했는지 증명해 줄 수 없어? 내 규칙에 맞지 않아."라고 거절당했습니다.
기존에는 이 두 가지를 연결하려면 아주 복잡한 번역기와 중재자가 필요해서, 구현하기 매우 힘들었습니다.
3. 해결책: "공통 언어"와 "변신술"
연구자들은 두 주인공이 대화할 수 있는 **가장 단순하고 공통된 언어 (Horn 논리)**를 찾아냈습니다. 그리고 다음과 같은 3 단계 마법을 부렸습니다.
번역 (Agda → Vampire):
아그다 건축가가 "이 벽돌이 저 벽돌과 같은가?"라고 묻는 복잡한 질문을, 뱀파이어가 이해할 수 있는 간단한 암호문으로 바꿉니다.
비유: 복잡한 건축 도면을, 뱀파이어가 읽을 수 있는 간단한 "A+B=C" 같은 수학 공식으로 요약하는 것입니다.
해결 (Vampire's Work):
뱀파이어는 이 간단한 공식을 순식간에 분석해서 "네, 맞습니다!"라고 답을 찾아냅니다.
비유: 뱀파이어가 초고속으로 계산기를 두드려서 정답을 찾아내는 순간입니다.
변신 (Vampire → Agda):
여기가 이 연구의 핵심입니다. 뱀파이어가 찾아낸 답을 다시 아그다 건축가가 받아들일 수 있는 완벽한 증명서로 다시 만들어줍니다.
연구자들은 뱀파이어의 답을 받아서, 아그다의 규칙에 맞춰 "이렇게 이렇게 계산했기 때문에 맞습니다"라는 상세한 증명 과정을 자동으로 재구성했습니다.
비유: 뱀파이어가 "정답은 42 입니다!"라고 외치면, 연구자가 만든 **변신 로봇 (Prolog 스크립트)**이 그 소리를 듣고 "42 가 맞습니다. 왜냐하면 20+22 이고, 20 은 10+10 이고..."라고 아주 상세한 증명서를 작성해 아그다에게 건네주는 것입니다.
4. 실제 성과: 2 일 걸릴 일을 1 초 만에
이 시스템을 실제로 테스트해 보았습니다.
과거: 복잡한 수학 문제 (복소수와 단위근의 성질) 를 증명하려면, 전문 아그다 개발자가 2 일 동안 밤을 새워가며 수동으로 증명해야 했습니다.
현재: 이 시스템을 쓰니, 수 초 만에 자동으로 모든 증명이 완료되었습니다.
아그다 건축가는 이 자동 생성된 증명서를 받아서 "오, 완벽하네!"라고 승인해 주었습니다.
5. 결론: 왜 이 연구가 중요한가요?
이 연구는 **"두 개의 서로 다른 세계를 억지로 합치려 하지 않고, 서로가 가장 잘하는 부분만 연결했다"**는 점이 훌륭합니다.
아그다는 여전히 안전하고 신뢰할 수 있는 건축가 역할을 합니다.
뱀파이어는 빠른 계산과 문제 해결을 담당합니다.
그 사이를 연결하는 작은 번역기는 아주 간단하게 만들어져 유지보수도 쉽습니다.
한 줄 요약:
"엄청나게 꼼꼼한 건축가 (아그다) 가 지루한 작은 문제들을 해결하느라 지칠 때, 초고속 해커 (뱀파이어) 가 순식간에 답을 찾아주고, 그 답을 다시 건축가가 인정할 수 있는 완벽한 문서로 바꿔주는 자동화 비서를 개발했습니다."
이 기술은 앞으로 소프트웨어 버그를 찾거나, 복잡한 수학 이론을 증명할 때 개발자들의 시간을 획기적으로 줄여줄 것으로 기대됩니다.
논문 요약: Agda 와 Vampire 의 만남 (When Agda met Vampire)
이 논문은 의존적 타입 이론 (Dependent Type Theory) 기반의 증명 보조기 (Proof Assistant) 인 Agda와 자동 정리 증명기 (ATP) 인 Vampire를 통합하여, Agda 의 증명 자동화 수준을 획기적으로 향상시키는 경량 통합 프레임워크를 제안합니다.
1. 문제 제기 (Problem)
증명 보조기의 한계: Agda, Lean, Rocq 와 같은 의존적 타입 기반 증명 보조기는 '구성 - 증명 (correct-by-construction)' 패러다임을 통해 높은 수준의 신뢰성을 보장합니다. 하지만 Curry-Howard 대응에 따라 모든 정리가 타입으로 표현되고, 이를 증명하기 위해 개발자가 직접 증명 의무 (proof obligations) 를 해결해야 합니다.
자동화의 부재: 이러한 증명 의무 중 상당수는 수학적으로 깊지 않으나 반복적이고 지루한 작업 (예: 두 구조의 동형 증명, 단순 속성 확인) 입니다. 현재 Agda 는 내장된 자동화 전략이 부족하여, 이러한 단순한 증명에도 전문 개발자가 많은 시간을 소모합니다.
기존 접근법의 문제: Isabelle 의 Sledgehammer 나 CoqHammer 와 같은 기존 '해머 (hammer)' 시스템은 외부 ATP 를 활용하지만, Agda 와 같은 의존적 타입 시스템에서는 다음과 같은 근본적인 불일치가 존재합니다.
논리 체계의 차이: ATP(Vampire 등) 는 **고전 논리 (Classical Logic)**와 **1 차 논리 (First-Order Logic)**를 기반으로 하는 반면, Agda 는 **구성적 논리 (Constructive Logic)**와 의존적 타입 이론을 기반으로 합니다.
신뢰성 문제: 외부 ATP 는 증명 과정에 '증명 항 (proof term)'을 제공하지 않거나, 고전 논리 (배제 중의 법칙 등) 를 사용하여 구성적 논리에서 유효하지 않은 증명을 생성할 수 있습니다.
구현 복잡도: 기존 해머 시스템은 내부 증명 재구성을 위해 복잡한 매핑과 신뢰성 보장을 위한 커널 수정이 필요하여 구현이 어렵습니다.
2. 방법론 (Methodology)
저자들은 두 시스템 간의 **공통된 표현 가능한 문법 조각 (Expressive Fragment)**을 찾아 양방향으로의 단순하고 신뢰할 수 있는 변환을 수행하는 경량 통합 방식을 채택했습니다.
2.1 핵심 아이디어: Horn 절 (Horn Clauses)
Agda 의 많은 증명 목표와 전제들은 Horn 절 (Horn Clauses) 형태로 표현될 수 있습니다 (즉, R1→R2→⋯→Rn 형태의 명제).
이 조각은 Agda 의 의존적 타입과 Vampire 의 1 차 논리 모두에서 자연스럽게 매핑될 수 있는 공통 언어입니다.
2.2 통합 워크플로우
반사 (Reflection) 를 통한 추출: Agda 의 내장 반사 (Reflection) 기능을 사용하여 현재 증명 목표 (Goal) 와 필요한 보조 정리 (Lemmas) 를 구문 분석 트리 (AST) 로 추출합니다.
SMT-LIB 변환: 추출된 Agda 항을 Vampire 가 이해할 수 있는 SMT-LIB 형식 (Horn 절) 으로 변환합니다.
kty, kdata, kfun 등의 매크로를 사용하여 타입, 데이터 타입, 함수를 Vampire 의 술어와 함수 기호로 매핑합니다.
목표는 부정을 가하여 (Negation) Vampire 의 반증 (Refutation) 모드로 입력합니다.
Vampire 실행: 변환된 입력을 Vampire 에 전달하여 증명을 수행합니다. Vampire 는 고전 논리를 사용하여 빈 절 (Empty Clause, ⊥) 을 유도하여 증명을 완료합니다.
증명 재구성 (Proof Reconstruction):
논리 변환: Vampire 의 고전적 반증 (Γ,¬G⊢⊥) 을 구성적 증명 (Γ⊢G) 으로 변환합니다. 이는 Friedman 의 A-translation 기법과 유사하게, ⊥을 목표 G로 치환하는 논리적 변환을 통해 이루어집니다.
Prolog 기반 변환: Vampire 가 생성한 TSTP 형식의 증명 로그를 Prolog 스크립트가 파싱합니다. Prolog 의 백트래킹 (Backtracking) 기능을 활용하여 각 추론 단계 (Resolution, Superposition 등) 를 Agda 의 증명 항 (Proof Term) 으로 매핑합니다.
타입 검사: 생성된 Agda 증명 항을 Agda 의 타입 체커에 통과시켜 신뢰성을 최종적으로 검증합니다.
2.3 기술적 특징
비침습적 (Non-invasive): Agda 나 Vampire 의 내부 코드를 수정하지 않고, 외부 인터페이스 (Reflection, Prolog) 만을 활용합니다.
Prolog 활용: 증명 재구성에 Prolog 를 사용한 것은 변수 이름 변경 (Variable Renaming) 과 같은 복잡한 작업을 Prolog 의 내장 메커니즘으로 자연스럽게 처리할 수 있어 구현이 간결합니다 (500 줄 미만의 코드).
3. 주요 기여 (Key Contributions)
경량 통합 프레임워크: Agda 와 Vampire 를 통합하여 Agda 의 증명 자동화를 가능하게 하는 최초의 실용적인 프로토타입을 제시했습니다.
Horn 절 기반의 양방향 변환: 의존적 타입 이론과 고전 1 차 논리 간의 불일치를 해결하기 위해, 두 시스템 모두에서 유효한 Horn 절 조각을 식별하고 이를 기반으로 한 신뢰할 수 있는 변환 메커니즘을 개발했습니다.
Prolog 기반 증명 재구성: 외부 ATP 의 증명을 구성적 증명 항으로 변환하는 효율적인 방법을 제안했습니다. 이는 기존에 복잡한 매핑이 필요했던 방식보다 구현이 간단하고 유지보수가 용이합니다.
실제 사례 검증: 복잡한 단위 (Roots of Unity) 를 갖춘 복소수 필드 (Complex Field) 의 속성을 증명하는 실제 연구 프로젝트에 적용하여 그 유효성을 입증했습니다.
4. 결과 (Results)
성능: 실제 연구 프로젝트에서 복소수 필드와 단위근 (Roots of Unity) 의 속성을 증명하는 데 전문 Agda 개발자가 약 2 일이 소요되었던 작업을, 이 시스템은 수십 초 이내에 자동으로 증명했습니다.
신뢰성: 생성된 모든 증명은 Agda 의 타입 체커를 통과하여 신뢰성이 보장됩니다.
확장성: 21 가지의 추론 규칙 (Inference Rules) 을 처리할 수 있으며, TPTP 벤치마크 세트의 지원된 조각 내에서 성공적으로 작동함을 확인했습니다.
5. 의의 및 결론 (Significance)
실용성: 의존적 타입 시스템의 채택 장벽 중 하나인 '지루한 증명 의무'를 효과적으로 제거하여, 실제 소프트웨어 및 수학 형식화 프로젝트의 생산성을 높일 수 있음을 보여줍니다.
일반성: 이 접근법은 Agda 에 국한되지 않습니다. 반사 (Reflection) 기능을 지원하는 다른 의존적 타입 증명 보조기 (Lean, Idris 등) 나 다른 ATP(E, Zipperposition 등) 로도 쉽게 확장 가능합니다.
미래 전망: 현재는 Horn 절에 제한되어 있지만, 이 프레임워크는 더 풍부한 타입 (파라미터화된 타입, 인덱스된 가족 등) 과 더 복잡한 논리 구조를 지원하도록 발전할 수 있는 기반을 마련했습니다.
요약하자면, 이 논문은 **"가장 잘하는 것을 활용한다 (Playing to strengths)"**는 철학 하에, Agda 의 신뢰성과 Vampire 의 강력한 자동화 능력을 결합하여, 복잡한 증명 보조기 환경에서도 실용적인 자동화 해머 시스템을 구축할 수 있음을 증명했습니다.