From Dag-Like Proofs to Boolean Circuits in Lean

당신이 모든 조각이 논리적 논증인 거대하고 복잡한 퍼즐을 풀으려 한다고 상상해 보십시오. 컴퓨터 과학과 수학의 세계에서 이것은 "형식 검증(formal verification)"이라고 불립니다. 이는 컴퓨터 프로그램이나 수학적 정리가 숨겨진 버그나 논리적 구멍 없이 절대적으로 정확하다는 것을 증명하는 과정입니다. 이를 위해 수학자들은 "자연 연역(Natural Deduction)"을 사용합니다. 이는 마치 가계도와 비슷하게 보이는, 단계별로 증명을 구축하는 방법입니다. 모든 결론은 이전 단계로부터 가지를 뻗어 나가며, 거대하고 넓게 퍼진 논리의 나무를 만들어냅니다.

하지만 이 증명들이 커질수록, 나무는 거대해지고 무질서해집니다. 동일한 가지가 같은 지점에서 반복해서 자라나는 것처럼 많은 중복이 발생합니다. 이로 인해 증명을 확인하는 작업이 느려지고 어려워집니다. 이를 해결하기 위해 연구자들은 "수평 압축(horizontal compression)"이라는 기술을 사용합니다. 그 거대한 나무를 짓눌러서 동일한 가지들이 하나의 공유된 경로로 합쳐지도록 만든다고 상상해 보십시오. 그 결과물은 더 이상 나무가 아니라 "DAG 유사 유도 구조(DLDS, Dag-Like Derivability Structure)"가 됩니다. 이는 기본적으로 경로가 교차하고 병합될 수 있는 지도이며, 공간을 엄청나게 절약해 줍니다. 하지만 까다로운 점은, 지도가 작아졌다고 해서 읽기 쉬워지는 것은 아니라는 점입니다. 압축된 지도가 여전히 유효한 증명인지 확인하는 것은 마치 엉킨 지하철 노선도 속에서 길을 잃지 않고 단 하나의 경로를 추적하는 것과 같습니다.

여기서 논문의 이야기가 시작됩니다. 저자인 로렌조 사라이바(Lorenzo Saraiva)와 에드워드 헤르만 헤슬러(Edward Hermann Haeusler)는 대담한 질문을 던집니다. "우리는 이 엉킨, 압축된 증명의 지도를 훨씬 더 단순하고 기계적인 것으로 바꿀 수 있을까?" 그들은 이러한 복잡한 논리 구조를 "불리언 회로(Boolean circuits)"로 변환하는 방법을 제안합니다. 불리언 회로를 실리콘 조각이 아니라, 거대하고 딱딱한 격자 형태의 전등 스위치와 전선 뭉치라고 생각하십시오. 경로를 추적하는 대신, 당신은 (잠재적인 경로를 나타내는) 일련의 스위치를 올리고 불빛을 관찰하기만 하면 됩니다. 만약 끝부분의 불빛이 올바른 패턴으로 켜진다면, 그 증명은 유효한 것입니다. 그렇지 않다면, 유효하지 않은 것입니다.

이 논문은 "순수 함축 최소 논리(purely implicational minimal logic)"라고 불리는 특정 유형의 논리에서 이러한 압축된 증명을 위한 회로를 구축하는 방법을 제시합니다. 그들은 임의의 스위치 조작 방식(즉, "경로 할당")에 대해, 이 회로가 해당 경로가 논리 규칙을 따르는지 정확하게 계산한다는 것을 보여줍니다. 그들은 단순히 추측한 것이 아닙니다. 그들은 "Lean"이라는 강력한 컴퓨터 도구를 사용하여 자신들의 회로 구축이 완벽하게 작동한다는 것을 형식적으로 검증된 기계적 증명을 작성했습니다. 이는 마치 로봇이 자신의 설계도를 직접 재검토하는 것과 같습니다. 그들이 모든 경로를 즉시 확인하는 문제를 해결한 것은 아니지만(그것은 너무 어렵습니다), 그들의 회로가 당신이 던져주는 어떤 개별 경로에 대해서도 신뢰할 수 있는 균일한 확인 방법임을 증명했습니다. 이는 미래에 증명 검증을 더 빠르고 새로운 기술, 예를 들어 양자 컴퓨터를 사용하는 문을 열어주며, 복잡한 증명 확인 작업을 깔끔한 '온/오프'의 전기 게임으로 바꾸어 놓았습니다.

주요 발견: 논리를 빛나는 격자로 바꾸기

이 논문의 핵심 성과는 이러한 압축된 증명에 대한 "균일한 불리언 평가(uniform Boolean evaluation)"를 만들어낸 것입니다. 저자들은 DLDS(압축된 증명 지도)가 작동하는 복잡한 규칙들을 가져와 고정된 논리 게이트 격자로 번역했습니다.

증명을 도시 격자라고 상상해 보십시오. 기존 방식에서는 경로가 유효한지 확인하려면 모든 교차로를 지나다니며 교통 신호가 제대로 작동하는지 일일이 확인해야 했습니다. 이는 느렸고, 그 특정 도시의 레이아웃에 전적으로 의존했습니다. 저자들의 새로운 방법은 모든 가능한 교차로가 잠재적인 "셀(cell)"로서 존재하는 거대하고 사전 제작된 격자를 구축합니다. 당신은 도시를 걷는 대신, "이 특정 거리들의 불을 켜고 나머지는 무시하라"는 지침(경로 할당)을 격자에 전달합니다.

그 후 회로는 거대한 자동 검사기 역할을 합니다. 회로는 두 가지 주요 사항을 확인합니다:

1. 경로가 잘 형성되었는가? 유효한 논리 단계(예: 함축 도입 또는 제거)의 순서를 선택했습니까? 만약 아무 곳에도 연결되지 않는 무작위한 거리를 선택했다면, 회로는 "무효(Invalid)"라고 표시합니다.
2. 가정이 해소되었는가? 논리에서, 당신은 종종 임시 가정(예: "X가 참이라고 가정하자")에서 시작합니다. 유효한 증명은 결국 X가 더 이상 중요하지 않음을 증명해야 합니다. 회로는 어떤 가정이 여전히 활성화되어 있는지를 나타내는 "의존 비트 문자열(dependency bitstring)"—즉, 불빛의 문자열—을 추적합니다. 만약 경로의 맨 끝에서 모든 불이 꺼져 있다면(즉, 남겨진 가정이 없다면), 회로는 "승인(Accepted)"이라고 말합니다나.

논문은 당신이 선택한 어떤 특정 경로에 대해서도 이 회로가 완벽하게 작동함을 증명합니다. 그들은 이를 "지점별 정확성(pointwise correctness)"이라고 부릅니다. 이는 만약 당신이 특정 스위치 조작을 제공한다면, 회로가 그 특정 경로에 대해 진실을 말해줄 것임을 의미합니다.

이 논문이 배제하고 명확히 한 것

저자들이 매우 주의 깊게 다루었듯이, 이 논문이 주장 하지 않는 바를 이해하는 것이 매우 중요합니다. 그들은 이 방법이 전통적인 의미에서 전체 증명을 확인하는 속도를 높여주지는 않는다고 명시적으로 밝히고 있습니다.

"전역적(global)" 조건—모든 가능한 경로에 대해 증명이 유효한지 확인하는 것—은 여전히 믿기 힘들 정도로 어렵습니다. 논문은 가능한 경로의 수가 지수적으로 증가함(증명이 커짐에 따라 매우 빠르게 증가함)을 언급합니다. 회로가 이 거대한 계산을 마법처럼 즉시 해결해 주는 것은 아닙니다. 대신, 저자들은 문제를 재정의합니다. 회로는 개별 경로를 확인하기 위한 도구이며, 전체 증명의 "유효성"은 그중 모든 경로가 검사를 통과한다는 사실로 정의됩니다.

또한 그들은 기존의 단계별 검증을 위한 "Flow" 함수(이러한 증명을 확인하는 표준 방식)를 개선한다고 주장하는 것도 아님을 명확히 합니다. 진짜 가치는 현재의 확인 과정을 더 빠르게 만드는 데 있는 것이 아니라, 확인의 형식을 바꾸는 데 있습니다. 증명을 불리언 함수(거대한 온/오프 기계)로 변환함으로써, 그들은 양자 컴퓨팅 기술과 같이 이 거대한 "모든 경로" 검사를 전통적인 컴퓨터가 할 수 없는 방식으로 처리할 수 있는 새로운 검증 방법의 문을 열어줍니다.

얼마나 확신하는가?

저자들은 매우 확신하고 있지만, 매우 구체적이고 엄격한 방식으로 그렇습니다. 그들은 단순히 컴퓨터로 시뮬레이션을 돌리거나 작동할 것이라고 추측한 것이 아닙니다. 그들은 형식적으로 증명했습니다.

Lean 증명 보조 도구를 사용하여, 그들은 전체 구조에 대한 기계 검증된 증명을 작성했습니다. 이는 컴퓨터가 그들의 수학적 증명을 한 줄 한 줄 읽고 논리적 공백이 없음을 확인했음을 의미합니다.

• 증명됨: "지점별 정확성"은 수학적 사실입니다. 고정된 경로에 대해 회로는 논리가 요구하는 대로 정확히 작동합니다.
• 증명됨 (한계 포함): 그들은 이 회로를 원래의 증명 구조와 다시 연결하는 "가교"를 증명했지만, 이는 "압축되지 않은 단순 트리 파편(uncompressed simple-tree fragment)"이라는 특정하고 더 단순한 유형의 증명에 대해서만 해당됩니다.
• 향후 과제: 그들은 "조상 엣지(ancestor edges)"와 재귀적 흐름 조건을 포함하는 완전히 압축된 복잡한 경우에 대해서는 아직 이 가교를 증명하지 못했음을 인정하며, 이를 향후 연구 과제로 남겨두었습니다.

"빛나는" 비유의 실제 적용

이를 시각화하기 위해, 격자 형태로 배열된 수천 개의 작은 전구가 있는 거대하고 투명한 판을 상상해 보십시오. 각 행은 증명의 단계를 나타내고, 각 열은 서로 다른 논리적 공식(formula)을 나타냅니다.

• 입력: 당신에게는 긴 버튼 목록이 있는 리모컨이 있습니다. 각 버튼 누름은 다음 행과 행 사이의 어떤 "전선"을 밝힐지 보드에 알려줍니다. 이것이 당신의 "경로 할당"입니다. 보드는 당신의 경로 할당에 따라 움직입니다.
• 회로: 보드 내부에는 작은 논리 게이트들이 있습니다. 만약 당신이 "전제 A"를 "전제 B"에 연결하여 "결론"을 형성하는 전선을 밝힌다면, 게이트는 다음과 같이 확인합니다: "이것이 논리 규칙과 일치하는가?" 만 만약 당신이 서로 맞지 않는 두 가지를 연결하려고 한다면, 게이트는 어두운 상태를 유지하거나 빨간색 오류 불빛을 깜빡입니다.
• 출력: 보드의 맨 아래에는 단 하나의 "목표(Goal)" 불빛이 있습니다. 만약 당신이 모든 규칙을 따르고 모든 임시 가정을 성공적으로 "해소(discharge)"하는 경로를 추적했다면, 목표 불빛은 초록색으로 변합니다. 만약 단계를 놓쳤거나 가정을 남겨두었다면, 불빛은 빨간색 상태를 유지합니다.

이 논문의 돌파구는 어떤 압축된 증문에 대해서도 이 보드를 만들 수 있으며, 빛이 어떻게 행동하는지에 대한 규칙은 증명이 아무리 복잡하더라도 항상 동일하다는 것을 보여준 데 있습니다. 이는 추상적이고 무질서한 논리적 연역의 기술을 스위치를 올리고 불빛을 관찰하는 구체적이고 기계적인 과정으로 바꾸어 놓습니다.

이것이 왜 중요한가

이것이 순수하게 이론적인 연습처럼 들릴 수 있지만, 현대 컴퓨팅의 미래에 큰 시사점을 가집니다. 증명을 불리언 회로로 변환함으로써, 저자들은 현대 하드웨어의 모국어로 말하고 있는 것입니다. 이는 양자 컴퓨터와 같은 고급 기술을 사용하여 증명을 검증하는 것을 가능하게 합니다.

결론에서 저자들은 우리가 "진폭 증폭(amplitude amplification)"(양자 기술)을 사용하여 거대한 모든 경로의 공간을 탐색하여 유효한 경로를 찾거나, 유효하지 않은 경로가 존재하지 않음을 증명할 수 있는 미래를 암시합니다. 또한 그들은 이것이 컴퓨터가 스스로 복잡한 수학적 문제에 대한 증명을 찾아내는 자동 정리 증명(automated theorem proving)에도 도움이 될 수 있다고 언급합니다.

논문은 비록 우리가 기초(회로와 단순 사례에 대한 정확성 증명)를 세웠지만, 완성된 집(복잡하고 압축된 사례)은 여전히 건설 중임을 인정하며 끝을 맺습니다. 그러나 그들은 건설자들에게 기계에 의해 검증된 완벽한 설계도를 건네주었으며, 엉킨 논리의 그물을 깔끔한 전기 격자로 바꾸는 방법을 정확히 보여주었습니다.