Axiom-Audited Trustworthy Formalization of Game-Theoretic Commitment in Lean

Motivation

• Known: program-equilibrium 이론(Tennenholtz, Kalai et al., Barász et al., Critch, Oesterheld 등)은 바인딩 커밋먼트 장치가 조정 게임에서 협력을 회복시킬 수 있음을 pen-and-paper 방식이나 소스코드 상호 읽기 가정 하에 보여주었으며, Coq/Isabelle 기반 게임이론 기계화(Bagnall et al., Le Roux et al., Pomeret-Coquot et al., Caminati et al.) 및 Lean 4 기반 죄수의 딜레마 형식화(MixedMatched contributors)도 존재한다.
• Gap: 기존 program-equilibrium 이론은 기계 검증되지 않았거나 적대적 소스코드 상호 읽기를 전제하며, 어떤 proof assistant 연구도 커밋먼트 장치 우월성 정리를 기계화한 바 없다. 또한 LLM이 생성한 formal proof의 신뢰성 검증에서 핵심인 foundational axiom footprint와 외부 미증명 신뢰 가정(trust assumption)을 명시적·기계적으로 감사하는 방법론이 부재하다.
• Why: LLM이 Lean, Rocq, Isabelle 등에서 점점 더 많은 증명을 생성함에 따라, 증명 스크립트가 어떤 foundational axiom에 의존하는지, 그리고 어디서 외부의 미증명 신뢰 가정이 개입하는지를 기계적으로 감사하는 것은 AI 생성 및 autoformalized 수학 검증 파이프라인의 신뢰성 확보에 핵심적인 문제이다.
• Approach: 저자는 n명 플레이어를 외부 attestation surface를 통해 매개하는 검증된 handshake wrapper를 Lean 4로 완전히 형식화하고, 빌드타임 axiom 감사 어설션과 TrustedOracle typeclass라는 두 가지 재사용 가능한 신뢰성 확보 기법을 이 사례 연구에서 추출하여 제시한다.

Achievement

Architecture of the verified handshake. Participating players submit attestations to an external trusted attestation surface,

1. 기계 감사된 커밋먼트 정리 형식화: Stag-Hunt-ordered 게임(2인/n인, 대칭/비대칭)에 대해 검증된 wrap 콤비네이터를 통해 attesting Cooperate가 약우월전략이 되고 상호협력이 유일한 파레토 비지배 내쉬균형임을 sorry 없이, 커스텀 axiom 없이 증명했다. 2인 결과는 n인 결과의 기계 검증된 특수화(specialization)로 얻어졌다.
2. 실행 가능한 회귀 테스트로서의 axiom hygiene: #guard_msgs로 감싼 #print axioms 어설션을 통해 56개 선언 전체의 foundational-axiom footprint(kernel+Classical만 사용)를 고정시켜, 어떤 axiom drift도 빌드 실패로 감지되도록 했다.
3. 명시적 신뢰 경계 설계 패턴: 외부 attestation이 의도를 충실히 반영한다는 단일 신뢰 가정을 TrustedOracle typeclass와 명시적 truthfulness predicate로 격리하고, 실제 인스턴스와 의무가 non-vacuous임을 증명하는 non-instance 반례를 함께 제시했다.

How

Architecture of the verified handshake. Participating players submit attestations to an external trusted attestation surface,

• 대칭 2×2 게임(Cooperate/Defect)에서 gcd < gdd < gdc < gcc로 특징지어지는 Stag-Hunt 순서를 정의하고, AsymGame 구조체를 통해 비대칭 게임(행/열 플레이어가 각기 독립적으로 Stag-Hunt-ordered인 별도 payoff matrix를 가짐)으로 일반화
• 각 플레이어가 행동 전에 바인딩 attestation("I will play C")을 게시하고, 모든 attestation이 C에 동의할 때만 wrapper가 실제 행동 C를 실현(그 외에는 D)하도록 하는 검증된 wrap 콤비네이터를 정의
• 2인 케이스(§3)를 먼저 개발한 후 임의의 n인 케이스(§4)로 확장하며, 2인 결과를 n인 결과의 기계 검증된 특수화로 도출
• dominance 증명을 임의의 Stag-Hunt-ordered payoff에 대해 파라미터화하고 oracle-agnostic하게 설계하여, oracle 위협 모델(스마트 컨트랙트, TEE attestation, DID/VC 등)을 증명 내부가 아닌 배포 표면(deployment surface)에서 처리
• mathlib을 유리수 산술, linarith, n-player 개발을 위한 finite-type 지원에만 제한적으로 활용
• #guard_msgs로 감싼 #print axioms 어설션을 빌드 파이프라인에 삽입하여 모든 선언의 axiom footprint를 기계적으로 고정
• TrustedOracle typeclass에 명시적 truthfulness predicate를 정의하고, worked instance와 non-instance 반례를 통해 의무의 non-vacuousness를 입증

Originality

• 커밋먼트 장치 기반 전략적 유인 변환(strategic-incentive transformation)을 기계 검증한 최초의 Lean 4 (혹은 어떤 proof assistant) 연구로, 기존 게임이론 기계화 연구들(Nash 존재성, 고정 메커니즘 등)과 차별화됨
• axiom footprint를 실행 가능한 회귀 테스트로 전환하는 아이디어(#guard_msgs + #print axioms)는 간단하지만 AI 생성 증명 검증 파이프라인에 즉시 이식 가능한 실용적 기여
• 전략 콤비네이터와 oracle 신뢰 가정을 분리 가능한(separately reviewable) 아티팩트로 취급하는 설계 원칙, 그리고 TrustedOracle typeclass를 통한 신뢰 경계의 명시적 격리와 non-instance 반례를 통한 non-vacuousness 입증은 신뢰성 감사 방법론으로서 독창적

Limitation & Further Study

• 단일 신뢰 오라클(single trusted attestation oracle)만을 가정하며, 비잔틴 결함 허용(Byzantine fault-tolerant) 쿼럼 변형은 향후 연구로 남겨둠
• 논문 자체가 워크숍 페이퍼(ICML AI for Math Workshop)로 분량이 제한적이며, 실제 LLM 생성 증명에 대한 적용 사례나 실험적 검증 없이 방법론적 제안과 단일 사례 연구에 그침
• 비협력 프로파일에 대한 weak-equilibrium 관련 언급 일부는 완전히 기계화되지 않고 서술적으로만 제시됨(예: wrapN_weak_nash 외 나머지는 stated rather than separately mechanized)
• 실제 배포 환경(스마트 컨트랙트, TEE, DID/VC)에서의 oracle 구현 및 위협 모델 검증은 형식화 범위 밖으로 남겨져 있어, 이론과 실제 배포 간 격차가 존재

Evaluation

총평: 게임이론적 커밋먼트 정리를 완전히 기계 검증하고 axiom 감사 및 신뢰 경계 명시화라는 실용적이고 이식 가능한 두 방법론을 제시한 견고한 워크숍 페이퍼로, 사례 연구는 작지만 AI 생성 formal proof 신뢰성 검증에 시사하는 바가 크다.