Proving Your Way to Cooperation: Formalizing Proof-Based Open Source Game Theory in Lean

Motivation

• Known: 고전적 game theory는 플레이어를 행동과 신념으로만 표현하며, OSGT는 상호 투명성 하에서 agent가 상대 source code에 대한 bounded proof search를 조건으로 전략을 구성할 수 있게 하여 Prisoner's Dilemma 같은 상황에서 협력을 이끌어낼 수 있음이 이론적으로 알려져 있다(Tennenholtz, 2004; Bárász et al., 2014; Critch et al., 2022).
• Gap: proof-based OSGT는 이론적으로는 풍부하지만 mechanized framework가 전혀 없어 실증적 연구와 실제 AI 시스템으로의 통합이 제한되어 있었고, 기존의 game theory 기계화 시도들은 classical game theory에 국한되어 proof-based OSGT를 다룬 적이 없었다.
• Why: Lean 기반 검증 프레임워크는 proof-based OSGT의 이론적 결과를 실제로 테스트하고 실제 AI 시스템에 통합하며 균형(equilibria)을 수작업 계산보다 훨씬 체계적으로 분석할 수 있게 하여, multi-agent 시스템에서의 강건한 협력(robust cooperation) 연구에 실질적 도구를 제공한다는 점에서 중요하다.
• Approach: 아홉 개의 open-source 프로그램(bot)과 이들의 pairwise play 결과를 규정하는 outcome theorem들을 Lean 4로 수작업 형식화한 뒤, 이 verified library 위에 자연어 전략 설명을 Lean-verified outcome theorem으로 자동 변환하는 retrieve-propose-check 구조의 agentic pipeline을 구축했다.

Achievement

Figure 1. (Top) DupocBot, a canonical Open Source Game

1. 최초의 Lean 4 formalization: proof-based OSGT의 기본 setting(§3.1–3.2, Appendix A)을 형식화하고, DupocBot을 포함한 9개 open-source agent와 이들의 bot-pair matrix에 대한 수작업 machine-checked outcome proof를 제공했다(특히 Critch et al. (2022)의 provability-conditioned construction을 mechanize).
2. Agentic pipeline 구축 및 검증: 자연어 전략 설명을 Lean 프로그램으로 변환하고 pairwise outcome theorem을 증명 시도하는 pipeline(Bot Writer, Proof Writer, Lean Engine)을 만들어, 45개 unordered outcome theorem 중 40개(약 88.9%)를 자율적으로 재증명하는 데 성공했다.
3. Program meta-game의 equilibrium 분석: verified outcome matrix를 이용해 Prisoner's Dilemma에 의해 유도된 program meta-game의 Nash equilibria를 열거했고, 원래 게임에는 없던 폭넓은 스펙트럼의 협력적 equilibria(효율적 payoff를 달성하는 full-cooperation equilibria 포함)를 발견했으며, DupocBot이 완전한 상호 협력이 발생하기 위해 반드시 필요한 유일한 구성 요소임을 규명했다.

How

Figure 1. (Top) DupocBot, a canonical Open Source Game

• Lean 4에서 normal-form game, admissible program, outcome function, program meta-game(Gprog) 등 OSGT의 formal 기반을 정의(§3.1, Appendix A)
• DupocBot과 같이 bounded proof search에 조건화된 program을 포함한 9개 bot을 구현하고, 이들의 모든 pairwise 조합에 대한 outcome theorem을 수작업으로 증명해 verified bot-pair matrix 구성
• agentic pipeline을 retrieve-propose-check 구조로 설계: Bot Writer가 자연어 설명을 읽어 Lean 파일에서 관련 정의를 검색하고 bot 정의를 제안한 뒤 Lean build를 실행, Proof Writer가 동일한 방식으로 outcome proof를 제안하고 Lean kernel로 검증하며 compiler feedback으로 반복 수정
• 파이프라인의 성능을 45개 unordered outcome theorem에 대한 자동 재증명 성공률로 평가(§3.3, Appendix B)
• verified outcome matrix를 기반으로 Prisoner's Dilemma에서 유도된 program meta-game의 Nash equilibria를 열거하는 equilibrium 분석 수행(§4.2, Appendix C)

Originality

• proof-based OSGT 자체를 mechanized formal framework로 구현한 최초의 시도로, 기존 game theory formalization(MixedMatched, 2023 등)이 다루지 않은 영역을 개척함
• 단순 formalization을 넘어, 자연어 전략 설명을 Lean-verified theorem으로 자동 변환하는 agentic pipeline을 결합하여 이론과 실제 검증 가능한 AI 시스템 통합 사이의 다리를 놓음
• 형식적으로 검증된 outcome matrix를 실제 equilibrium enumeration에 활용해 이론적 개념(Program Equilibrium)을 구체적 사례 연구로 실증화함

Limitation & Further Study

• bot library가 9개 프로그램, 45개 pairwise outcome theorem으로 상당히 제한적이어서 일반화 가능성이나 더 복잡한 전략 공간에 대한 확장성이 검증되지 않음
• agentic pipeline이 45개 중 40개만 성공적으로 재증명했으며, 실패한 5개 사례에 대한 원인 분석이나 한계에 대한 상세 논의가 부족해 보임
• admissibility 조건(Σi)을 의도적으로 under-specified 상태로 두었다고 명시하는데, 이는 이론적 유연성을 주지만 실제 구현의 엄밀성 및 재현성에 영향을 줄 수 있음
• 후속 연구로는 더 큰 규모의 bot library 확장, 다양한 underlying game(PD 외의 게임)에 대한 적용, 그리고 pipeline의 실패 사례에 대한 체계적 분석이 필요해 보임

Evaluation

총평: proof-based OSGT를 Lean으로 최초 형식화하고 이를 자동 증명 pipeline 및 equilibrium 분석으로 확장한 참신하고 견고한 연구로, 향후 formal AI safety 및 multi-agent cooperation 연구에 실질적인 도구를 제공할 잠재력이 크다.