💻 computer science

Formal Verification of Minimax Algorithms

이 논문은 Dafny 검증 시스템을 활용하여 알파-베타 가지치기와 전이 테이블을 포함한 미니맥스 검색 알고리즘의 정형 검증을 수행하고, 깊이 제한 검색에 대한 증거 기반 정확성 기준을 제시하여 두 가지 실제 변형 중 하나는 완전한 정형 증명, 다른 하나는 오류 사례를 도출한 연구입니다.

원저자: Wieger Wesselink, Kees Huizing, Huub van de Wetering

게시일 2026-04-23

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Wieger Wesselink, Kees Huizing, Huub van de Wetering

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

체스 엔진의 '정답 찾기'를 수학적으로 증명하다: 미니맥스 알고리즘 검증 이야기

이 논문은 컴퓨터가 체스나 바둑 같은 게임을 할 때, **"어떤 수를 두는 것이 최선인지"**를 계산하는 복잡한 프로그램 (알고리즘) 이 정말로 옳은지를 수학적으로 증명하는 연구입니다.

일반적인 프로그램은 "테스트를 해봤는데 잘 돌아가네?"라고 확인하지만, 이 연구는 **"수학적으로 100% 틀릴 수 없음을 증명했다"**는 것을 목표로 합니다.

1. 배경: 게임 엔진은 왜 위험할까?

게임 AI 는 **'미니맥스 (Minimax)'**라는 알고리즘을 사용합니다.

비유: 여러분이 체스를 둔다고 상상해 보세요. "내가 이 수를 두면 상대는 저 수를 두고, 나는 또 이 수를 두고..."라고 미래의 모든 가능성을 상상하며 최선의 수를 찾습니다.
문제점: 게임의 경우의 수는 너무 많아서 모든 것을 다 볼 수 없습니다. 그래서 AI 는 **"이쪽 길은 이미 실패가 확실하니 아예 안 보자"**라고 잘라내는 **알파 - 베타 가지치기 (Alpha-Beta Pruning)**라는 기술을 씁니다.
또 다른 기술: 같은 상황 (보드 상태) 을 다시 계산하지 않기 위해, **"전에 계산한 결과는 메모리에 저장해 두자"**는 **전위 테이블 (Transposition Table)**을 사용합니다.

이런 기술들은 매우 정교하고 빠르지만, 미세한 실수 하나만 있어도 AI 가 엉뚱한 수를 두거나, 최악의 수를 최선으로 착각할 수 있습니다. 테스트만으로는 이런 숨은 버그를 찾기 어렵습니다.

2. 연구의 핵심: "증거 (Witness)"라는 개념 도입

연구진은 **다프니 (Dafny)**라는 '수학적 증명 도구'를 사용했습니다. 하지만 여기서 가장 중요한 것은 새로운 정확성 기준을 세운 것입니다.

기존의 어려움: 전위 테이블을 쓰면, AI 는 현재 보고 있는 나무 (게임 트리) 가 아니라, 다른 곳에서 계산해 둔 깊은 결과를 가져다 씁니다. 이렇게 되면 "어떤 경로를 통해 이 결과가 나왔는지"가 흐려집니다.
새로운 비유 (증거 나무): 연구진은 이렇게 정의했습니다.

"AI 가 내놓은 답이 맞으려면, 그 답을 정당화할 수 있는 '완벽하게 계산된 작은 나무 (증거)'가 반드시 존재해야 한다."

즉, AI 가 "이 수를 두면 3 점이야!"라고 말했을 때, 그 3 점이 실제로 그 부분의 나무를 모두 다 계산해서 나온 값이어야 한다는 뜻입니다. 만약 계산하지 않은 가지를 건너뛰고 나온 값이라면, 그것은 '증거'가 없는 허위 주장입니다.

3. 두 가지 알고리즘의 대결: 위키백과 vs 마슬랜드

연구진은 두 가지 유명한 알고리즘을 이 기준으로 검증해 보았습니다.

🟢 A. 위키백과 버전 (NegamaxTTW) - 합격

특징: 전위 테이블에 저장된 값을 볼 때, **"이 값이 지금의 상황에서도 확실히 결론을 내줄 수 있는가?"**를 먼저 확인합니다. 만약 확실하지 않으면, 아예 그 값을 무시하고 다시 처음부터 계산합니다.
결과: 완벽하게 증명되었습니다. 이 방식은 너무 보수적이라 속도가 조금 느릴 수 있지만, "증거 나무"가 항상 존재하므로 절대 틀릴 수 없습니다.

🔴 B. 마슬랜드 버전 (NegamaxTTM) - 불합격 (버그 발견)

특징: 전위 테이블의 값을 더 적극적으로 활용합니다. "아까 계산한 값이 3 점이었으니, 지금 계산할 때 최소한 3 점 이상은 될 거야"라고 범위를 좁혀서 계산을 빠르게 끝내려 합니다.
발견된 문제: 연구진은 이 알고리즘이 **어떤 상황에서는 엉뚱한 답을 내놓는다는 구체적인 예시 (반례)**를 찾아냈습니다.
- 상황: AI 가 "이쪽 길은 3 점 이상일 거야 (하한선)"라고 메모리에 적어뒀습니다.
- 실수: 그런데 실제로는 그 길이 1 점인 길이 숨어 있었습니다. 하지만 AI 는 "3 점 이상일 거야"라는 메모리를 믿고, 1 점인 그 길을 아예 보지 않고 넘어갔습니다.
- 결과: AI 는 2 점인 나쁜 수를 최선으로 선택해 버렸습니다. 이 답을 정당화할 수 있는 '증거 나무'는 존재하지 않았습니다.

4. 결론: 왜 이 연구가 중요한가?

수학적 증명: 게임 AI 같은 복잡한 프로그램도 수학적으로 "틀릴 수 없음"을 증명할 수 있음을 보여주었습니다.
숨은 버그 발견: 단순히 "잘 돌아가는 것"이 아니라, **"어떤 조건에서 왜 틀리는지"**를 찾아냈습니다. 마슬랜드 알고리즘은 실전에서도 쓰이지만, 이 연구는 그 알고리즘이 가진 치명적인 논리적 허점을 드러냈습니다.
미래의 길: 이 연구는 AI 가 더 똑똑해지고 (양자 컴퓨팅 등) 더 복잡해질수록, "수학적 증명"이 필수적임을 보여줍니다.

요약

이 논문은 **"게임 AI 가 빠른 계산을 위해 메모리를 쓸 때, 그 결과가 진짜인지 확인하는 새로운 방법 (증거 나무)"**을 개발했습니다. 그리고 그 방법으로 위키백과 버전은 안전하지만, 마슬랜드 버전은 특정 상황에서 엉뚱한 답을 낼 수 있다는 것을 수학적으로 증명해냈습니다.

이는 마치 **"빠른 길로 가려다가 길을 잘못 들지 않았는지, 지도 (증거) 를 다시 한번 확인해야 한다"**는 교훈을 주는 연구입니다.

이 논문은 게임 트리 탐색 알고리즘, 특히 **알파-베타 프루닝 (Alpha-Beta Pruning)**과 **전위 테이블 (Transposition Tables, TT)**을 활용한 최소 - 최대 (Minimax) 및 네가맥스 (Negamax) 알고리즘의 형식적 검증 (Formal Verification) 에 관한 연구입니다. 저자들은 Delft 공과대학교 (TU/e) 의 Wieger Wesselink, Kees Huizing, Huub van de Wetering 이며, Dafny라는 형식 검증 도구를 사용하여 알고리즘의 정확성을 수학적으로 증명했습니다.

다음은 논문의 주요 내용을 기술적으로 요약한 것입니다.

1. 문제 정의 (Problem)

배경: 알파-베타 프루닝과 전위 테이블을 사용하는 최소 - 최대 알고리즘은 체스, 바둑 등 게임 엔진의 핵심 요소로 널리 사용되고 있습니다.
도전 과제: 이러한 알고리즘은 최적화되어 있고 미묘한 논리를 포함하고 있어, 단순한 테스트만으로는 숨겨진 오류를 발견하기 어렵습니다.
특정 난제: **깊이 제한 탐색 (Depth-limited search)**에서 전위 테이블을 사용할 때의 정확성 증명이 특히 어렵습니다.
- 전위 테이블은 다른 깊이와 다른 탐색 창 (search window) 에서 계산된 값을 캐싱합니다.
- 이로 인해 단순한 트리 순회 (tree-traversal) 의미론만으로는 알고리즘의 동작을 설명할 수 없게 되며, 기존 연구들은 주로 깊이 무제한 (depth-unlimited) 환경에 국한되어 있었습니다.
- 전위 테이블의 의미론이 명확히 정의되지 않아, 캐싱된 값이 올바른지 판단하는 기준이 모호했습니다.

2. 방법론 (Methodology)

저자들은 Dafny (선언형 프로그래밍 언어이자 형식 검증기) 를 사용하여 다음과 같은 접근법을 취했습니다.

증거 기반 정확성 기준 (Witness-based Correctness Criterion) 도입:
- 전위 테이블을 사용하는 깊이 제한 탐색의 정확성을 정의하기 위해 새로운 기준을 제안했습니다.
- 알고리즘이 반환한 값이 **어떤 완전히 탐색된 서브트리 (witness, 증인)**의 최소 - 최대 (또는 네가맥스) 값과 일치해야 한다는 개념을 정립했습니다.
- 이 '증인 (witness)'은 전위 테이블을 통해 재사용된 깊이 있는 서브트리를 포함하여, 원래의 잘린 트리 (truncated tree) 를 확장한 구조로 정의됩니다.
- 핵심 조건:
  1. 증인은 원래 트리의 서브트리여야 함.
  2. 원래 트리의 깊이 $d$ 까지 잘린 부분과 동형 (isomorphic) 이어야 함.
  3. 특정 노드의 자식들은 모두 포함되거나 모두 배제되어야 함 (부분 집합은 허용되지 않음).
  4. 알고리즘의 반환값이 이 증인 트리에서의 알파 - 베타 결과와 일치해야 함.
구현 및 검증:
- 위 기준을 바탕으로 두 가지 실제 변형 알고리즘 (NegamaxTTW와 NegamaxTTM) 을 Dafny 로 모델링하고 검증했습니다.
- NegamaxTTW: 위키백과 및 커뮤니티에서 흔히 볼 수 있는 변형.
- NegamaxTTM: Marsland 가 제안한 변형 (최적의 수 best-move 추적을 제거한 버전).

3. 주요 결과 (Results)

A. NegamaxTTW (위키백과 변형) 의 성공적 검증

결과: NegamaxTTW 알고리즘은 제안된 '증거 기반' 정확성 기준을 만족함이 완전히 기계적으로 증명되었습니다.
성과: 이 작업은 알파 - 베타 프루닝과 전위 테이블을 사용한 깊이 제한 네가맥스 검색에 대한 첫 번째 형식적 정확성 증명으로 기록됩니다.
검증 시간: 약 850 줄의 Dafny 코드로 작성되었으며, 표준 워크스테이션에서 약 4 초 내에 검증 완료.

B. NegamaxTTM (Marsland 변형) 의 반례 발견

결과: NegamaxTTM 알고리즘은 제안된 정확성 기준을 위반함이 증명되었습니다.
반례 (Counterexample):
- 전위 테이블에서 **좁은 창 (narrow window)**으로 계산된 하한값 (lower bound) 이, 이후 **더 넓은 창 (wider window)**을 가진 탐색에서 재사용될 때 문제가 발생했습니다.
- 이 재사용으로 인해 탐색 창이 잘못 좁혀져 (premature pruning), 실제로 더 좋은 값을 가진 노드가 탐색되지 않고 잘못된 값이 반환되는 경우가 발생했습니다.
- 구체적으로, 알고리즘이 반환한 값 (예: 2) 을 정당화할 수 있는 유효한 '증인 (witness)' 트리가 존재하지 않음이 확인되었습니다.
원인: Marsland 의 알고리즘은 전위 테이블의 경계값을 사용하여 탐색 창을 동적으로 좁히는 전략을 사용하는데, 이것이 깊이 제한 환경에서 정확성을 해치는 것으로 드러났습니다.

C. 알고리즘 비교 분석

Table Lookup 전략의 차이:
- NegamaxTTW: 전위 테이블의 값이 즉시 컷오프 (cutoff) 를 보장하는 경우에만 검색을 종료하고, 그렇지 않으면 기존 창으로 전체 탐색을 수행합니다. (보수적 접근)
- NegamaxTTM: 전위 테이블의 경계값을 사용하여 탐색 창을 좁히고, 이를 기반으로 검색을 계속합니다. (이 전략이 오류를 유발)
결론: NegamaxTTW 의 더 보수적인 정책이 증인 트리의 존재성을 보장하여 정확성을 유지하는 반면, NegamaxTTM 의 전략은 이를 깨뜨립니다.

4. 기여도 및 의의 (Contributions & Significance)

새로운 정확성 기준의 정립: 깊이 제한 탐색과 전위 테이블을 결합한 알고리즘에 대해, '증거 (witness)'를 기반으로 한 엄밀하고 직관적인 정확성 정의를 처음 제시했습니다. 이는 전위 테이블의 복잡한 의미론을 형식적으로 다룰 수 있는 토대를 마련했습니다.
실무 알고리즘의 검증: 게임 엔진에서 실제로 널리 사용되는 알고리즘 변형들을 대상으로 형식 검증을 수행하여, 위키백과식 구현 (NegamaxTTW) 은 안전하지만 Marsland 의 변형 (NegamaxTTM) 은 특정 조건에서 논리적 결함을 가질 수 있음을 밝혔습니다.
도구로서의 Dafny 입증: 재귀적이고 상태가 있는 (stateful) 복잡한 알고리즘을 검증하는 데 Dafny 가 효과적임을 보여주었습니다. 특히 루프 불변식 (loop invariants) 과 전위 테이블의 불변식을 관리하는 데 있어 자동화 및 수동 증명의 균형을 잘 잡을 수 있음을 입증했습니다.
오픈 소스 및 재현성: 모든 검증 아티팩트 (Dafny 증명, 실행 가능한 Python 구현, 무작위 테스트) 를 GitHub 에 공개하여 연구의 투명성과 재현성을 보장했습니다.

5. 결론 및 향후 과제

이 연구는 게임 트리 탐색 알고리즘의 최적화 기법 (특히 전위 테이블) 을 다룰 때 형식적 검증이 얼마나 중요한지 보여줍니다. NegamaxTTM 의 경우처럼, 미묘한 알고리즘적 차이가 명백한 오류로 이어질 수 있음을 지적했습니다.

향후 연구 방향으로는 SSS*나 MTD(f) 와 같이 전위 테이블 상태의 지속성에 의존하는 다른 탐색 알고리즘으로의 확장, 그리고 NegamaxTTM 과 같은 알고리즘에 적합한 '완화된 (relaxed)' 정확성 기준을 찾는 작업, 그리고 양자 컴퓨팅 환경으로의 확장이 제안되었습니다.