Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

당신이 모든 책이 숫자로 이루어진 거대하고 복잡한 퍼즐인 도서관의 숙련된 기록관이라고 상상해 보십시오. 때때로 당신은 그 아래에 숨겨진 더 단순한 패턴을 찾기 위해 퍼즐의 페이지들을 재배열해야 합니다. 이것이 바로 선형대수학(linear algebra)의 세계입니다. 선형대수학은 숫자 격자(행렬이라고 불리는)를 다루는 수학의 한 분야입니다. 행렬을 정수의 스프레드시트라고 생각할 수 있습니다. 당신이 패턴을 찾기 위해 이름 목록을 알파벳 순으로 정리하는 것처럼, 수학자들은 이 숫자 격자를 '스미스 정규형(Smith Normal Form)'으로 정리하려고 노력합니다. 이는 숫자들이 아래로 내려갈수록 점점 커지며, 각 숫자가 다음 숫자를 완벽하게 나누는, 매우 깔끔하고 대각선 형태를 띤 버전입니다.

하지만 여기 함정이 있습니다. 숫자를 정렬하는 법을 설명하는 것은 쉽지만, 실제로 그 수학적 계산을 수행하는 것은 악몽이 될 수 있습니다. 당신이 숫자를 정리하기 위해 행과 열을 뒤섞는 동안, 내부의 숫자들은 엄청나게 커질 수 있습니다. 이 숫자들이 너무 거대해져서 컴퓨터를 다운시키거나 계산하는 데 백만 년이 걸릴 수도 있습니다. 수십 년 동안 수학자들은 이 격자를 정렬하는 방법(칸난-바켐 알고리즘이라 불리는 방법)을 알고 있었지만, 이 과정이 무한 루프에 빠지지 않을 것이라는 확신과 숫자가 통제 불능으로 커지지 않을 것이라는 확신이 필요했습니다. 이 논문은 단순히 "이것이 작동한다"라고 말하는 것을 넘어, 그것이 작동한다는 것을 증명하는 디지털적이고 깨지지 않는 증명을 구축하고, 이를 수행하는 데 정확히 얼마나 많은 "계산 에너지"가 드는지 측정하는 작업에 발을 들여놓았습니다.

디지털 이중 점검

이 논문에서 워싱턴 대학교의 준 지(Jun-ye Ji)는 정수 행렬을 정렬하는 영리한 레시피인 칸난-바켐 알고로즘을 가져와, Lean 4라는 도구를 사용하여 이를 기계 검증된 증명으로 구축합니다. Lean 4를 수학적 증명의 모든 단계가 논리적으로 완벽하지 않으면 문을 닫아버리는 매우 엄격하고 로봇 같은 사서라고 생각해 보십시오. 만약 당신이 "아마도"라거나 "아마 그럴 것이다"라는 말을 몰래 끼워 넣으려 한다면, 로봇은 문을 쾅 닫아버릴 것입니다. 지는 단순히 코드를 작성한 것이 아니라, 그 코드가 항상 종료되고, 절대 충돌하지 않으며, 매번 정확한 답을 낼 것임을 로봇이 검증하도록 강제했습니다.

목표는 임의의 0이 아닌 정수 정사각형 격자에 대해, 이 알고리즘이 격자를 깔끔한 대각선 형태인 '스미스 정규형'으로 변환하면서 동시에 그곳에 도달하기 위해 수행된 정확한 이동 경로를 추적하는 것을 증명하는 것이었습니다. 결과물은 단순히 "작동한다"는 메모가 아닙니다. 그것은 최종 정렬된 격자, 그곳에 도달하는 '순방향' 맵, 그리고 원래 상태로 되돌아오는 '역방향' 맵을 포함하는 완전하고 검증된 패키지입니다. 이는 마치 보물 지도와 귀환 티켓을 가지고 있는 것과 같으며, 당신이 거대한 숫자의 숲에서 길을 잃지 않도록 로봇이 둘 다 검증한 것과 같습니다.

"피벗" 댄스와 줄어드는 숫자들

알고리즘의 핵심은 **안정화(stabilization)**라고 불리는 댄스입니다. 당신이 지저도한 방을 정리하려고 한다고 상상해 보십시오. 당신은 바닥의 특정 지점(피벗)을 선택하고 그 행과 열에 있는 다른 모든 것들을 사라지게 만들려고 시도합니다. 때때로 수학이 복잡해져서 모든 것을 완벽하게 사라지게 할 수 없을 때가 있습니다. 그런 일이 발생하면, 알고리즘은 포기하는 대신 현재의 피벗을 더 작은 숫자(진약수)로 교체하는 특별한 동작을 수행합니다.

논문은 결정적인 사실을 증명합니다: 이 특별한 동작이 일어날 때마다, 피벗의 비트(이진 크기)는 엄격하게 작아집니다. 이것은 무거운 돌을 가벼운 조약돌로 바꿀 수 있지만, 조약돌을 무거운 돌로 바꿀 수는 없는 게임과 같습니다. 당신은 영원히 작게 만들 수는 없기 때문에(결국 0에 도달하게 됩니다), 이 게임은 반드시 끝나야 합니다. 저자들은 이 "하강"이 보장된다는 것을 증명했으며, 이는 알고리즘이 절대 무한 루프에 빠지지 않을 것임을 의미합니다.

비용 계산하기: "트레이스(Trace)"

이 연구의 가장 흥미로운 부분 중 하나는 비용을 어떻게 계산했느냐 하는 것입니다. 보통 우리가 알고리즘이 "빠르다"고 말할 때, 몇 초 정도 걸릴 것이라고 추측하곤 합니다. 하지만 여기서 저자들은 컴퓨터가 수행한 모든 미세한 수학 연산(덧셈, 곱셈, 나눗셈)을 목록으로 만드는 영수증과 같은 **'플랫 트레이스(flat trace)'**를 만들어, 정확한 산술 비용을 파악하고자 했습니다.

그들은 이 영수증의 총비용이 다항식 비율로 성장함을 증명했습니다. 쉬운 말로, 입력 행렬이 거대해지더라도 이를 해결하는 데 걸리는 시간은 무한대로 폭발하지 않고 예측 가능하고 관리 가능한 방식으로 성장한다는 뜻입니다. 그들은 심지어 이 성장의 구체적인 "차수"까지 계산했습니다. 논문에 따르면, 수행된 작업량에 대한 비용은 차수가 2,150,677인 다항식으로 제한되며, 출력 크기에 대한 비용은 98,990입니다.

이제 이 숫자들은 무시무시하게 커 보이지만, 저자들은 이것이 무엇을 의미하는지 매우 신중하게 설명합니다. 이것들은 "날카로운" 지수(예를 들어 정확히 $n^2$ 단계가 걸린다고 말하는 것)가 아니라 **보수적인 증거(conservative witnesses)**입니다. 이것을 수학 세계의 "1,000톤"이라고 생각하십시오. 만약 당신이 다리를 건설한다면 100톤을 견뎌야 한다고 계산하겠지만, 안전을 위해 1,000톤을 견디도록 설계할 것입니다. 이 거대한 숫자들은 알고리즘이 안전하고 효율적이라는 보장, 즉 실제 성능은 훨씬 더 좋을지라도 이 알고리즘이 안전하다는 것을 보여주는 "1,000톤"입니다.

무엇이 제외되었는가?

이 논문이 하지 않은 일을 아는 것도 중요합니다. 저자들은 증명의 경계를 매우 명확히 했습니다. 그들은 오직 산술 연산(수학 자체)만을 계산했습니다. 컴퓨터가 데이터를 메모리에 로드하는 시간, 결과를 출력하는 시간, 또는 프로그래밍 언 자체의 오버헤드는 계산하지 않았습니다. 또한 이것이 행렬을 정렬하는 가장 빠른 방법이라는 것을 증명한 것도 아닙니다. 그들은 단지 이 특정한 방식이 안전하고, 종료가 보장되며, 계산된 다항식 한계보다 더 많은 자원을 사용하지 않는다는 것을 증명했을 뿐입니다.

최종 판결

그렇다면 결론은 무엇일까요? 이 논문은 **형식 검증(formal verification)**의 승리입니다. 수십 년 된 복잡한 수학적 레시피를 가져와서 로봇에게 모든 단계를 확인하게 합니다. 로봇은 그 레시피가 항상 작동하고, 항상 종료되며, 시스템을 망가뜨릴 정도로 큰 숫자를 만들지 않는다는 것을 확인합니다. 이는 정렬된 행렬, 변환 맵, 그리고 그곳에 도달하기 위해 얼마나 많은 작업이 필요했는지에 대한 수학적으로 증명된 보장을 포함하는 "정확성의 인증서"를 제공합니다.

호기심 많은 십 대에게 이것은, 루빅스 큐브를 푸는 것뿐만 아니라, 큐브가 아무리 뒤섞여 있더라도 절대 갇히지 않고, 큐브를 부수지 않으며, 정해진 횟수 내에 완료할 것임을 증명하는 법적 계약서까지 작성하는 로봇을 만드는 과정을 보는 것과 같습니다. 이것은 수학에서의 "아마도"를 가장 엄격한 판사에 의해 검증된 "확실히"로 바꾸어 놓습니다.