Towards a Certifying Grounder

당신이 거대하고 복잡한 미스터리를 풀려는 탐정이라고 상상해 보십시오. 당신은 소수의 전문가만이 읽을 수 있는 복잡하고 높은 수준의 코드로 작성된 일련의 단서들을 가지고 있습니다. 이 사건을 해결하기 위해, 당신은 이 단서들을 컴퓨터가 따를 수 있는 단순한 단계별 체크리스트로 번역해야 합니다. 이 번역 과정은 "그라운딩(grounding)"이라고 불립니다. 이것은 은유가 가득한 소설을 "만약 용의자가 주방에 있다면 창문을 확인하라; 만약 그들이 정원에 있다면 울타리를 확인하라"와 같은 엄격한 지침 목록으로 바꾸는 것과 같습니다.

수십 년 동안, 이 퍼즐들을 푸는 컴퓨터들은 믿기지 않을 정도로 빠르고 똑똑해졌습니다. 하지만 숨겨진 문제가 있습니다. 때때로 이 번역 단계(그라운딩)에서 실수가 발생하거나, 컴퓨터가 혼란에 빠져 거기에 없던 단서를 만들어내기도 합니다. 만약 번역이 틀린다면, 컴퓨터의 논리가 아무리 완벽하더라도 최종 답안은 틀린 것이 됩니다. 현실 세계에서 이것은 매우 중요합니다. 만약 컴퓨터가 우주선 미션을 계획하거나 환자와 신장 기증자를 매칭하는 일을 돕고 있다면, 번역에서의 아주 작은 오류가 재앙으로 이어질 수 있습니다. 우리는 컴퓨터가 단순히 정답을 "추측"한 것이 아니라, 처음부터 끝까지 규칙을 완벽하게 따랐음을 확신할 수 있는 방법이 필요합니다. 여기서 "증명 로깅(proof logging)"이라는 개념이 등장합니다. 이는 마치 두 번째의 더 단순한 탐정이 작업을 검토하고 "네, 당신이 제대로 수행했습니다"라고 말할 수 있도록, 탐정이 자신의 추론 과정을 모든 단계마다 기록하는 것과 같습니다.

이 논문은 이 "증명 로깅"을 번역 단계 자체에 도입하는 CertiFOX라는 새로운 시스템을 소개합니다. 저자들(KU Leuven과 Vrije Universiteit Brussel의 팀)은 단순히 문제를 해결하는 것을 넘어, 고수준의 미스터리에서 저수준의 체크리스트로의 번역이 올바르게 수행되었음을 증명하는 인증서를 작성하는 프레임워크를 구축했습니다. 그들은 세 가지 주요 도구를 만들었습니다: 인증서를 작성하기 위한 새로운 언어, 인증서를 작성하며 작동하는 "그라운더(translator, 번역기)", 그리고 그 인증서를 읽어 작업을 검증하는 "체커(두 번째 탐정)"입니다. 그들의 실험은 이 시스템이 현재의 최고 수준 도구들과 동일하게 잘 작동하며, 증명을 쓰고 확인하는 데 필요한 추가 시간이 매우 적다는 것(아주 작은 상수 배수만큼)을 보여줍니다. 그들은 단지 이것이 작동할 것이라고 제안만 한 것이 아니라, 실제로 구축하고, 실제 퍼즐들로 테스트했으며, 속도를 크게 늦추지 않고도 이 임무를 수행할 수 있음을 증명했습니다.

탐정의 딜레마: 번역가를 신뢰할 수 있는가

이야기를 더 깊이 파헤쳐 봅시다. 컴퓨터 과학, 특히 "선언적 해결(declarative solving)"이라는 분야에서 사람들은 수학이나 논리와 유사해 보이는 고수준 언어를 사용하여 문제를 기술합니다. 이는 읽기 쉽고 우아합니다. 하지만 컴퓨터는 "우아한 논리"를 직접 이해하지 못합니다. 대신 매우 엄격한 저수준 언어(긴 참/거짓 문장의 목록과 같은)를 사용합니다. 우아한 아이디어에서 엄격한 목록으로 넘어가기 위해, **그라운더(grounder)**라고 불리는 특수한 프로그램이 핵심적인 역할을 수행합니다. 그라운더는 고수준의 규칙들을 가져와서 가능한 모든 구체적인 사례로 확장합니다.

이것은 레시피와 같습니다. 고수준 이론은 레시피입니다: "모든 손님을 위해 케이크를 굽는다." 그라운더는 손님 명단을 보고 구체적인 지침을 작성하는 요리사입니다: "앨리스를 위해 케이크를 굽는다. Bob을 위해 케이크를 굽는다. Charlie를 위해 케이크를 굽는다..." 만약 요리사가 손님 수를 잘못 세거나 이름을 누락한다면, 파티는 망쳐집니다. 문제는 이러한 요리사(그라운더)들이 믿을 수 없을 정도로 복잡하다는 점입니다. 그들은 거대한 손님 명단을 빠르게 처리하기 위해 영리한 트릭과 지름길을 사용합니다. 너무나 복잡하기 때문에, 그들이 실수를 하지 않는다고 100% 확신하기 어렵습니다. 만약 요리사가 실수를 한다면, 컴퓨터는 실제로는 해답이 존재하지 않음에도 불구하고 "해답을 찾았습니다!"라고 말할 수도 있고, 그 반대의 경우도 발생할 수 있습니다.

CertiFOX 솔루션: 종이 기록(The Paper Trail)

이 논문의 저자들은 우리가 최종 답안(컴퓨터가 해답을 찾았는가?)을 확인하는 데는 능숙해졌지만, 번역(요리사가 목록을 올바르게 작성했는가?)을 확인하는 데는 미흡했다는 점을 깨달았습니다. 그들은 이 "신뢰의 간극"을 메우고자 했습니다.

이를 위해 그들은 CertiFOX를 구축했습니다. CertiFOX를 요리사가 단순히 요리만 하는 것이 아니라, 자신이 하는 모든 움직임을 상세한 단계별 일기로 기록하는 새로운 종류의 주방이라고 상상해 보십시오.

1. GroundFOX: 이것은 새로운 요리사입니다. 고수준 레시피를 가져와 저수준 목록으로 번역합니다. 하지만 작업하는 동안 특별한 형식의 "증명"을 작성합니다. 단순히 "앨리스를 위해 케이크를 만들었다"라고 말하는 것이 아니라, "나는 손님 명단을 확인했고, 앨리스를 발견했으며, 규칙 4를 적용하여 '앨리스를 위해 굽기'를 작성했다"라고 기록합니다.
2. 증명 형식(The Proof Format): 이것은 일기의 언어입니다. 저자들은 요리사가 따라야 할 특정 규칙 세트(문법)를 설계했습니다. 이 규칙들은 컴퓨터가 쉽게 읽고 모든 단계가 이전 단계로부터 논리적으로 따르는지 검증할 수 있을 만큼 단순합니다.
3. CheckFOX: 이것은 독립적인 검사관입니다. 스스로 미스터리를 풀려고 시도하지 않습니다. 단지 요리사의 일기를 읽고 수학을 검증할 뿐입니다. "요리사가 정말로 명단에서 앨리스를 보았는가? 그렇다. 규칙이 그녀를 위해 굽으라고 했는가? 그렇다. 좋아, 이 단계는 정확하다."

어떻게 작동하는가: "가드(Guards)"의 마법

저자들이 사용한 영리한 트릭 중 하나는 **그라운딩 정규형(Grounding Normal Form, GNF)**이라고 부르는 것입니다. 쉽게 말해, 이것은 요리사가 더 똑똑해질 수 있도록 규칙을 조직하는 방법입니다. 보통 요리사는 세상의 모든 사람을 일일이 확인해야 할 수도 있습니다. 그것은 느립니다. 하지만 GNF를 사용하면 규칙에 "가드(guard)"가 포함됩니다.

특정 배지를 가진 사람들만 들여보내는 문 앞의 경비원을 상상해 보십시오. 요리사는 가드를 통과하는 사람들만 확인하면 됩니다. 논문의 언어로 표현하자면, 이는 그라운더가 무관한 세부 사항을 건너뛸 수 있음을 의미합니다. 예를 들어, 규칙이 "만약 어떤 존재가 비둘기라면, 구멍을 찾아라"라면, 그라운더는 고양이나 바위가 아닌 비둘기만을 살펴봅니다. 이 방식은 번역을 훨씬 빠르게 만들고 증명을 훨씬 짧게 만듭니다. 저자들은 이러한 가드를 사용함으로써 증명(일기)을 압축적이고 관리 가능하게 유지할 수 있음을 보여주었습니다.

테스트 드라이브: 실제로 작동하는가?

팀은 단순히 이론적으로 구축한 것이 아니라, 이를 테스트했습니다. 그들은 몇 가지 표준 퍼즐(지도 색칠하기, 안정 결혼 문제, 숫자 패턴 찾기 등)을 가져와 새로운 시스템을 통해 실행했습니다. 그들은 새로운 요리사(GroundFOX)를 두 명의 유명한 요리사인 IDP-Z3 및 pyclingo와 비교했습니다.

결과는 인상적이었습니다.

• 속도: 새로운 요리사는 전문가만큼 빨랐습니다. 어떤 경우에는 약간 느렸지만, 다른 경우에는 매우 경쟁력이 있었습니다. 거의 모든 퍼즐을 제한 시간 내에 해결했습니다.
• 증명의 비용: 가장 중요한 질문은 "일기를 쓰기 때문에 얼마나 더 느려지는가?"였습니다. 대답은 "그리 많지 않다"였습니다. 증명을 쓰는 데 드는 추가 시간은 아주 작았습니다. 그리고 검사관(CheckFOX)이 일기를 읽을 때, 요리 자체보다 약 2~3배 정도 더 걸렸습니다. 이는 완전한 확실성을 위해 지불할 수 있는 매우 작은 대가입니다.
• 메모리: 흥anche히도, 이 새로운 시스템은 일부 매우 어려운 퍼즐에서 다른 도구들에 비해 메모리 부족 문제를 더 잘 해결했습니다.

저자들은 또한 "일기"(증명)의 크기에 대해서도 조사했습니다. 그들은 대부분의 퍼즐에 대해 일기의 크기가 적절하다는 것을 발견했습니다. 그러나 특정 유형의 퍼즐(RamseyNumbers)의 경우, 일기가 거대해졌습니다. 왜일까요? 그 퍼즐은 "가드"를 효과적으로 사용하지 못해 요리사가 수백만 단계를 기록하도록 강제했기 때문입니다. 이는 "가드"를 적절히 사용하는 것이 증명을 작게 유지하는 데 결정적이라는 점을 가르쳐 주었습니다.

결론

이 논문은 CertiFOX가 선언적 해결을 신뢰할 수 있게 만드는 실행 가능하고 유망한 방법이라고 결론짓습니다. 이는 하드한 문제를 해결할 수 있을 뿐만 아니라, 번역이 올적으로 수행되었다는 수학적 보증을 제공하는 시스템을 가질 수 있음을 입증합니다.

저자들은 자신들이 모든 문제를 해결했다고 주장하지 않도록 주의를 기울였습니다. 그들은 현재 시스템이 특정 유형의 논리(GNF)에 가장 잘 작동하며, 더 복잡한 언어를 다루기 위해 여전히 확장할 필요가 있다고 언급했습니다. 또한 "검사관(CheckFOX)"이 매우 큰 증명에 대해 많은 메모리를 사용할 수 있으며, 이는 향후 해결해야 할 과제라고 덧붙였습니다.

하지만 핵심 메시지는 명확합니다. 우리는 마침내 우리가 작성하는 고수준의 아이디어와 컴퓨터가 주는 저수준의 답 사이의 간극을 메울 수 있습니다. 단순한 독립적 검사를 추가함으로써, 우리는 추측을 멈추고 우리의 컴퓨터 솔루션이 진정으로 올바르다는 것을 알 수 있습니다. 이것은 마치 모든 컴퓨터 탐정에게 작업을 재검토하는 신뢰할 수 있는 파트너를 붙여주어, 우리가 생사가 달린 결정에 이 기계들을 의지할 때 완전히 믿을 수 있도록 하는 것과 같습니다.