Verification of a DPLL Transition System in Rocq

컴퓨터가 끊임없이 "참 또는 거짓"이라는 고도의 심리전을 벌이는 세상을 상상해 보십시오. 이 게임에서 컴퓨터는 "설탕을 넣으면 반드시 밀가루도 넣어야 하지만, 밀가루를 넣으면 소금은 넣을 수 없다"와 같은 논리적 문장들이 엉킨 거대한 매듭을 건네받습니다. 목표는 규칙을 어기지 않고 레시피를 따르는 방법을 찾는 것입니다. 이것이 바로 충족 가능성(Satisfiability, SAT) 문제입니다. 이는 어떤 조각은 빨간색이고 어떤 조각은 파란색이며, 지침에는 "빨간색 옆에 파란색을 두지 마시오"라고 적혀 있는, 수백만 개의 퍼즐 조각을 상자에 끼워 맞추려는 시도와 디지털적으로 매우 유사합니다.

왜 우리가 이것에 관심을 가져야 할까요? 이것은 단순한 논리 퍼즐이 아니라, 컴퓨팅의 거의 모든 복잡한 과정 뒤에 있는 엔진이기 때문입니다. 마이크로칩을 설계하는 것부터 수학적 정리가 참인지 증명하는 것에 이르기까지, 컴퓨터는 이러한 거대한 논리의 미로를 헤쳐 나가기 위해 SAT 솔버(solver)를 사용합니다. 하지만 여기 함정이 있습니다. 이러한 솔버들은 믿을 수 없을 정도로 복잡합니다. 만약 코드 안에 아주 작은 버그 하나라도 숨어 있다면, 컴퓨터는 어떤 증명이 유효하다고 자신 있게 말하지만 실제로는 엉터리일 수도 있습니다. 이것이 바로 수학자와 컴퓨터 과학자들이 **형식 검증(formal verification)**에 집착하는 이유입니다. 형식 검증을 일종의 "수학적 현미경"(증명 보조기라고 불리는 도구)이라고 생각하십시오. 이는 논리의 모든 단계를 점검하여 기계가 결코 답에 대해 거짓말을 할 수 없도록 만드는, 매우 엄격하고 깨지지 않는 안전망을 구축하는 작업입니다.

논문의 위대한 모험: 신뢰할 수 있는 논리 기계 구축하기

이 논문에서 율리아 디스트라(Julia Dijkstra)와 베네딕트 아렌스(Benedikt Ahrens)는 이러한 논리 기계를 신뢰할 수 있게 만드는 데 있어 거대한 도약을 이뤄냈습니다. 그들은 단순히 프로그램을 작성한 것이 아니라, Rocq라는 도구 안에 DPLL(Davis-Putnam-Logemann-Loveland)이라 불리는 유명한 논리 해결 방법의 수학적으로 증명된 골격을 구축했습니다.

DPLL 방법을 경직된 로봇이 대본을 따르는 것이 아니라, "상태 전환(State Switching)" 게임이라고 생각해 보십시오. 탐정이 미스터리를 해결하려고 노력한다고 상상해 봅시다. 탐정은 빈 공책(단서 없음)에서 시작합니다. 그들에게는 공책을 업데이트하는 규칙들이 있습니다:

1. "아, 알겠다!" 규칙 (단위 전파, Unit Propagate): 만약 단서가 "집사 혹은 메이드가 범인이다"라고 말하고, 탐정이 이미 메이드가 무죄라는 것을 알고 있다면, 공책은 반드시 "집사가 범인이다"라고 업데이트되어야 합니다. 탐정에게는 선택의 여지가 없습니다. 논리가 움직임을 강제합니다.
2. "순수 추측" 규칙 (순수 리터럴, Pure Literal): 만약 탐정이 "정원사"에 대한 단서는 보았지만 "정원사가 아니다"라는 단서는 한 번도 보지 못했다면, 그는 모순에 대한 두려움 없이 정원사가 관련되었을 것이라고 안전하게 추측할 수 있습니다.
3. "가지치기" 규칙 (결정, Decide): 만약 탐정이 막혔다면, 그는 무작위 단서(예: "집사가 범인이다")를 골라 이를 하나의 **결정(decision)**으로 기록합니다. 이것은 갈림길입니다.
4. "앗, 잘못된 길이다" 규칙 (백트래킹, Backtrack): 만 만약 탐정이 결정을 내렸는데 나중에 모순(예: "집사는 범인이 아니다"라는 단서)을 발견한다면, 그는 그 결정 이후에 일어난 모든 일을 지우고, 결정을 뒤집은 후(이제 집사는 범인이 아니다), 다시 시도해야 합니다.
5. "게임 종료" 규칙 (실패, Fail): 만약 모든 것을 지우고 마지막 결정을 뒤집었음에도 여전히 모순에 부딪힌다면, 게임은 끝난 것입니다. 그 미스터리는 풀 수 없는 것입니다.

저자들의 주요 업적은 이 전체 게임을 Rocq가 읽고 검증할 수 있는 언어로 기술한 것입니다. 그들은 단순히 "이것은 옳아 보인다"라고 말한 것이 아닙니다. 그들은 세 가지 거대한 사실을 증명했습니다:

• 정확성(Correctness): 만약 게임이 해결책과 함께 끝난다면, 그 해결책은 확실히 실제적인 것입니다. 컴퓨터는 가짜 모델을 환각해내지 않습니다.
• 완전성(Completeness): 만약 해결책이 존재한다면, 게임은 반드시 그것을 찾아낼 것입니다. 컴퓨터는 멈춰 있거나 하지 않아도 될 때 포기하지 않습니다.
• 종료성(Termination): 게임은 영원히 실행되지 않습니다. 게임은 해결책을 찾든, "게임 종료"에 도달하든 수학적으로 반드시 멈춘다는 것이 보장됩니다.

새로운 반전 추가: "순수" 규칙

이 논문의 멋진 기여 중 하나는 이전 버전의 이론들이 놓쳤던 특정 규칙인 **순수 리터럴 규칙(Pure Literal Rule)**을 게임에 추가한 것입니다. 탐정의 비유에서, 이것은 탐정이 "잠깐, 정원에 대해서는 아무런 반대 증거를 본 적이 없으니, 그냥 정원사가 범인이라고 가정하자"라고 깨닫는 순간입니다. 저자들은 이 규칙을 추가하는 것이 안전 보장을 깨뜨리지 않으면서도 게임을 더 빠르게 만든다는 것을 증명했습니다. 그들은 이 추가적인 지름길을 사용하더라도 논리가 여전히 빈틈없이 견고하다는 것을 보여주었습니다.

이론에서 실제 (하지만 단순한) 로봇으로

이론적으로 게임의 규칙이 완벽하게 작동함을 증명한 후, 저자들은 다음과 같이 질문했습니다. "우리가 실제로 이 게임을 플레이하는 로봇을 만들 수 있을까?" 그들은 탐정이 다음 규칙을 무엇을 선택할지에 대한 지침인 **전략(strategy)**을 만들었습니다. 그들은 Rocq에서 이 전략의 구체적인 버전을 구축했고, 그 후 **추출(extraction)**이라는 마법 같은 도구를 사용하여 수학적 증명을 OCaml로 작성된 실제 컴퓨터 프로그램으로 변환했습니다.

그들은 이 새로운 로봇을 몇 가지 간단한 퍼즐로 테스트했습니다. 작동했습니다! 로봇은 155개의 변수와 1,135개의 절이 포함된 zebra.cnf라는 퍼즐을 포함하여 문제들을 정확하게 해결했습니다. 그러나 저자들은 로봇의 한계에 대해 매우 솔직합니다. 이것은 마치 프로토타입 장난감 자동차와 같습니다. 엔진이 작동한다는 것을 증명하기 위해 완벽하게 주행하지만, 아직 포뮬러 1 레이싱 카는 아닙니다. 실제 레이싱 카는 고속 메모리를 사용하는 반면, 이 로봇은 단서를 기억하기 위해 단순한 리스트를 사용하기 때문에 느립니다. 저자들은 이 버전이 오늘날 기업들이 사용하는 산업용 거물들을 이길 준비가 되지 않았음을 인정하지만, 이것은 하나의 **검증된 핵심(verified core)**입니다. 이는 더 빠르고 스마트한 솔버를 구축할 수 있는 작지만 깨지지 않는 기초입니다.

이것이 미래에 의미하는 바

이 논문은 세계에서 가장 빠른 SAT 솔버를 만드는 문제를 해결했다고 주장하는 것이 아닙니다. 대신, 그들은 가장 안전한 가능한 청사진을 만들었다고 주장합니다. Rocq에서 추상적인 규칙을 증명함으로써, 그들은 "신뢰할 수 있는 핵심"을 만들어냈습니다. 미래의 연구자들은 이제 이 청사진을 가져가서, 현대적인 솔버의 화려한 기능들—예를 들어 "실수로부터 배우기(절 학습)"나 "여러 단계를 한꺼번에 되돌아가기(비연속적 백트래킹)" 등—을 추가하면서도, 그 근저에 깔린 논리가 여전히 건전하다는 확신을 가질 수 있습니다.

요약하자면, 디스트라와 아렌스는 더 나은 자동차를 만든 것이 아니라, 절대로 사고가 날 수 없는 자동차의 청사진을 만들었으며, 바퀴 뒤에 있는 논리가 수학적으로 완벽하다는 것을 증명했습니다. 이것은 미래의 훨씬 더 크고 복합적이며 신뢰할 수 있는 논리 기계로 가는 길을 닦는, 검증된 작은 발걸음입니다.