정형 기법을 통한 최적의 Caverna 플레이

2026년 2월 21일 · 태그: formal-methods, humor, game-theory, lean, formal · 원문 · 한국어 번역(원문에서 변경됨)

저는 Caverna(Uwe Rosenberg의 고전적인 유럽식 일꾼 놓기 테이블탑 보드게임)에서 항상 이깁니다. 항상 말입니다. 하지만 “항상“이라는 말은 “지금까지는 매번“이라는 뜻일 뿐이므로, 저에게는 수학적으로 더 영속적인 무언가가 필요했습니다. 그래서 저는 게임 전체를 Lean 4로 형식화했고, 가능한 모든 게임 구성에서 제 전략이 유일한 약우월 순수 전략임을 증명했습니다. 제 친구들은 이것이 지나치다고 생각합니다. 제 친구들은 Caverna에서도 집니다. 이와는 관계없는 이야기이지만, 저는 요즘 보드게임 모임에 별로 초대받지 못합니다.

Caverna: The Cave Farmers는 Agricola의 2013년 후속작으로, 동굴에 살면서 수상할 정도로 농사를 많이 짓는 드워프들을 먹여 살리는 게임입니다. 일꾼을 놓고, 자원을 모으고, 동물을 번식시키고, 동굴을 파고, 방에 설비를 들이고 나면, 12라운드가 끝날 때 점수 공식이 여러분이 이룬 모든 것과 이루지 못한 모든 것을 합산합니다. 좋은 게임입니다. 또한 2인 변형 규칙에서는 이산적인 단계를 가진 유한하고 결정론적인 완전 정보 시스템이기도 합니다. 이는 곧 레이블 전이 시스템이라는 뜻이고, 이는 곧 형식 검증이 가능하다는 뜻입니다. 그래서 저는 그렇게 했습니다.

여기에는 아주 작은 수학적 모델이 있습니다. 우리는 두 가지만 정의합니다. 하나는 시작 상태를 기술하는 init 술어이고, 다른 하나는 상태에서 상태로 가는 모든 합법적인 수를 기술하는 trans 관계입니다. 그런 다음 게임을 실행하는 대신 구조적 귀납법으로 게임의 성질을 증명합니다. 그 성질이 시작 시점에 성립함을 보이고, 모든 합법적인 전이가 그 성질을 보존함을 보이면, 게임을 하나도 열거하지 않고도 가능한 모든 게임을 다룬 것이 됩니다. 이는 하드웨어 검증과 프로토콜 증명에 쓰이는 것과 같은 기법을 보드게임에 적용한 것입니다.

이 프로젝트는 19개의 모듈에 걸친 약 3,000줄의 Lean 4 코드로 이루어져 있습니다. 게임 전체를 모델링하는 정의 파일 11개(24개의 행동 칸 전부, 48개의 고유한 가구 타일 전부, 원정 전리품 시스템, 보드 기하 구조, 수확 일정, 점수 계산 공식)와 기계로 검증된 증명 176개를 담은 정리 파일 8개입니다. 이 모델은 가능한 2,880가지의 2인 게임 설정(카드 순서 144가지 곱하기 수확 마커 배치 20가지)을 모두 다룹니다.

주요 결과는 설비 러시가 약우월 전략이라는 것입니다. 어떤 카드가 언제 나오든, 수확 마커가 어디에 놓이든 상관없이, 모든 설정에서 모든 상대에 대한 최적 대응입니다.

대화형 증명 청사진에는 모든 정리가 어떻게 연결되는지 보여 주는 의존성 그래프와 함께 전체 유도 과정이 담겨 있습니다. 소스 코드는 컴파일됩니다.

레이블 전이 시스템

레이블 전이 시스템(LTS)은 세 쌍 $(S, A, T)$ 입니다. 여기서 $S$ 는 상태의 집합이고, $A$ 는 행동의 집합이며, $T \subseteq S \times A \times S$ 는 어떤 상태 변화가 합법적인지를 지정하는 전이 관계입니다. init 술어를 만족하는 어떤 초기 상태에서 시작합니다. 시스템은 행동을 취하면서 진행됩니다. $(s, a, s^{'}) \in T$ 이면 행동 $a$ 를 수행하여 상태 $s$ 에서 상태 $s^{'}$ 로 이동할 수 있습니다. 초기 상태에서 어떤 상태까지 이어지는 유한한 전이의 사슬이 있으면 그 상태는 도달 가능합니다. 어떤 성질이 도달 가능한 모든 상태에서 성립하면 그 성질은 불변식입니다.

Lean 4에서 LTS는 세 개의 필드로 이루어집니다:

structure LTS (State : Type) (Action : Type) where
  init : State -> Prop
  trans : State -> Action -> State -> Prop

도달 가능성은 두 개의 생성자를 가진 귀납 타입입니다. 초기 상태는 도달 가능하며, $s$ 에 도달할 수 있고 행동 $a$ 를 취해 $s^{'}$ 에 갈 수 있다면 $s^{'}$ 도 도달 가능합니다:

inductive Reachable (sys : LTS State Action) : State -> Prop where
  | init : forall s, sys.init s -> Reachable sys s
  | step : forall s a s', Reachable sys s -> sys.trans s a s' -> Reachable sys s'

쉽게 말하면, LTS는 상태 전이 관계로 인코딩된 규칙서입니다. init은 시작 보드가 어떤 모습인지를 나타내고, trans는 모든 합법적인 수를 상태 간 제약으로 인코딩합니다. Caverna 규칙서 전체가 약 250줄의 Lean 코드에 들어갑니다. 24개의 행동 칸 전부와 그 효과를 매칭하는 160줄짜리 applyPlacement 함수, 그리고 페이즈 전이, 수확 로직, 라운드 진행을 연결하는 90줄짜리 cavernaLTS 정의로 구성됩니다. 이것이 함수가 아니라 관계인 이유는 Caverna에서 행동 안에 하위 선택(곡식 파종 대 채소 파종, 어떤 가구 타일을 설치할지, 어떤 전리품을 가져갈지)이 있어서, 하나의 행동 칸 배치가 여러 후속 상태로 이어질 수 있기 때문입니다. 관계는 그 모든 상태를 포착합니다.

init과 trans가 있으면, 도달 가능한 모든 상태를 열거하지 않고도 어떤 속성이 그 모든 상태에서 성립함을 증명할 수 있습니다. 기저 사례(초기 상태에서 성립함)와 귀납 단계(모든 유효한 전이가 그 속성을 보존함)를 증명하면 됩니다. 이는 테스트보다 엄밀하게 더 강력합니다. 테스트는 특정한 플레이 순서를 확인합니다. 불변식 증명은 모든 설정에 걸쳐 합법적인 수의 모든 순서를 다루며, 사람이라면 결코 두지 않을 순서까지 포함합니다.

한 라운드의 플레이가 상태 기계로서 어떻게 동작하는지 감을 잡을 수 있도록 Caverna LTS의 작은 일부를 보여 드리겠습니다.

한 라운드 플레이에 대한 게임 상태 기계의 일부

각 상태는 플레이어의 자원과 배치할 남은 드워프를 기록합니다. 전이는 행동 칸 선택에 대응합니다. 초기 행동 칸 13개와 드워프 2명만으로도 단 한 라운드에서 $13 \times 12 = 156$ 가지 배치 순서가 생깁니다. 가족이 늘어나는 12라운드에 걸치면 분기 계수는 천문학적이지만, LTS는 개의치 않습니다. 구조는 유한하며, 그 안의 모든 경로는 불변식 증명으로 다뤄집니다.

전이 관계로서의 게임

보드게임은 자연스러운 LTS 후보입니다. 2인용 Caverna에서 상태는 완전한 게임 구성(라운드 번호, 페이즈, 두 플레이어의 인벤토리, 보드 배치, 사용 가능한 행동 칸)이고, 행동은 드워프 배치와 수확 이벤트이며, 전이 관계는 규칙서를 인코딩합니다.

게임에는 각 라운드 안에서 순환하는 다섯 개의 페이즈가 있습니다.

inductive Phase where
  | placeP1      -- player 1 places a dwarf
  | placeP2      -- player 2 places a dwarf
  | harvest      -- harvest phase (feeding, breeding, fields)
  | roundEnd     -- round cleanup, advance to next round
  | gameOver     -- game has ended

전체 게임 상태는 두 플레이어가 가질 수 있는 모든 것과 보드의 전역 상태를 추적합니다.

structure GState where
  round : Nat
  phase : Phase
  p1 : FullPlayer
  p2 : FullPlayer
  p1IsFirst : Bool
  placementsLeft : Nat
  acc : AccState
  occupiedSpaces : List ActionSpaceId := []
  harvestSchedule : Nat -> HarvestEvent
  wishIsUrgent : Bool := false

전이 관계는 (gs.phase, act)에 대한 match를 가진 하나의 함수입니다. 각 경우는 하나의 게임 규칙입니다. 다음은 플레이어 1의 배치 로직 중 Core 부분입니다:

def cavernaLTS (schedule : Nat -> HarvestEvent) :
    TransitionSystem.LTS GState GameAction where
  init := fun gs => gs = initFullGState schedule
  trans := fun gs act gs' =>
    match gs.phase, act with
    | .placeP1, .place space choice =>
      spaceAvailable gs.round space = true /\
      spaceUnoccupied gs space = true /\
      gs.placementsLeft > 0 /\
      (let (p1', acc') := applyPlacement gs.p1 gs space choice
       let newPlacements := gs.placementsLeft - 1
       let newOccupied := space :: gs.occupiedSpaces
       if newPlacements == 0 then
         gs' = { gs with p1 := p1', acc := acc',
                         phase := .harvest, placementsLeft := 0,
                         occupiedSpaces := newOccupied }
       else
         gs' = { gs with p1 := p1', acc := acc',
                         phase := .placeP2,
                         placementsLeft := newPlacements,
                         occupiedSpaces := newOccupied })
    -- ... Player 2, harvest, round end, game over ...
    | _, _ => False

마지막 줄이 아름답습니다. | _, _ => False는 명시적으로 나열되지 않은 모든 행동이 불법이라는 뜻입니다. 전이 관계는 닫혀 있습니다. 정의되지 않은 동작도, 엣지 케이스도, “규칙에 하면 안 된다고는 안 쓰여 있다“는 주장도 없습니다. match에 없으면 일어나지 않습니다.

applyPlacement 함수는 24개의 행동 칸 전부에 대한 250줄짜리 match이며, 각각은 규칙서에 나온 정확한 효과를 인코딩합니다. 대장간 일은 광석으로 무기를 벼리고 원정을 떠납니다. 자녀 소망은 수용 공간이 있는 주거지가 있을 때만 가족을 늘릴 수 있습니다. 굴착은 돌을 주고 동굴/터널 쌍을 파낼 수 있게 해 줍니다. 모든 하위 선택(곡식 파종 대 채소 파종, 작은 목초지 대 큰 목초지 건설, 어떤 가구 타일을 설치할지)은 ActionChoice 타입의 한 분기입니다.

게임 타임라인

2인용 Caverna의 게임 타임라인

총 12라운드입니다. 초록색 노드는 드워프를 먹여야 하는 수확 라운드입니다. 중요한 분기점은 두 가지입니다. 4라운드의 “Wish for Children“으로 첫 번째 가족 성장(드워프 2명에서 3명으로)이 가능해지고, 8라운드의 “Family Life“로 두 번째 성장(3명에서 최종적으로 5명까지)이 가능해집니다. 매 라운드 새로운 행동 칸이 하나씩 공개되어, 선택할 수 있는 행동이 13개에서 24개로 늘어납니다. 카드가 공개되는 시점과 수확이 닥치는 시점 사이의 상호작용이 전체 전략 분석을 움직이는 시계입니다.

타임라인이 중요한 이유는 다음과 같습니다. 성장 없이는 12라운드 전체에 걸쳐 드워프를 총 44번 배치합니다. 4라운드에 한 번 성장하면 47번이 됩니다. 두 번 모두 성장하면 56번이 됩니다. 가족을 최대한 빨리 늘리면 전체 행동 횟수가 27% 증가하는 셈이며, 행동은 다른 모든 것(점수, 식량, 자원)을 묶는 제약 조건이므로 “성장 없음“과 “두 번 모두 성장” 사이의 12번의 배치 차이는 이 게임에서 가장 중요한 단일 전략 지렛대입니다.

정제 타입: 불법적인 상태를 표현할 수 없게 만들기

이 형식화에서 가장 만족스러운 패턴 중 하나는 의존 타입을 사용해 불법적인 게임 상태를 아예 구성할 수 없게 만드는 것입니다. 무기가 가장 명확한 예입니다. 실제 게임에서 무기 강도는 1부터 14까지입니다. 이를 그냥 Nat으로 모델링하고 아무도 0이나 15를 넘기지 않기를 바랄 수도 있습니다. 아니면 타입 시스템이 제약 조건을 강제하도록 만들 수도 있습니다.

structure Weapon where
  strength : Nat
  h__min : strength >= 1
  h__max : strength <= 14

모든 Weapon 값은 강도가 범위 안에 있다는 증명을 지니고 있습니다. 즉 forgeWeapon은 단조한 강도가 유효하다는 증거를 만들어 내야 하고, upgradeWeapon은 값을 증가시켜도 범위 안에 머문다는 것을 보여야 합니다.

def forgeWeapon (oreSpent : Nat) (h__pos : oreSpent >= 1) : Option Weapon :=
  if h : oreSpent <= maxInitialWeaponStrength then
    some { strength := oreSpent
         , h__min := h__pos
         , h__max := by simp [maxInitialWeaponStrength] at h; omega }
  else
    none

def upgradeWeapon (w : Weapon) : Weapon :=
  if h : w.strength < maxWeaponStrength then
    { strength := w.strength + 1
    , h__min := by omega
    , h__max := by simp [maxWeaponStrength] at h; omega }
  else
    w

by omega 호출은 Lean의 선형 산술 전술로, 증명 의무를 자동으로 해소합니다. w.strength < 14이면 w.strength + 1 <= 14입니다. oreSpent >= 1이면 strength >= 1입니다. 타입 검사기는 이를 컴파일 시점에 검증합니다. 전체 형식화에서 어떤 무기도 강도 0이나 15를 가질 수 없습니다.

같은 패턴이 RoundPlacements에도 나타나는데, 이 타입은 한 라운드 안에서 네 번의 드워프 배치가 모두 서로 다른 행동 칸으로 간다는 증명을 지니고 있습니다.

structure RoundPlacements where
  firstPlayer1  : ActionSpaceId
  secondPlayer1 : ActionSpaceId
  firstPlayer2  : ActionSpaceId
  secondPlayer2 : ActionSpaceId
  h__distinct12 : firstPlayer1 != secondPlayer1
  h__distinct13 : firstPlayer1 != firstPlayer2
  h__distinct14 : firstPlayer1 != secondPlayer2
  h__distinct23 : secondPlayer1 != firstPlayer2
  h__distinct24 : secondPlayer1 != secondPlayer2
  h__distinct34 : firstPlayer2 != secondPlayer2

각 쌍마다 하나씩, 총 여섯 개의 서로 다름 증명이 있습니다. 두 드워프가 같은 행동 칸을 공유하는 RoundPlacements는 말 그대로 구성할 수 없습니다. 게임 규칙이 타입 안에 녹아 있는 것입니다.

무기 시스템

무기 강도 성장 경로

무기는 강도 1부터 8까지로 제련되며(강도만큼의 광석이 소모됩니다), 이후 원정마다 +1씩 성장하여 최대 14에 이릅니다. 파란색 구간은 제련으로 도달할 수 있고, 복숭아색 구간은 원정을 반복해야만 도달할 수 있습니다. 소 전리품은 강도 9에서 해금되므로, 최대치(광석 8개)로 제련하더라도 소를 얻으려면 최소 한 번은 원정을 떠나야 합니다.

전리품 표는 각 항목마다 최소 강도 요구 조건이 있는 귀납적 타입입니다:

def LootItem.minStrength : LootItem -> Nat
  | .allWeaponsPlus1    => 1
  | .dog                => 1
  | .wood               => 1
  | .grain              => 2
  | .sheep              => 2
  | .stone              => 3
  | .donkey             => 3
  | .ore                => 4
  | .wildBoar           => 4
  | .stableFree         => 5
  | .gold2              => 6
  | .furnishCavern      => 7
  | .buildFencesCheap   => 8
  | .cattle             => 9
  | .dwelling           => 10
  | .sow                => 11
  | .breedTwoTypes      => 12
  | .furnishCavernAgain => 14

강도 1에서는 개나 막대기를 전리품으로 얻을 수 있습니다. 강도 14에서는 두 번째 동굴에 무료로 시설을 놓을 수 있습니다. 주요 강도별 전리품 개수는 강도 1에서 3개, 강도 8에서 13개, 강도 14에서 18개입니다. 즉, 5개의 고급 항목(소, 주거지, 파종, 번식, 두 번째 시설)이 원정 반복의 벽 뒤에 잠겨 있습니다. 광석 투자가 그만한 가치가 있는지가 무기 러시 아키타입의 Core 질문이며, 답은 결국 “아니요, 그렇지는 않습니다“로 밝혀집니다.

보편적 식량 위기

Caverna의 모든 전략은 무엇보다 먼저 같은 문제를 해결해야 합니다. 두 플레이어 모두 첫 수확 때 식량 부족에 직면합니다:

식량 변환 네트워크

플레이어 1은 음식 1개로 시작하며 4개가 필요합니다(드워프 2명 곱하기 각 음식 2개). 플레이어 2는 식량 2개로 시작하며 4개가 필요합니다. 부족분은 각각 3과 2입니다. 이는 universal__food__crisis로 증명됩니다:

theorem universal_food_crisis :
    feedingCost 2 0 - startingFoodP1 = 3 /\
    feedingCost 2 0 - startingFoodP2 = 2 := by decide

그 함의(food__crisis__shapes__all__strategies)는 실행 가능한 모든 전략 유형이 처음 몇 번의 행동을 식량 확보에 써야 한다는 것입니다. “먹이기를 건너뛰고 곧장 득점으로 가는” 선택지는 없습니다. 구걸 토큰의 벌점은 개당 $- 3$ 점이며, 정리 absolute__floor__is__neg55는 모든 라운드에 걸쳐 행동을 하나도 하지 않은 플레이어가 $- 55$ 점을 얻는다는 것을 보여 줍니다. 식량 위기는 선택 사항이 아니라 구조적인 것입니다.

식량 변환 네트워크 자체는 교환 비율이 유쾌하게 뒤엉킨 덩어리입니다. 소는 마리당 식량 4개, 멧돼지는 3개, 양은 2개, 곡물은 1개, 채소는 2개를 주며, 금은 $n - 1$ 의 손실 비율로 변환되고(금 1개가 부대 비용으로 낭비됩니다), 루비는 개당 2개 이상의 비상 식량이 됩니다. 그리고 당나귀가 있는데, 당나귀에는 초선형적인 짝 보너스가 있어서 이를 형식화하는 데 민망할 만큼 많은 시간을 들였습니다:

def donkeyFoodValue (n : Nat) : Nat :=
  let pairs := n / 2
  let remainder := n % 2
  pairs * 3 + remainder * 1

theorem donkey__superlinear :
    donkeyFoodValue 2 > donkeyFoodValue 1 + donkeyFoodValue 1 := by decide

당나귀 두 마리를 함께 쓰면 식량 3개가 나오지만, 따로 쓰면 1 + 1 = 2개가 나옵니다. 전체가 부분의 합보다 큽니다. Uwe Rosenberg는 거의 확실히 이것을 집합 함수의 초가법성(super-additivity) 성질로 생각하지는 않았겠지만, 실제로 그것이 맞으며 Lean은 이를 증명할 수 있습니다.

먹이기 연쇄

식량 공급 함수는 생존의 Core 메커니즘입니다. 수확이 닥치면 드워프는 각각 음식 2개를 먹습니다(자녀는 1개를 먹습니다). 식량이 충분하지 않으면 부족분이 자원을 따라 연쇄적으로 처리됩니다. 먼저 식량을 쓰고, 다음으로 곡물을 변환하고(개당 식량 1개), 그다음 채소를 변환하고(개당 식량 2개), 그래도 남는 부족분에 대해서는 구걸 토큰을 받습니다.

def FullPlayer.feed (p : FullPlayer) : FullPlayer :=
  let cost := p.dwarfs * 2 + p.offspring * 1
  if p.food >= cost then
    { p with food := p.food - cost }
  else
    let deficit := cost - p.food
    let p' := { p with food := 0 }
    let grainUsed := min p'.grain deficit
    let p'' := { p' with grain := p'.grain - grainUsed }
    let deficit' := deficit - grainUsed
    let vegUsed := min p''.vegetables (deficit' / 2 + deficit' % 2)
    let vegFood := min (vegUsed * 2) deficit'
    let p''' := { p'' with vegetables := p''.vegetables - vegUsed }
    let deficit'' := deficit' - vegFood
    { p''' with beggingMarkers := p'''.beggingMarkers + deficit'' }

그리고 일반적인 수확은 세 단계를 하나의 우아한 파이프라인으로 합성한 것입니다:

def FullPlayer.normalHarvest (p : FullPlayer) : FullPlayer :=
  p.fieldPhase.feed.breedingPhase

필드 단계에서는 씨를 뿌린 작물을 수확합니다. 먹이기 단계에서는 식량 비용을 지불합니다(또는 구걸 마커가 생깁니다). 번식 단계에서는 두 마리 이상 있는 동물 종류마다 한 마리씩 추가합니다. 순서가 중요합니다. 필드는 먹이기 전에 식량을 생산하고 번식은 그 뒤에 일어나므로, 새로 태어난 동물은 태어난 라운드에 먹이를 줄 필요가 없습니다. Caverna 규칙서 6쪽에 나오는 이 순서 규칙은 함수 합성에 인코딩되어 있습니다.

가구 타일과 BonusContext

게임에는 가구 타일이 48개 있으며, 각 타일에는 자원 비용과 기본 승점이 있고, (일부 타일에는) 최종 보드 상태에 따라 달라지는 게임 종료 보너스 점수 공식이 있습니다. BonusContext 구조체는 가구 타일이 보너스를 계산할 때 살펴볼 수 있는 모든 것을 담습니다.

structure BonusContext where
  stoneInSupply        : Nat := 0
  oreInSupply          : Nat := 0
  sheepCount           : Nat := 0
  cattleCount          : Nat := 0
  numAdjacentDwellings : Nat := 0
  numArmedDwarfs       : Nat := 0
  numDwarfs            : Nat := 0
  rubyCount            : Nat := 0
  grainCount           : Nat := 0
  vegCount             : Nat := 0
  farmAnimalCount      : Nat := 0
  hasAnyWeapon         : Bool := false
  allDwarfsArmed       : Bool := false
  numYellowTagTiles    : Nat := 0

보너스 점수 함수는 타일 ID에 대한 match로, Caverna 부록에 나오는 모든 점수 공식을 구현합니다.

def furnishingBonusPoints (fid : FurnishingId) (ctx : BonusContext) : Nat :=
  match fid with
  | .stoneStorage   => ctx.stoneInSupply
  | .oreStorage     => ctx.oreInSupply / 2
  | .weavingParlor  => ctx.sheepCount / 2
  | .milkingParlor  => ctx.cattleCount
  | .stateParlor    => ctx.numAdjacentDwellings * 4
  | .mainStorage    => ctx.numYellowTagTiles * 2
  | .weaponStorage  => ctx.numArmedDwarfs * 3
  | .suppliesStorage => if ctx.allDwarfsArmed then 8 else 0
  | .broomChamber   => if ctx.numDwarfs >= 6 then 10
                        else if ctx.numDwarfs >= 5 then 5
                        else 0
  | .prayerChamber  => if ctx.hasAnyWeapon then 0 else 8
  | _ => 0

기도실은 특히 고약합니다. 기도실은 공짜로 8점을 주지만, 무기를 가진 드워프가 하나도 없을 때만 그렇습니다. 무기를 하나라도 벼리는 순간 점수는 0으로 떨어집니다. 이 때문에 진짜 전략적 딜레마가 생기며, 이를 형식화하고 증명하면 다음과 같습니다.

theorem prayer__chamber__vs__weapons :
    furnishingBonusPoints .prayerChamber {} = 8 /\
    furnishingBonusPoints .prayerChamber { hasAnyWeapon := true } = 0 :=
  by constructor <;> native_decide

가구 러시 아키타입의 힘은 서로 잘 맞는 보너스 타일을 쌓는 데서 나옵니다. 사무실의 돌출 보너스, 인접한 주거지마다 +4(최대 +16)를 주는 귀빈실, 드워프 수에 따라 +5 또는 +10을 주는 빗자루 창고, +8을 주는 기도실(무기 없음)이 그 예입니다. 이 보너스들은 서로 누적됩니다. 드워프 5명, 인접한 주거지 4개, 무기 없음인 플레이어는 타일 세 개로 보너스 점수 +39점을 얻을 수 있습니다. 가구 러시의 상한선이 가장 높은 이유가 여기에 있습니다.

전략 공간

LTS, 점수 함수, 식량 경제가 갖춰졌으니 다음 질문은 이것입니다. 플레이어가 실제로 따를 수 있는 상위 수준의 계획에는 어떤 것이 있습니까? 전이 관계는 대략 $1 0^{30}$ 가지의 플레이 순서를 정의하지만, 그중 압도적 다수는 말이 되지 않습니다. 1라운드에 (귀한 광석을 써서) 무기를 벼리고도 원정은 한 번도 나가지 않고, 3라운드에 밭에 씨를 뿌리고도 곡식을 한 번도 거두지 않고, 5라운드에 목초지를 만들고도 동물을 한 마리도 들이지 않고, 8라운드에는 아무 이유 없이 시작 플레이어를 가져가는 플레이어를 생각해 봅시다. 이 플레이어는 한 번도 쓰지 않은 무기, 텅 빈 목초지, 곡식이 썩어 가는 밭을 남기고, 구걸 벌점을 빼면 최종 점수가 20점 안팎인 채로 게임을 끝냅니다. LTS는 이 경로도 포함합니다. 불변식 증명도 이 경로에서 성립합니다. 이것은 규칙상 허용되는 플레이 순서이며, 동시에 다섯 살 아이가 행동 칸을 무작위로 골랐을 때 나올 법한 바로 그런 플레이 순서이기도 합니다.

상태 공간의 대부분은 이런 모습입니다. 플레이어가 모든 것에 조금씩 손대면서 어느 것에도 전념하지 않는, 흩어지고 방향 없는 경로들로, 끝내 점수로 바뀌지 않는 자원을 쌓으며 템포와 식량을 줄줄 흘립니다. 행동 칸 그래프를 지나는 일관된 “채널” 몇 개만이 합리적인 상대를 상대로 경쟁력 있는 점수에 이릅니다. 전략 아키타입은 12라운드 게임 전체에 걸쳐 행동 칸을 일관되게 사용하는 패턴입니다. 저는 어떤 행동 칸과 가구 타일이 자연스럽게 함께 묶이는지 살펴서 여덟 가지를 찾아냈습니다. 두 행동이 같은 자원을 두고 경쟁하거나 같은 점수 범주를 열어 준다면, 두 행동은 같은 아키타입에 속합니다. 예를 들어 대장간, 원정, 무기에 의존하는 전리품은 모두 무기 러시 묶음을 이루고, 굴착, 집안일, 보너스 점수를 주는 가구는 가구 러시 묶음을 이룹니다. 분류는 수작업으로 했지만, Lean 증명이 이를 검증합니다. 모든 아키타입의 점수 추정치는 형식화된 게임 규칙에서 도출되며, 지배 관계는 그 결과로 나온 보수 행렬 위에서 기계로 검사됩니다.

inductive StrategyArchetype where
  | furnishingRush
  | weaponRush
  | animalHusbandry
  | miningHeavy
  | balanced
  | peacefulFarming
  | rubyEconomy
  | peacefulCaveEngine

그렇다면 왜 하필 여덟 가지일까요? 그 답은 게임의 득점 채널 구조에 있습니다. 득점 채널이란 행동 칸을 거쳐 자원을 점수로 바꾸는 경로입니다. 가구 채널은 발굴(Excavation)과 가사(Housework)를 거쳐 가구가 놓인 동굴로 이어지고, 무기 채널은 대장장이(Blacksmithing)를 거쳐 원정과 전리품으로 이어지는 식입니다. 득점 채널은 정확히 여섯 가지입니다.

inductive ScoringChannel where
  | furnishing        -- Excavation + Housework -> caverns -> furnishing tiles
  | weaponExpedition  -- Blacksmithing + Adventure -> weapons -> loot
  | agriculture       -- Clearing + Sustenance -> fields -> crops
  | animalBreeding    -- Sheep Farming + Donkey Farming -> pastures -> animals
  | mining            -- Ore/Ruby Mine Construction -> mines
  | economy           -- Starting Player + Ore Trading + Ruby Mining -> gold/rubies

각 아키타입은 하나의 주 채널에 집중하며, 여덟 가지 아키타입이 여섯 채널을 모두 포괄합니다(all__channels__covered). 일부 채널은 공유 자원을 두고 충돌합니다. 무기/원정 채널과 채광 채널은 모두 광석이 필요하고, 가구 채널과 채광 채널은 모두 돌이 필요합니다. channelsConflict 함수는 이러한 긴장 관계를 표현합니다. 한 게임에서 생산적인 행동은 47번이고 각 채널이 경쟁력 있는 점수에 도달하려면 최소 6번의 전용 행동이 필요하므로, 플레이어가 본격적으로 투자할 수 있는 채널은 최대 2개입니다(budget__bounds__channels). 아키타입은 서로 양립할 수 있는 채널 조합 가운데 극대인 것들입니다. 주 채널이 하나인 아키타입 6개에 하이브리드 2개가 더해집니다(하나는 3개 채널에 고르게 분산하는 균형형이고, 다른 하나는 무기를 득점이 아니라 식량 확보에 쓰는 평화로운 동굴 엔진형입니다).

완전성 증명(archetype__channel__surjection)은 모든 채널에 그 채널을 주 채널로 삼는 아키타입이 적어도 하나 있음을 보여 줍니다. 점수를 얻으려면 반드시 어떤 채널을 거쳐야 하며, 모든 채널이 아키타입으로 대표됩니다. 이 분류에서 벗어나는 유효한 전략은 없습니다.

각 아키타입에는 추정 득점 상한(모든 셋업 중 최선의 경우)과 하한(최악의 경우)이 있습니다.

여덟 가지 전략 아키타입의 추정 점수 범위

가구 러시는 상한 140점으로 1위이며, 하한도 60점으로 공동 1위입니다. 무기 러시는 하한은 같지만 상한이 120점에 그칩니다. 나머지 아키타입은 그보다 뒤처집니다. 구간 차트를 보면 지배 관계가 바로 드러납니다. 가구 러시의 막대는 다른 어떤 아키타입보다 오른쪽으로 더 길게 뻗어 있고(상한이 더 높음), 왼쪽 끝점(하한)도 다른 어느 아키타입에 뒤지지 않습니다.

지배 계층

보수 행렬을 만들기 전에 추정 점수만으로도 부분적인 지배 관계를 확립할 수 있습니다. 전략 $s$ 의 상한과 하한이 모두 전략 $t$ 보다 높다면(적어도 하나는 엄격한 부등식일 때), 추정 점수에서 $s$ 가 $t$ 를 지배합니다.

전략 아키타입 간 지배 관계의 부분 순서

녹색 실선 화살표는 추정 점수를 통한 지배(더 높은 상한과 하한)를 나타냅니다. 녹색 점선 화살표는 전체 보수 행렬을 통해서만 확립되는 지배를 나타냅니다. 축산과 채광 중심은 추정 점수로는 비교할 수 없지만(한쪽은 상한이, 다른 쪽은 하한이 더 높음), 보수 행렬에서는 둘 다 가구 러시에게 약하게 지배당합니다.

비교 불가능성은 구성적으로 증명됩니다.

theorem incomparable__strategies__exist :
    not (dominates .miningHeavy .animalHusbandry) /\
    not (dominates .animalHusbandry .miningHeavy) := by decide

보수 행렬

다음 질문은 서로 다른 아키타입을 택했을 수 있는 두 플레이어가 공유 행동 칸을 두고 부딪칠 때 어떤 일이 일어나는가입니다. 이를 $8 \times 8$ 보수 행렬 $M$ 으로 모델링합니다. 여기서 $M_{ij}$ 는 행 플레이어가 아키타입 $i$ 를, 열 플레이어가 아키타입 $j$ 를 플레이할 때 행 플레이어의 추정 점수입니다.

8x8 보수 행렬

녹색 테두리는 Furnishing Rush 행(약우월)을 나타냅니다. 파란색 테두리는 대각선(미러 매치업, 항상 낮은 값)을 강조합니다. 셀 색상의 농도는 보수의 크기를 나타내며, 연한 녹색(55)부터 코랄색(135)까지입니다.

Lean에서 이 행렬은 Fin 8 -> Fin 8 -> Int 형태의 함수이며, 64개 항목이 모두 전략 분석 결과에 따라 하드코딩되어 있습니다.

def payoffMatrix : Fin 8 -> Fin 8 -> Int
  | 0, 0 =>  85 | 0, 1 => 130 | 0, 2 => 135 | 0, 3 => 130
  | 0, 4 => 125 | 0, 5 => 135 | 0, 6 => 135 | 0, 7 => 130
  | 1, 0 =>  80 | 1, 1 =>  75 | 1, 2 => 100 | 1, 3 =>  85
  | 1, 4 =>  95 | 1, 5 => 105 | 1, 6 => 100 | 1, 7 =>  85
  -- ... 48 more entries ...

여기서 “추정“이 무엇을 의미하는지 짚고 넘어가겠습니다. 행렬의 항목은 몬테카를로 시뮬레이션이나 어림짐작이 아니라 형식화된 게임 규칙(점수 함수, 식량 비용, 행동 예산)에서 도출한 것입니다. 하지만 각 아키타입 안에서 가능한 47수 시퀀스를 모두 빠짐없이 풀어 본 것은 아니므로 추정치라고 할 수 있습니다. 이 결과는 얼마나 민감합니까? min__dominance__margin__is__5 정리는 각 열에서 가구 러시 행과 그다음으로 좋은 항목 사이의 최소 격차가 정확히 5점임을 증명합니다(이 격차는 미러 매치업 열에서 나타납니다). 어떤 항목 하나를 5점 미만으로 변동시켜도 우월 관계는 뒤집히지 않습니다. 셀 하나가 10점이나 바뀌더라도 영향을 받는 것은 한 열뿐이며, 전체 결과에는 영향이 없습니다. 내시 균형은 더 민감하지만(대각선에 의존하기 때문입니다), 균형이 바뀌려면 85인 미러 매치업 값이 그다음으로 좋은 대응 값인 80 아래로 떨어져야 합니다. 이후의 증명들은 제시된 행렬 그대로를 대상으로 기계 검증되었으므로, 형식적 보장은 이 항목들을 전제로 할 때 정확합니다.

조건부 보장보다 더 나은 결과를 얻을 수 있습니다. 각 스칼라 항목을 실제 보수를 포함하는 닫힌 구간으로 바꾸십시오. 미러 매치업에는 좁은 범위를 부여합니다(두 플레이어가 같은 계획을 실행하고 경합이 대칭적이므로 점추정치 $\pm 2$ 입니다). 서로 다른 아키타입 간의 매치업에는 더 넓은 범위를 부여합니다(전략 간 상호작용의 불확실성을 반영하여 $\pm 5$ 입니다). 구간 보수 행렬은 다음과 같습니다.

structure PayoffInterval where
  lo : Int
  hi : Int
  valid : lo <= hi

def intervalPayoff : Fin 8 -> Fin 8 -> PayoffInterval
  | 0, 0 => { lo := 83, hi := 87, valid := by omega }   -- mirror: eps=2
  | 0, 1 => { lo := 125, hi := 135, valid := by omega }  -- vs weapon: eps=5
  -- ... 62 more entries ...

강건한 약우월은 다음을 묻습니다. 모든 열과 가구 러시가 아닌 모든 대안에 대해, 가구 러시의 하한이 그 대안의 상한 이상입니까? 그렇다면 가구 러시는 점추정치뿐만 아니라 이 구간 안에 있는 모든 실제 보수 행렬에 대해 우월합니다.

theorem robust_weak_dominance :
    forall (col : Fin 8) (alt : Fin 8), alt != 0 ->
      (intervalPayoff 0 col).lo >= (intervalPayoff alt col).hi := by decide

이 검사를 통과합니다. 가장 빠듯한 셀은 열 0(미러 매치업)으로, 가구 러시 $[83, 87]$ 대 무기 러시 $[77, 83]$ 입니다. 여유는 $83 - 83 = 0$ 으로, 경계에서 약한 동률입니다. 다른 모든 열의 여유는 20 이상입니다(non__mirror__columns__robust). 오차 범위를 1점만 넓혀도 열 0이 실패하며(fragility__column__0), 이를 통해 결과가 정확히 어디에서 가장 취약하고 허용 오차가 얼마인지 알 수 있습니다.

구간 분석으로 강건한 후생 범위도 얻을 수 있습니다. 내시 후생은 $[166, 174]$ 안에, 사회적 최적은 $[200, 220]$ 안에 있습니다. 이기적인 플레이에 가장 유리하고 협력에 가장 불리한 경우에도 사회적 최적은 여전히 내시 후생보다 큽니다(robust__price__of__anarchy). 죄수의 딜레마 구조는 점추정치 때문에 생긴 착시가 아닙니다.

첫 번째 행은 모든 열에서 다른 모든 행보다 크거나 같습니다. 이것이 전부입니다. 이것이 결과의 전부입니다. 게임 이론에서는 이 성질을 약한 우월(weak dominance)이라고 부릅니다. 모든 상대 전략 $o$ 와 모든 대안 전략 $σ$ 에 대해 다음이 성립하면 전략 $σ^{*}$ 는 약한 우월 전략입니다.

$M (σ^{*}, o) \geq M (σ, o)$

Lean 증명은 furnishing__rush__weakly__dominant이며, 정확히 다음을 말합니다.

theorem furnishing_rush_weakly_dominant :
    forall (row : Fin 8) (col : Fin 8),
      payoffMatrix 0 col >= payoffMatrix row col := by decide

모든 상대에 대해, 모든 대안에 대해, 가구 러시의 보수가 크거나 같습니다. 증명은 decide입니다. Lean의 커널이 64개의 칸을 모두 검사합니다. 누구도 제 산술을 믿을 필요가 없습니다.

경합 효과

보수 행렬의 대각선 성분은 비대각선 성분에 비해 항상 낮습니다.

theorem diagonal__always__depressed :
    forall (i : Fin 8), exists (j : Fin 8), j /= i /\
      payoffMatrix i j > payoffMatrix i i := by decide

모든 미러 매치업은 같은 행에 있는 비(非)미러 매치업 중 적어도 하나보다 낮은 점수를 얻습니다. 이것이 경합 효과입니다. 두 플레이어가 같은 전략 유형을 추구하면 같은 행동 칸을 두고 다투게 됩니다. 가구 러시 미러에서는 굴착과 집안일을 두고 경쟁합니다. 무기 러시 미러에서는 대장장이 일을 두고 다툽니다. 채굴 미러에서는 광석 광산 건설을 두고 충돌합니다.

이 게임은 똑같이 하는 것을 벌합니다. 다만 똑같이 한 데 대한 벌(85)이 더 나쁜 것을 고른 데 대한 벌(가구 러시를 고른 상대를 만났을 때 60에서 80)보다 여전히 덜 아플 뿐입니다.

내시 균형과 죄수의 딜레마

약한 우월성으로부터 게임 이론의 결과가 도미노처럼 줄줄이 따라 나옵니다. 최선 응답 함수 $BR : Strategies \to Strategies$ 는 각 상대 전략을 해당 열에서 값을 최대로 만드는 행으로 대응시킵니다. 가구 러시가 모든 열에서 최댓값을 달성하므로, BR은 상수 함수입니다.

$BR (x) = FurnishingRush \forall x$

내시 균형은 결합 최선 응답 대응의 고정점, 즉 $a = BR (b)$ 이고 $b = BR (a)$ 인 쌍 $(a, b)$ 입니다. BR이 상수이므로, 유일한 고정점은 (FurnishingRush, FurnishingRush)입니다. 존재성과 유일성을 세 줄로 보이면 다음과 같습니다.

theorem exactly__one__nash__equilibrium :
    (exists a b, isNashEquilibrium a b) /\
    (forall a b, isNashEquilibrium a b ->
      a = .furnishingRush /\ b = .furnishingRush) :=
  <<.furnishingRush, .furnishingRush, furnishing_mirror_is_nash>,
   furnishing_mirror_unique_nash>

유일성 증명은 64개의 전략 쌍 모두에 대해 경우를 나누고, 그중 하나만 내시 조건을 만족함을 확인하는 방식으로 이루어집니다.

theorem furnishing__mirror__unique__nash :
    forall a b : StrategyArchetype,
      isNashEquilibrium a b ->
        a = .furnishingRush /\ b = .furnishingRush := by
  intro a b h
  have h1 := h.1; have h2 := h.2
  cases a <;> cases b <;> simp_all [bestResponse, isNashEquilibrium]

순수 내시 균형은 정확히 하나뿐이며, 그것은 두 플레이어가 똑같은 행동을 하는 균형입니다. 조금 비극적인 일입니다.

무정부 상태의 대가

내시 균형에서 두 플레이어는 모두 85점을 얻습니다. 만약 두 플레이어가 어떻게든 서로 다른 전략(예를 들어 가구 러시 대 목축)으로 협조할 수 있다면, 합산 후생은 $85 + 85 = 170$ 대신 $135 + 75 = 210$ 이 될 것입니다.

내시 후생 대 사회적 최적

무정부 상태의 대가는 내시 후생에 대한 사회적 최적의 비율입니다.

$PoA = \frac{210}{170} = \frac{21}{17} \approx 1.24$

이기적인 플레이는 사회적 최적의 약 19%를 잃게 합니다. 단순한 산술이므로 Lean 증명은 decide입니다:

theorem price__of__anarchy__ratio :
    socialOptimumValue = 210 /\ nashWelfare = 170 /\
    210 * 17 = 170 * 21 := by decide

우울한 함의는 두 플레이어 모두 상대방이 다른 전략을 쓰기를 바라지만, 어느 쪽도 자신이 손해를 보지 않고서는 일방적으로 이탈할 수 없다는 것입니다. 여러분은 각자 85점에 갇힌 채, 테이블 건너편에서 이 블로그 글을 똑같이 읽은 상대를 바라보게 됩니다.

점수 함수

자연스럽게 떠오르는 질문은 점수가 실제로 어디에 도달할 수 있느냐는 것입니다. 게임 종료 시의 점수 함수는 모든 양수 및 음수 기여를 합산합니다:

def FullPlayer.score (p : FullPlayer) : Int :=
  let animals := (p.dogs + p.sheep + p.donkeys +
                  p.wildBoars + p.cattle : Int)
  let grainPts := (((p.grain + p.fieldsWithGrain * 3) + 1) / 2 : Int)
  let vegPts := ((p.vegetables + p.fieldsWithVeg * 2) : Int)
  let rubyPts := (p.rubies : Int)
  let dwarfPts := ((p.dwarfs + p.offspring) : Int)
  let pasturePts := (p.smallPastures * 2 + p.largePastures * 4 : Int)
  let minePts := (p.oreMines * 3 + p.rubyMines * 4 : Int)
  let goldPts := (p.gold : Int)
  let furnPts := p.furnishings.foldl (fun acc fid =>
    acc + ((furnishingSpec fid).basePoints : Int)) (0 : Int)
  let missingTypes :=
    (if p.sheep == 0 then 1 else 0) + (if p.donkeys == 0 then 1 else 0) +
    (if p.wildBoars == 0 then 1 else 0) + (if p.cattle == 0 then 1 else 0)
  let unusedPenalty := (p.unusedMountain + p.unusedForest : Int)
  let beggingPenalty := (p.beggingMarkers * 3 : Int)
  let missingPenalty := (missingTypes * 2 : Int)
  animals + grainPts + vegPts + rubyPts + dwarfPts + pasturePts +
  minePts + goldPts + furnPts - unusedPenalty - beggingPenalty - missingPenalty

이론적 하한은 $- 55$ 점입니다. 모든 라운드에 걸쳐 행동을 하나도 하지 않은 플레이어는 시작 드워프 두 명으로 +2점, 네 가지 농장 동물 종류를 모두 갖추지 못해 $- 8$ 점, 사용하지 않은 보드 칸 22개로 $- 22$ 점, 그리고 각각 $- 3$ 점인 구걸 마커 9개로 $- 27$ 점을 받습니다. 이론적 상한은 202점이며, 모든 점수 범주의 독립적인 최댓값을 합산하여 계산합니다. 하지만 202점에는 도달할 수 없습니다. 모든 점수 항목이 12라운드에 걸친 똑같은 56번의 드워프 배치를 두고 경쟁하기 때문입니다. 동굴 12개에 시설을 갖추고, 광산 5개를 짓고, 동물 20마리를 번식시키고, 밭 10개에 씨를 뿌리는 일을 동시에 할 수는 없습니다. 행동 예산이 실질적인 제약 조건입니다. 실질적인 상한은 약 140점이며, 경쟁자가 없을 때 시설 러시로 달성할 수 있습니다.

이론적 범위는 195점( $- 55$ 에서 140까지)이지만, $- 55$ 점이라는 하한은 12라운드 동안 말 그대로 아무것도 하지 않아야 하므로 전략적으로 의미가 없습니다. 모든 아키타입에 걸친 실질적인 하한은 약 45점(최악의 설정에서의 평화로운 농사)이며, 따라서 실질적인 범위는 약 95점입니다. 우월 전략 자체의 범위는 80점(60에서 140까지)이며, dominant__strategy__variance로 증명됩니다. 안전 마진(dominant__strategy__safety__margin)은 이론적 하한보다 115점 높지만, 더 의미 있는 수치는 시설 러시의 최악의 경우(60)와 실행 가능한 아키타입 중 가장 나쁜 것의 최악의 경우(45) 사이의 격차입니다: 가장 불리한 설정에서도 올바르게 선택하면 최소 15점을 더 얻습니다.

사기적인 조합

형식화 과정에서 따로 놓고 보면 사기적으로 보이는 조합이 여럿 드러났습니다. 그중 네 가지가 두드러집니다.

맥주 홀은 점수 계산 전에 곡물을 3:2 비율로 금으로 바꿉니다: 곡물 2개마다 금 3개가 됩니다. 맥주 홀이 없으면 곡물 20개는 10점입니다(곡물 공식은 $⌈ n /2 ⌉$ 입니다). 맥주 홀이 있으면 같은 곡물 20개가 금 30개가 됩니다. 이는 기본 곡물 가치에 3배의 배수를 적용하는 것이며, 금은 다른 모든 점수 범주와 중첩됩니다. beer__parlor__max__gold 정리는 beerParlorGold 20 = 30을 증명합니다. 함정은 곡물 20개를 모으는 일입니다: 여러 라운드에 걸쳐 공격적으로 씨를 뿌려야 하며, 이는 동굴을 파는 대신 화전과 생계 행동에 행동을 소모해야 한다는 뜻입니다.

개가 지킬 수 있는 양에는 상한이 없습니다: 한 목초지에 있는 개 $n$ 마리는 양 $n + 1$ 마리를 지킵니다. 개 10마리와 직조실을 쌓으면 단일 타일 조합만으로 51점을 얻을 수 있습니다. 함정은 개 10마리를 얻으려면 대략 6번의 원정 행동이 필요하다는 것이며(개는 힘 1의 전리품이라 얻기는 쉽지만 원정마다 행동 하나를 소모합니다), 그 6번의 행동은 동굴을 짓거나 가족을 늘리는 데 쓰이지 않습니다.

집필실은 돌 2개로 최대 7점의 손실을 막아 줍니다. 이는 점수 범주 전체를 무시해도 된다는 면허처럼 들리고, 실제로도 그렇습니다. 다만 건너뛰게 될 범주(사용하지 않은 칸, 갖추지 못한 가축 종류)는 바로 시설 러시가 자연스럽게 채워 주는 범주입니다. 집필실의 혜택을 가장 많이 보는 플레이어는 큰 벌점이 쌓일 만큼 서툴게 플레이하는 사람들이며, 그 시점에서는 7점이라는 상한 때문에 정말로 방치된 보드에는 거의 흠집도 내지 못합니다.

기도실(Prayer Chamber)이 가장 우아합니다. 자원을 전혀 투자하지 않고도 8점을 주지만, 어떤 드워프든 무기를 단조하는 순간 그 보너스는 사라집니다. prayer__chamber__vs__weapons 정리는 이것이 엄격한 이분법임을 증명합니다. 8점 아니면 0점이며, 그 사이는 없습니다. 이는 진정한 전략적 갈림길(평화로운 플레이 대 원정 플레이)을 만들어 내며, 게임의 나머지 설계는 이 갈림길을 신중하게 유지합니다.

이 중 어느 것도 지배 전략을 무너뜨리지 못합니다. 모든 콤보는 같은 구속 제약에 부딪힙니다. 가족을 최대로 늘렸을 때 총 56번의 행동이라는 제약입니다. 한 점수 범주에서 화려한 숫자를 낼 수는 있지만, 모든 범주를 다 채울 수는 없습니다. 보드 채우기, 가족 늘리기, 가구 시너지에 균형 잡힌 접근을 취하는 기본 가구 러시가 여전히 상한선으로 남습니다. 콤보는 버그가 아니라 기능입니다. 지배 전략을 알고 난 뒤에도 게임을 다시 플레이할 가치가 있게 만드는 것이 바로 콤보입니다. 표준 노선이 막혔을 때 방향을 틀 대안을 주기 때문입니다.

게임은 풀렸는가?

진지한 수학자라면 이것을 “모델의 매개변수가 계산된 것이 아니라 추정된 것이라는 단서가 붙은, 모델에 대한 형식적 분석“이라고 부를 것입니다. 이는 응용 수학, 운영 연구, 메커니즘 설계에서 정당하고 흔한 패턴입니다. 증명은 기계로 검증되었고 빈틈이 없지만, 보수 행렬을 전제로 합니다. 정리들이 말하는 바는 이렇습니다. 보수 행렬이 이와 같다면, 가구 러시는 약지배 전략이고, 내시 균형은 유일하며, 무정부 비용은 21/17입니다. 정리들이 말하지 않는 바는 이렇습니다. 최적으로 플레이한 가구 러시가 최적으로 플레이한 축산 상대를 만났을 때의 실제 기대 점수가 정확히 135점이라는 것입니다. 그 숫자는 게임 트리를 전수 탐색해서 얻은 것이 아니라, 형식화된 행동 경제에서 도출한 추정치입니다.

이 추정치를 얼마나 신뢰해야 할까요? min__dominance__margin__is__5 정리는 가구 러시와 가장 가까운 경쟁 전략 사이의 최소 격차가 5점임을 증명합니다. 추정 방법론의 체계적 편향이 5점 미만이라면(추정치가 실제 플레이에서 쓰이는 것과 같은 점수 함수와 행동 예산으로부터 도출된다는 점을 고려하면 그럴 법합니다), 정성적 결과는 유지됩니다. 행렬의 한 행 전체에 걸쳐 5점 이상의 상관된 변동이 생기면 미러 열에서 약지배가 깨질 수 있지만, 그러려면 방법론이 자기 경합 시나리오에서 가구 러시의 성과를 일관되게 과대평가해야 합니다. 미러 페널티(대각선 밖의 130점 이상 대 85점)가 이미 심한 경합을 모델링하고 있다는 점을 고려하면, 이는 가능성이 낮아 보입니다.

추정 문제를 아예 우회하는 더 강력한 구조적 논증이 있습니다. 각 점수 채널에는 행동당 최대 산출량이 있습니다. 가구는 행동을 행동당 6점으로 점수로 바꾸고(굴착 + 보너스 배수가 붙은 가구 타일), 무기/원정은 4점, 나머지는 모두 3점 이하입니다. ActionAllocation은 37번의 생산적 행동(총 47번의 배치에서 약 ~10번의 식량 의무를 뺀 것)을 6개 채널에 분배합니다. no__better__allocation__exists 정리는 유효한 모든 분배에 대해 총점이 가구를 극대화하는 분배의 상한인 원점수 222점(37 * 6)을 넘을 수 없음을 증명합니다. 가구에서 차선 채널(무기)로 돌린 행동은 하나당 정확히 2점을 잃고, 농업이나 채광으로 돌리면 3점을 잃습니다. 가구 20 + 무기 17이라는 그럴듯한 혼합 분배는 최대 188점을 얻으며, 34점이 부족합니다. 행동 예산을 어떻게 재분배해도 이 격차를 메울 수 없습니다. 행동 경제가 구조적으로 더 나은 전략의 존재를 허용하지 않습니다.

theorem no_better_allocation_exists :
    forall a : ActionAllocation, a.valid ->
      a.rawScore <= furnishingMaxRawScore := by
  intro a h__valid
  simp only [ActionAllocation.rawScore, furnishingMaxRawScore,
             furnishingMaxAllocation, channelYieldPerAction,
             productiveActionsEstimate, totalPlacementsOneGrowthRound4]
  simp only [ActionAllocation.valid, ActionAllocation.totalActions,
             productiveActionsEstimate, totalPlacementsOneGrowthRound4] at h__valid
  omega

증명은 네 줄입니다. 모든 채널 산출량이 최대 6이므로 37번의 행동에 대한 어떤 분배도 최대 37 * 6 = 222점을 얻기 때문에 omega가 증명을 마무리합니다. 이 결과는 보수 행렬과 무관합니다. 이 결과는 점수 규칙과 행동 예산에만 의존하며, 둘 다 규칙서로부터 형식화되었습니다. 모든 보수 추정치가 50점씩 틀렸다 하더라도 이 정리는 여전히 성립합니다. 가구 채널은 행동당 한계 수익이 가장 높고, 유한한 행동 예산 때문에 그 우위는 극복할 수 없기 때문입니다.

아키타입 수준에서는, 그렇습니다, 이 게임은 풀렸습니다. 2인 게임이라면 2,880가지 구성 중 어느 것을 뽑든, 모델은 최적의 순수 전략이 가구 러시라고 말합니다. 이 증명은 특정한 카드 순서나 수확 마커 배치에 의존하지 않습니다. 제가 하지 않은 것은 각각의 구체적인 셋업에 대해 드워프 배치의 정확한 순서를 계산하는 일입니다. 그러려면 대략 $1 0^{30}$ 개의 노드를 가진 게임 트리를 풀어야 합니다. 하지만 실제 플레이에서 중요한 것은 아키타입 수준의 결과입니다. 여러분은 이제 계획을 알고 있습니다. 아키타입 내부의 결정(어느 동굴을 먼저 굴착할지, 어느 가구 타일을 우선할지)은 전략적인 것이 아니라 전술적인 것입니다. 그런 결정은 답을 바꾸지 않습니다.

3인 이상 변형은 여전히 미해결 문제로 남아 있습니다. 보수 행렬은 512개의 항목을 가진 3차 텐서가 되고, 행동 칸 경합은 이진적인 것에서 조합적인 것으로 바뀌며, 순수 지배 결과는 거의 확실히 성립하지 않습니다. 3자 경쟁에서는 가구 타일이 부족해져 혼합 균형이 나올 가능성이 높기 때문입니다. 누군가 그것을 형식화하고 싶다면, 저는 그 증명을 꼭 읽어 보고 싶습니다.

지배 전략을 플레이하십시오

가구 러시를 플레이하십시오. 1라운드부터 4라운드까지 공격적으로 굴착하십시오. 돌출 보너스를 위해 사무실(Office Room)을 일찍 확보하십시오. 주거지당 +4점을 위해 응접실(State Parlor)을 확보하십시오. 드워프를 5명까지 늘리고 +10 보너스를 위해 빗자루 방(Broom Chamber)을 확보하십시오. 상대가 다른 전략을 쓰면, 여러분은 125점에서 135점을 얻고 상대는 60점에서 105점을 얻습니다. 상대도 가구 러시를 플레이하면 두 사람 모두 85점에 그치는데, 이는 협력 최적값인 210점보다는 나쁘지만 어떤 일방적 이탈보다는 낫습니다. 여러분은 테이블에 앉아 둘 다 최대한 빨리 동굴을 굴착하면서, 한 사람이 10점을 희생하면 다른 사람에게 50점을 줄 수 있다는 것을 둘 다 알지만, 아무도 먼저 물러서는 쪽이 되려 하지 않을 것입니다.

동굴 속의 죄수의 딜레마입니다. 우베 로젠베르크(Uwe Rosenberg)는 아마 이것을 의도하지 않았겠지만, 형식적 분석은 그것이 존재한다고 말합니다.

코드는 Mathlib과 함께 Lean 4 v4.28.0 위에 구축되었으며, 24개의 행동 칸 전부, 48개의 가구 타일 전부, 원정 전리품 표 전체, 보드 격자, 그리고 2인 게임의 12라운드 수확 일정 전체를 모델링합니다. 저는 Caverna가 아름답게 디자인된 게임이라고 생각하며, 바로 그렇기 때문에 정형 분석 아래에서도 전략 구조가 이토록 탄탄하게 유지된다는 사실을 발견한 것이 뿌듯했습니다. 잘못 설계된 게임이라면 게임을 지루하게 만드는 자명한 지배 전략이 있을 것입니다. Caverna의 지배 전략에는 미러 매치업에서 19%의 후생 손실이 따릅니다. 이는 상대가 예상치 못한 수를 둘 때 게임이 언제나 더 흥미로워진다는 뜻이고(게임에서든 인생에서든 내시 균형이 재미있는 곳인 경우는 드뭅니다), 이는 실제로 사람들이 항상 지배 전략을 따르지는 않는다는 뜻이며, 이는 곧 게임이 계속 재미있다는 뜻입니다.

알고 보니, 좋은 게임 디자인은 풀려도 끄떡없습니다. 이제 여러분은 최적의 플레이를 알고 있습니다. 그것을 따를지 말지는, 다행히도, 정리가 아닙니다.

Keyboard shortcuts

Stephen Diehl 블로그 한국어 번역