Anti-Unification Completeness Analysis in PVS

두 개의 매우 다른 레고 성이 있다고 상상해 보세요. 하나는 아주 작고 단순한 탑이고, 다른 하나는 비밀 통로가 있는 거대하고 복잡한 요새입니다. 이제 당신은 두 성의 '정수(essence)'를 모두 담아낼 수 있는 '마스터 청사진'을 만들고 싶습니다. 당신은 그들이 공유하는 부분(예: "문이 있음" 또는 "지붕이 있음")을 찾아내고, 고유하고 혼란스러운 부분들을 일반적인 자리 표시자(예: "어떤 색깔의 블록")로 바꾸고 싶어 합니다. 이 과정, 즉 공통점을 찾으면서 차이점은 숨기는 기술을 **역통일(anti-unification)**이라고 부릅니다.

수십 년 동안 컴퓨터 과학자들은 이 기술을 사용하여 버그를 수정하고, 복사된 코드를 찾아내며, 심지어 느린 소프트웨어를 빠른 병렬 소프트웨어로 변환해 왔습니다. 하지만 한 가지 문제가 있었습니다. 우리는 청사진을 만드는 레시피(알고리즘)는 가지고 있었지만, 모든 가능한 성의 쌍에 대해 그 레시피가 항상 완벽하게 작동한다는 수학적으로 빈틈없는 보증은 가지고 있지 않았습니다. 우리는 그것이 오류를 일으키지 않는다는 것("건전성", sound)은 알고 있었지만, 그것이 매번 가장 최선의 청사진을 찾아낸다는 것("완전성", complete)은 증명하지 못했습니다.

이 논문은 연구팀이 PVS라는 디지털 증명 검사기를 사용하여 마침내 그 누락된 보증을 구축해 낸 이야기입니다.

"해결된" 조각들의 퍼즐

이것이 왜 그렇게 어려웠는지 이해하려면 알고리즘이 어떻게 작동하는지를 살펴봐야 합니다. 알고리즘은 두 성을 조각조로 분해합니다.

• 쉬운 부분: 만약 똑같은 벽돌 두 개를 발견하면, "알았어!"라고 말하며 다음으로 넘어갑니다.
• 까다로운 부분: 만약 서로 다른 두 벽돌(예: 빨간색과 파란색)을 발견하면, 일반적인 매칭 게임처럼 포기하는 대신, "아, 이것들은 다르구나! 이 차이점을 기억해 두고 다른 빨간색 대 파란색 불일치 사례들도 계속 찾아보자"라고 말합니다.

일반적인 매칭 게임(이를 "통일(unification)"이라 부릅니다)에서는 차이점을 찾는 것이 곧 패배를 의미합니다. 하지만 역통일에서는 차이점을 찾는 것이 바로 목표입니다. 알고로리즘은 발견한 모든 차이점을 기록하는 '실행 일지'를 계속 작성해야 합니다.

연구자들은 알고리즘이 "쉬운" 부분에 대해 작동함을 증명하는 것이 놀라울 정도로 어렵다는 것을 발견했습니다. 실제로 그들이 이전 작업들을 살펴보았을 때, 알고리즘이 올바르게 작동함을 증명하는 데 들어간 노력의 **91.10%**가 단 두 가지 특정 사례, 즉 "해결된" 문제(알고리즘이 차이점을 포착하는 경우)와 "구문적(syntactic)" 문제(조각들이 동일한 경우)를 처리하는 데 집중되었습니다. 단순해 보이지만, 알고리즘이 혼동 없이 이러한 차이점들을 정확하게 기록하고 있음을 증명하는 데는 엄청난 양의 엄격한 검증이 필요했습니다.

알고리즘의 "역사책"

이 논문의 주요 돌파구는 알고리즘이 최선의 청사진을 찾는 것을 증명하려면 단순히 현재 단계만을 봐서는 안 된다는 점을 깨달은 데 있습니다. 당신은 계산의 전체 역사를 보아야 합니다.

저자들은 알고리즘의 "메모리"를 생각하는 새로운 방법을 도입했습니다. 그들은 다음을 모두 고려하는 마스터 청사진인 "전체 일반화자(Total Generalizer)"라는 멋진 용어를 정의했습니다:

1. 아직 확인을 기다리고 있는 조각들.
2. 이미 확인되었고 "다름"으로 표시된 조각들.
3. 알고리즘이 진행하면서 만들어가는 "치환(substitution)"(규칙 목록).

그들은 여러 가지 "불변성 속성(invariance properties)"을 증명했습니다. 이것은 "알고리즘이 몇 단계를 거치든, 지금까지 찾아낸 차이점의 전체 목록이 사라지거나 그 의미가 변하지 않는다"라고 말하는 규칙과 같습니다. 그들은 알고리즘이 큰 문제를 작은 하위 문제들로 나눌 때조차도, 원래 문제의 "이야기"가 마치 조각난 퍼즐 조각들을 섞어 놓아도 전체 그림은 그대로 유지되는 것처럼 온전히 유지된다는 것을 보여주었습니다.

"제한된" 청사진

여기서 영리한 반전이 있습니다. 증명을 성공시키기 위해 저자들은 **"제한된 전체 일반화자(Restricted Total Generalizer)"**라는 특별한 종류의 청 blueprint를 발명해야 했습니다.

당신이 요리법을 쓰고 있다고 상상해 보세요. 만약 주방에 이미 있는 재료(알고리즘이 현재 사용 중인 변수들)를 사용한다면, 요리법을 쓰는 도중에 실수로 레시피를 바꿔버릴 수도 있습니다. 그래서 저자들은 "우리의 증명을 위해 오직 신선하고 사용되지 않은 재료만 사용하자"라고 말했습니다. 그들은 만약 이 "신선한" 재료들을 사용하는 청사진을 찾을 수 있다면, 그것을 언제든지 일반적인 청사진으로 다시 변환할 수 있다는 것을 증명했습니다.

이러한 신선한 재료들로 청사진을 제한함으로써, 그들은 **정리 20(Theorem 20)**을 증명할 수 있었습니다: 알고리즘의 최종 결과는 당신이 생각해 낼 수 있는 그 어떤 다른 청사진보다도 최소한 그만큼은 구체적이라는 것입니다. 즉, 알고리즘은 결코 더 나은 해결책을 놓치지 않습니다.

이것이 의미하는 것 (그리고 의미하지 않는 것)

이 논문은 구문적 역통일(syntactic anti-unification)을 위한 규칙 기반 알고리즘이 **완전하다(complete)**는 것을 (단순히 제안하는 것이 아니라) 증명합니다. 이는 이 알고리즘이 임의의 두 항(term)에 대해 항상 최소 일반화자(가장 정밀한 공통 청사진)를 찾아낸다는 것이 수학적으로 보장됨을 의미합니다.

하지만 이 논문은 아직 하지 못한 부분에 대해서도 매우 신중하게 명시하고 있습니다:

• 이 논문은 지금 당장 실행할 수 있는 최종적인 "기계 검증 실행 코드"를 제공하는 것이 아닙니다. 저자들은 새로운 정의와 보조 정리(lemma)의 정식화가 "진행 중인 작업(work in progress)"이라고 밝히고 있습니다.
• 이 논문은 모든 종류의 수학(교환 법칙이나 결합 법칙이 포함된 경우 등)에 대한 역통일 문제를 해결했다고 주장하는 것이 아닙니다. 이 논문은 엄격히 "구문적" 역통일(표준적인 방식)에 초점을 맞추고 있습니다.
• 이 논문은 알고리즘이 속도 측면에서 빠르거나 효율적이라고 주장하는 것이 아닙니다. 단지 그 "논리"가 올바르고 완전하다는 것을 증명할 뿐입니다.

결론

이 논문은 컴퓨터 알고리즘에 대한 엄격하고 단계적인 해부입니다. 저자들은 단순히 "작동한다"라고 말한 것이 아닙니다. 그들은 디지털 논리의 요새를 구축하여 모든 단계, 특히 알고리즘이 차이점을 포착하는 지루하지만 결정적인 부분을 하나하나 검사했습니다. 그들은 완벽한 "계산의 역사책"을 유지하고, 솔루션을 생각하는 영리한 "제한된" 방식을 사용함으로써, 알고리즘이 항상 정답을 찾아낸다는 것을 보여주었습니다.

이제 수학적으로 증명되었으므로, 다음 단계인 "인증된 실행 코드 추출"을 위한 문이 열렸습니다. 이는 미래에 우리가 이 알고리즘을 가져와서 코드나 화학 화합물에서 공통 패턴을 찾는 데 있어 수학적으로 결코 실수하지 않을 것이라고 보장되는 소프트웨어로 바꿀 수 있음을 의미합니다. 하지만 지금 단계에서의 승리는 증명 그 자체에 있습니다. 왜 이것이 작동하는지에 대한 미스터리가 마침내 풀렸기 때문입니다.