Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

탐정의 가이드: 사물을 일치시키는 법

당신이 두 가지 서로 다른 범죄 현장 묘사가 사실은 동일한 사건임을 밝혀내야 하는 미스터리를 해결하려는 탐정이라고 상상해 보십시오. 한 목격자는 "용의자는 빨간 모자와 파란 코트를 입었다"라고 말합니다. 다른 목격자도 "용의자는 빨간 모자와 파란 코트를 입었다"라고 말한다면 아주 쉽겠죠? 하지만 만약 두 번째 목격자가 "용의자는 빨간 모자와 파란 코트를 입었지만, 그 모자는 사실 파란 코트를 위한 변장이었다"라고 말한다면 어떻게 될까요? 이제 당신은 적절한 값으로 '변수'(색상이나 아이템 같은 구체적인 요소들)를 교체함으로써 이 두 이야기가 일치하게 만들 수 있는지 알아내야 합니다. 컴퓨터 과학의 세계에서 이 퍼즐은 **유니피케이션(unification, 단일화)**이라고 불립니다. 이것은 체스를 두는 인공지능부터 당신의 코드가 올바르게 작성되었는지 확인하는 소프트웨어에 이르기까지 모든 것을 움직이는 엔진입니다.

수십 년 동안 컴퓨터 과학자들은 기계에게 이 퍼즐을 자동으로 풀도록 가르치기 위해 노력해 왔습니다. 목표는 단순히 컴퓨터가 "예, 일치합니다"라고 말하게 하는 것이 아니라, 컴퓨터가 그것들을 일치시키는 단계별 레시피(알고리즘)를 직접 발명하도록 하는 것입니다. 이것을 **연역적 프로그램 합성(deductive program synthesis)**이라고 합니다. 이것을 똑똑한 로봇에게 수학 정리를 증명하라고 요청하는 것과 같다고 생각하십시오. 다만 로봇은 마지막에 단순히 "Q.E.D."라고 쓰는 대신, 문제를 해결하는 데 실제로 작동하는 소프트웨어를 당신에게 건네주어야 합니다. 여기서 핵심은, 로봇이 그 소프트웨어가 정확하다는 것을 반드시 확신해야 한다는 점입니다. 왜냐하면 증명이 곧 보증이기 때문입니다. 증명이 성립하면 프로그램은 작동합니다. 증명이 실패하면 그 프로그램은 쓰레기입니다.

논문의 위대한 발견: 스스로 퍼즐 해결사를 만드는 법을 배우는 로봇

리처드 월디어(Richard Waldinger)가 쓴 이 논문은, 오직 논리의 규칙만을 사용하여 유니피케이션 알고리즘을 처음부터 구축하도록 요청받은 **스나크(Snark)**라는 이름의 로봇에 관한 이야기입니다. 저자는 스나크에게 정답을 그냥 준 것이 아니라, 일련의 논리적 규칙(공리적 이론)과 목표를 주었습니다: "이 두 표현식을 동일하게 만드는 치환(substitution)을 찾아라."

이 논문의 주요 발견은 스나크가 작동하는 유니피케이션 알고리즘을 **자동으로 도출(automatically derived)**하는 데 성공했다는 점입니다. 스나크는 기존의 것을 단순히 복사한 것이 아니라, 이전의 수동 시도들보다 실제로 더 효율적이고 이해하기 쉬운 새로운 버전을 발견해 냈습니다. 로봇은 문제 생성을 거대한 논리 퍼즐로 취급함으로써 이 일을 해냈습니다. 스나크는 모호한 목표에서 시작하여, 문제를 더 작은 사례들(예: "첫 번째 항목이 상수라면?", "변수라면?")로 나누는 과정을 통해 복잡한 "if-then-else" 결정 트리(decision tree)를 구축했습니다. 이 트리가 최종적인 프로그램이 됩니다.

논문은 이것이 단순한 일회성 요행이 아니라는 점을 명시적으로 배제합니다. 저자는 적절한 논리적 규칙을 설정하고 적절한 "기초 관계(well-founded relations)"(로봇이 무한 루프에 빠지지 않도록 보장하는 규칙을 의미함)를 선택하는 과정에서 많은 "인간의 도움"이 필요했음을 인정합니다. 또한 논문은 유니피케이션이 단순하고 직관적인 문제가 아니라는 주장에도 반박합니다. 논문의 한 구절처럼, "철저한 제시가 시도될 때, 그것이 상당히 미묘하고 까다로운 문제라는 점이 깨지게 된다." 이 논문은 이것이 모든 프로그램 합성 문제를 해결한다거나 모든 소프트웨어 공학을 위한 마법의 지팡이라고 주장하지 않습니다. 대신, 이 논문은 복잡한 알고리즘의 완전 자동 도출이 가능하다는 것을 보여주는 성공적인 **사례 연구(case study)**로서 이를 제시하며, 이는 여전히 많은 다른 유형의 프로그램들에 대해서는 연구 과제로 남아 있습니다.

로봇은 어떻게 "생각"했는가

스나크가 이 일을 어떻게 수행했는지 이해하려면, 당신이 아이에게 어지러운 장난감 더미를 분류하는 법을 가르친다고 상상해 보십시오. 당신은 단순히 "분류해"라고 말하지 않습니다. 대신 규칙을 줍니다: "만약 블록이라면 빨간 바구니에 넣어. 만약 자동차라면 파란 바구니에 넣어." 그런데 만약 장난감이 블록이면서 동시에 자동차라면 어떻게 될까요? 당신은 그 경우를 위한 규칙도 필요할 것입니다.

스나크는 **데덕티브 타블로(deductive tableaux, 연역적 표)**라고 불리는 방법을 사용했습니다. 화이트보드에 두 개의 열이 있다고 상상해 보십시오: "우리가 아는 것"(단언, Assertions)과 "우리가 찾아야 할 것"(목표, Goals).

1. 목표: "표현식 A와 표현식 B를 동일하게 만드는 방법을 찾아라."
2. 과정: 스나크는 목표를 보고 질문합니다. "만약 A가 변수라면? 만약 상수라면?" 스나크는 문제를 이러한 서로 다른 "경우(cases)"로 나눕니다.
3. "아하!" 모먼트: 스나크는 큰 문제를 해결하기 위해 먼저 동일한 문제의 더 작은 버전을 해결해야 할 수도 있다는 것을 깨달았을 때, **재귀(recursion)**를 도입합니다. 이것은 마치 "이 큰 더미를 분류하려면, 먼저 왼쪽 절반을 분류하고, 그다음 오른쪽 절형을 분류한 뒤, 그 결과를 결합하겠다"라고 말하는 것과 같습니다. 논문은 스나크가 이 과정에서 영원히 분류 작업을 반복하지 않도록 매우 주의해야 했다고 설명합니다. 스나크는 "기초 관계(well-founded relation)"(모든 단계가 문제를 점점 더 작게 만든다는 수학적 보장, 예를 들어 100에서 0으로 숫자를 줄여가는 것과 같은 방식)를 사용하여 프로세스가 결국 멈출 것임을 증명했습니다.

"환경"의 기술

이 논문의 가장 영리한 움직임 중 하나는 로봇이 문제를 더 쉽게 풀 수 있도록 문제를 약간 변형한 것이었습니다. 단순히 "A와 B를 어떻게 매칭하는가?"라고 묻는 대신, 스나크에게 "이미 가지고 있는 매칭 목록이 있을 때, A와 B를 어떻게 매칭하는가?"라고 물었습니다. 이 목록을 **환경(environment)**이라고 부릅니다.

이것은 "사이먼 세즈(Simon Says)" 게임과 같습니다. 사이먼이 "코를 만져"라고 하면 당신은 그렇게 합니다. 하지만 사이먼이 "모자를 써"라고 말한 후에 "코를 만져"라고 한다면, 당신은 모자를 썼다는 사실을 기억하면서 코를 만져야 합니다. 이 "환경"(모자)을 추적함으로써 로봇은 더 효율적인 알고리즘을 구축할 수 있었습니다. 논문은 이 세 개의 인자를 가진 버전(표현식 A, 표현식 B, 그리고 환경)이 인간이 보통 사용하는 단순한 두 개의 인자 버전보다 컴퓨터가 자동으로 합성하기에 실제로 더 쉽다고 제안합니다.

최종 결과: 새로운 레시피

논문은 스나크가 생성한 실제 코드를 보여주며 마무리됩니다. 그것은 긴 "만약 ~라면, 그렇다면 ~이다" 식의 지침들로 이루어져 있습니다.

• 만약 환경이 깨졌다면, "실패(failure)" 신호를 반환하라.
• 만약 두 표현식이 이미 같다면, 현재의 매칭 목록을 반환하라.
• 만약 하나는 변수이고 다른 하나는 상수라면, 그것들을 교체하기 위한 새로운 규칙을 만들어라.
• 만약 둘 다 복잡한 구조(예: 아이템 리스트)라면, 그것들을 왼쪽과 오른쪽 부분으로 나누고, 왼쪽 부분을 먼저 해결한 다음, 그 결과를 사용하여 오른쪽 부분을 해결하라.

논문은 이 프로그램이 **증명 가능하게 정확하다(provably correct)**는 점을 강조합니다. 프로그램이 논리적 증명으로부터 직접 추출되었기 때문에, 우리는 그것이 작동한다는 것을 압니다. 만약 증명이 "이 단계는 유효하다"라고 말한다면, 코드의 단계도 유효합니다. 저자는 스나크 시스템이 증명을 찾는 데 약 10초가 걸렸지만, 진짜 가치는 그 방법론에 있다고 언급합니다. 즉, 우리는 단순히 추측하고 확인하는 것이 아니라, 정리를 증명함으로써 소프트웨어를 구축할 수 있다는 것을 보여준다는 것입니다.

이것이 왜 중요한가 (그리고 왜 아직 마법은 아닌가)

논문은 미래에 대한 유쾌한 암시와 함께 끝을 맺습니다. 현대의 AI(거대 언어 모델 등)가 코드를 작성할 수는 있지만, 때때로 "환각(hallucinate)"을 일으키거나 사실을 지어내기도 한다는 점을 언급합니다. 그들은 겉보기에는 맞지만 숨겨진 버그가 있는 프로그램을 작성할 수도 있습니다. 반면, 연역적 합성은 수학적 증명과 같습니다. 단계가 옳다면 결과는 반드시 옳아야 합니다.

저자는 우리가 이 두 세계를 결합할 수 있는 미래를 제안합니다. 즉, 똑똑한 AI를 사용하여 논리적 규칙과 증명을 위한 "추측"을 설정하는 데 도움을 받고, 엄격한 정리 증명기(theorem prover)를 사용하여 최종 결과를 검증하는 방식입니다. 하지만 현재로서는, 이 논문은 순수 수학의 길로 완벽한 소프트웨어에 도달할 수 있음을 보여주는 하나의 증거로서, 기계가 복잡하고 까다로운 문제를 바라보고 단계별로 스스로의 해결책을 발명해 낼 수 있었음을 입증하고 있습니다.