In diffusion auctions, sellers can leverage an underlying social network to broaden participation, thereby increasing their potential revenue. Specifically, sellers can incentivise participants in their auction to diffuse information about the auction through the network. While numerous variants of such auctions have been recently studied in the literature, the formal verification and strategic reasoning perspectives have not been investigated yet.
Our contribution is threefold. First, we introduce a logical formalism that captures the dynamics of diffusion and its strategic dimension. Second, for such a logic, we provide model-checking procedures that allow one to verify properties as the Nash equilibrium, and that pave the way towards checking the existence of sellers' strategies. Third, we establish computational complexity results for the presented algorithms.
논문 ID : 2511.08765제목 : Formal Verification of Diffusion Auctions저자 : Rustam Galimullin (노르웨이 베르겐 대학교), Munyque Mittelmann (프랑스 CNRS, LIPN, 소르본 파리 노르 대학교), Laurent Perrussel (프랑스 IRIT, 툴루즈 카피톨 대학교)분류 : cs.GT (게임 이론), cs.LO (컴퓨터 과학의 논리)발표 시간/학회 : AAAI 2026논문 링크 : https://arxiv.org/abs/2511.08765v1 확산 경매는 판매자가 기저 소셜 네트워크를 활용하여 참여도를 확대함으로써 잠재적 수익을 증가시킬 수 있도록 한다. 구체적으로, 판매자는 경매 참여자들이 네트워크를 통해 경매 정보를 전파하도록 장려할 수 있다. 최근 문헌에서 이러한 경매의 다양한 변형이 연구되었음에도 불구하고, 형식 검증과 전략 추론의 관점은 아직 탐구되지 않았다. 본 논문의 세 가지 주요 기여는 다음과 같다: (1) 확산 동역학 및 그 전략적 차원을 포착하는 논리적 형식화 체계 도입; (2) 내시 균형 등의 성질을 검증할 수 있는 모델 검증 절차 제공 및 판매자 전략 존재성 검증의 길을 개척; (3) 제안된 알고리즘의 계산 복잡도 결과 수립.
전통적인 경매 이론과 메커니즘 설계에서 참여자 집합은 일반적으로 고정되어 있으며, 사회적으로 독립적이다(즉, 에이전트 간의 기저 소셜 네트워크를 고려하지 않음). 그러나 판매자는 구매자의 소셜 네트워크를 활용하여 경매를 홍보할 수 있으며, 더 큰 시장은 더 높은 평가를 가진 참여자를 포함할 수 있어 사회적 복지 또는 판매자 수익을 증가시킬 수 있다.
참여자 장려의 모순 : 구매자는 경쟁자이므로 더 많은 참여자를 초대할 동기가 없다. 왜냐하면 이는 경쟁을 증가시키고 경매 물품 획득 가능성을 낮추기 때문이다.확산 경매 메커니즘 : 구매자에게 이웃 초대로부터 이익을 얻도록 장려함으로써, 메커니즘은 구매자가 경매 정보를 전파한 후의 새로운 효용이 원래 효용 이상임을 보장한다.미탐사 영역 : 다중 판매자 경쟁 시나리오에서의 전략적 행동과 형식 검증은 아직 연구되지 않았다.기존 확산 경매 연구는 주로 단일 판매자 시나리오와 경제적 성질(예: 유인 양립성, 최적성)에 초점을 맞춤 다중 판매자 경쟁 환경에서의 전략적 행동에 대한 형식적 분석 부재 이러한 메커니즘의 성질을 검증하기 위한 체계적인 검증 프레임워크 없음 본 논문은 소셜 네트워크 논리, 동적 인식 논리(DEL), 연합 논리(CL) 및 교대 시간 시간 논리(ATL)의 아이디어를 결합한 확산 경매의 첫 번째 논리 기반 형식 검증 방법이다. 이는 확산 경매의 규범화 및 검증을 위한 강력한 도구를 제공한다.
논리적 형식화 체계 : n개 판매자 확산 장려 논리 Ln 및 그 전략적 변형 SLn을 도입하여 경매 정보 확산의 동역학 및 전략적 차원을 포착통용 메커니즘 모델 : 확산 경매 메커니즘 모델(DAM)을 제안하여 다양한 메커니즘 유형을 포착할 수 있을 정도로 충분히 통용적모델 검증 알고리즘 : Ln과 SLn에 대한 모델 검증 절차 제공, 복잡도는 각각 P와 PSPACE-완전전략 존재성 문제 : 전략 존재성 문제를 형식화하고 해결하여 NP-완전임을 증명표현력 분석 : SLn이 Ln보다 엄격히 더 표현력이 있음을 증명하지만, 유한 메커니즘에서는 동등한 변환 가능다중 판매자 확산 경매에서의 형식 검증 문제를 연구하며, 여기서:
입력 : n개 판매자가 동일 물품의 사본을 판매하고, 소셜 네트워크를 통해 구매자가 연결됨동적 과정 : 판매자는 직접 이웃(구매자)을 장려하여 친구들을 경매에 초대하도록 함목표 : 메커니즘 성질(예: 내시 균형) 검증 및 판매자 전략 존재성 검증구문:
φ := α | (z₁t₁ + ... + zₘtₘ) ≥ z | ¬φ | (φ ∧ φ) | □φ | [σ₁:β₁,...,σₙ:βₙ]φ | ♡γ
핵심 구성:
명칭(Nominals) α ∈ Nom: 특정 에이전트를 지칭선형 부등식 : 효용 관계 표현, 예: ut_α ≥ 3친구 모달리티 □φ: 현재 에이전트의 모든 친구가 φ를 만족동시 확산 모달리티 σ:β φ: 판매자 σᵢ가 구매자 βᵢ를 장려한 후 φ 성립할당 연산자 ♡γ: 에이전트 γ가 물품을 획득연합 모달리티 추가:
⟨[C]⟩φ := 판매자 연합 C가 다른 판매자들의 행동에 관계없이 φ가 성립하도록 하는 전략이 존재
의미론:
M,a ⊨ ⟨[C]⟩φ iff ∃βC∀βS\C: M,a ⊨ ⟨σC:βC⟩⊤ 및 M,a ⊨ [σC∪σS\C:βC∪βS\C]φ
n개 판매자 시장 네트워크 M = (Agt, F, Bdg, V, I, N):
Agt = B ∪ S : 구매자 및 판매자 집합F: Agt → 2^B : 대칭 비반사적 우정 관계Bdg: Agt → Q⁺∪{0} : 각 에이전트의 예산V: B → Q⁺∪{0} : 구매자의 물품에 대한 평가I: B × S → Q⁺∪{0} : 판매자가 구매자에게 지불할 의사가 있는 장려금N : 명칭을 에이전트에 매핑하는 명명 함수M = (M, P, Pay, U):
P: Agt → {0,1} : 할당 함수(누가 물품을 획득하는가)Pay: B → Q⁺∪{0} : 지불 함수U: Agt → Q⁺∪{0} : 효용 함수이러한 함수의 구체적 정의는 고정되지 않아 모델이 통용적이며, 다양한 메커니즘 유형을 수용할 수 있다.
판매자 σᵢ가 구매자 βᵢ를 장려할 때:
σᵢ가 제공한 장려금이 가장 높고 예산이 충분한 경우 βᵢ의 모든 친구가 σᵢ의 경매에 참여: F^Upd(s) = F(s) ∪ {b | b ∈ F(N(βᵢ))} 예산 조정:
Bdg^Upd(s) = Bdg(s) - I(N(βᵢ), s) Bdg^Upd(N(βᵢ)) = Bdg(N(βᵢ)) + I(N(βᵢ), s) 동적 소셜 네트워크 모델링 : DEL의 모델 업데이트 아이디어를 경매 확산에 처음 적용하여 소셜 네트워크 구조가 판매자 행동에 따라 동적으로 변함혼합 논리 기법 : 명칭(nominals)을 사용하여 특정 에이전트를 정확히 지칭하고, "에이전트 α의 효용 증가" 같은 성질 표현 지원동시 장려 작업 : σ₁:β₁,...,σₙ:βₙ 을 통해 다중 판매자의 동시 행동을 모델링하고, •를 사용하여 순차 실행 구현선형 부등식 통합 : 확률 추론 및 자원 제약 인식 논리에서 영감을 받아 효용 및 예산 제약 표현에 사용연합 전략 연산자 : CL/ATL에서 영감을 받았지만 동적 모델에 맞게 조정하여 경쟁 환경에서의 전략 능력 포착논문은 단일 물품 다중 단위 첫 가격(SMF) 경매를 실행 예시로 사용:
할당 함수 정의 :
각 판매자 sᵢ에 대해, 그 경매에 참여하는 구매자의 평가 순서 집합 sᵢ 구성(높은 것부터 낮은 것 순) 집합 정제: sᵢ = sᵢ \ {sⱼ(1) | 0 < j < i}(이미 물품을 획득한 구매자 제거) sᵢ가 비어있지 않으면, 최고 입찰자가 물품 획득: P(a) = 1 for V(a) = sᵢ(1) 지불 및 효용 :
구매자 지불: Pay(a) = V(a) 구매자 효용: U(a) = Bdg(a) - V(a)·P(a) 판매자 효용: U(sᵢ) = V(a) + Bdg(sᵢ)(a는 승자) 판매자 s 예산 5, 구매자 a,b,c,d 평가 각각 1,2,9,10 초기 상태: M,a ⊨ (ut_σ = 7) ∧ ♡β(β 승리, 판매자 효용 7) α 장려 후: M,a ⊨ ⟨α⟩(ut_σ = 9 ∧ ♡γ)(γ 참여 및 승리, 효용 9로 증가) 추가 진행 불가: M,a ⊨ ¬⟨α⟩⟨γ⟩(ut_σ > 9)(예산 부족으로 최부자 도달 불가) 두 판매자 s₁,s₂ 각 예산 1, 6명 구매자 초기: ut_σ₁ = 2 ∧ ut_σ₂ = 2 조정된 확산 σ₁:δ, σ₂:γ : 두 판매자 효용 모두 증가(3과 4) 경쟁 확산 σ₁:α, σ₂:γ : s₁이 α를 장려하여 높은 평가 구매자 b 초대, s₂ 효용 초과 결론 : 다항식 계산 가능한 P, Pay, U 함수를 가진 유한 DAM에 대해, Ln 모델 검증은 P에 속함
증명 개요 (알고리즘 1):
동적 모달리티 σ:β ψ 검사: 판매자가 그 경매의 구매자를 장려하고 예산이 충분한지 검증 최고 장려금을 제공하는 판매자 확인(사전식 순서로 동점 해결) 메커니즘 업데이트: F^(σ:β), Bdg^(σ:β) ψ 재귀적 검증 복잡도 분석: 업데이트 메커니즘 크기 O(|M|²), |φ|번 재귀, 총 다항식 시간 문제 정의 : 유한 메커니즘 M과 목표 φ∈Ln이 주어졌을 때, 유한 동시 장려 수열 ⟨σ:β⟩*이 존재하여 M,s ⊨ ⟨σ:β⟩*φ인가?
결론 : NP-완전
증명 :
NP 상한 : 수열 길이는 예산으로 제한되어 다항식이며, 추측하고 P 시간 내에 검증 가능NP 어려움 : 3-SAT에서 귀약
메커니즘 M_Ψ 구성: 에이전트는 절(bᵢ), 리터럴(cᵢⱼ,ₗ), 원자(dᵢ), 진리값(tᵢ,fᵢ)에 대응 계층 구조: s → bᵢ → cᵢⱼ,ₗ → dᵢ → eᵢⱼ → {tᵢ,fᵢ} 목표 공식 φ_Ψ는 3-SAT 제약 인코딩 장려 수열은 진리값 할당에 대응 결론 1 : 유한 메커니즘 M,a와 φ∈SLn에 대해, ψ∈Ln이 존재하여 M,a ⊨ φ ⟺ M,a ⊨ ψ
변환 : t(⟨C ⟩φ) = ⋁{βC} ⋀ {βS\C} (⟨σC:βC⟩⊤ ∧ σC∪σS\C:βC∪βS\C t(φ))
결론 2 : SLn은 Ln보다 엄격히 더 표현력이 있음(정리 4)
반례 : ⟨σ ⟩♢γ ∈ SL₁은 동등한 Ln 공식이 없음
두 메커니즘 M₁,M₂ 구성, 구매자 β의 장려금 다름(2 vs 1) β가 name(φ)에 없지만 ⟨σ ⟩는 모든 구매자 명칭을 정량화 M₁,s ⊭ ⟨σ ⟩♢γ(예산 부족)이지만 M₂,s ⊨ ⟨σ ⟩♢γ 모든 Ln 공식 φ는 두 메커니즘에서 동일하게 행동 결론 : PSPACE-완전
증명 :
PSPACE 상한 (알고리즘 2):
⟨C ⟩ψ에 대해, 연합 C의 구매자 선택 열거(|B|^|C|가지) 각 선택에 대해, 다른 판매자의 선택 열거(|B|^|S\C|가지) 깊이 우선 탐색, 공간 복잡도 O(|φ|·|M|²) PSPACE 어려움 : QBF에서 귀약
M_Ψ 구성: 2n+1개 에이전트(s, a⁰ᵢ,a¹ᵢ, b⁰ᵢ,b¹ᵢ) a⁰ᵢ,b⁰ᵢ는 pᵢ=거짓 모델링, a¹ᵢ,b¹ᵢ는 pᵢ=참 모델링 공식 φ_Ψ는 양자 교대 인코딩: ⟨σ⟩ 는 ∀에 대응, ⟨σ ⟩는 ∃에 대응 보호 fixed_k는 처음 k개 원자가 할당되었음을 보장 일 단계 내시 균형을 표현 가능:
φ ∧ ⋀ᵢ₌₁ⁿ ⋀_{γ∈Nom_M} ⟨σ₁:β₁,...,σᵢ:γ,...,σₙ:βₙ⟩(ut_σᵢ ≤ mᵢ)
여기서 φ := ⟨σ:β⟩⋀_{1≤i≤n} ut_σᵢ = mᵢ
k 단계 NE로 일반화: 어떤 판매자도 k 단계 내에서 일방적 이탈로 효용을 증가시킬 수 없음을 검증.
SLn의 일부 타당 공식(CL에서 상속):
⟨C ⟩φ → ⟨C∪D ⟩φ(상위 집합은 최소한 동등하게 강력) ⟨∅⟩ φ → ⟨S ⟩φ(공 연합과 전체 연합 관계)⟨C ⟩(φ∧ψ) → ⟨C ⟩φ(두 목표 달성이 단일 목표 달성 함축) 입찰 언어 : OR/XOR 언어는 조합 경매에서 선호도 표현(Nisan 2000)경매 규칙 표현 : 경량 형식화(Mittelmann et al. 2022)반복 경매 전략 : 표현 및 추론(Belardinelli et al. 2022)제한된 합리성 : 경매에서 제한된 합리성 포착(Mittelmann et al. 2021)전략 논리 : 메커니즘 설계 및 합성을 위한 SL 변형 사용(Mittelmann et al. 2023, 2025)
자동 검증 : 경매 프로토콜의 형식 검증(Garg et al. 2025; Caminati et al. 2015)본 논문의 혁신 : 논리 관점에서 경매 확산 동역학을 처음 탐구하며, 에이전트 집합이 고정되지 않음.
DEL : 지식 변화 이벤트 모델링, 본 논문은 모델 업데이트 아이디어 차용소셜 네트워크 논리(SNL) :
정보 확산(Christoff & Hansen 2015; Baltag et al. 2019) 사회적 영향(Christoff et al. 2016) 에코 챔버(Pedersen et al. 2019) 관련 연구 : 소셜 네트워크 상 게시물 가시성 및 전파(Galimullin & Pedersen 2024)혼합 논리 : 명칭을 사용한 에이전트 지칭(Areces & ten Cate 2007)연합 공고 : DEL의 연합 연산자(Ågotnes & van Ditmarsch 2008)
모델 검증 복잡도 PSPACE-완전(Alechina et al. 2021) 동시 게임 : DEL 모달리티를 사용하여 모델을 수정하는 다중 단계 동시 게임(Maubert et al. 2020)모달 논리에 화살표 추가 (Areces et al. 2015)본 논문의 위치 : SNL, DEL, CL/ATL 아이디어를 결합하여 확산 경매 검증에 처음 적용.
확산 경매의 첫 번째 논리 기반 형식 검증 프레임워크 제시 Ln과 SLn은 물품 할당, 효용 변화, 네트워크 국소 성질, 내시 균형 등을 포착 가능 논리는 동적이며, 네트워크 수정 후 성질 검증 가능 모델 검증 복잡도: Ln은 P, SLn은 PSPACE-완전 전략 존재성 문제는 NP-완전 DAM 정의는 통용적이며, 다양한 경매 유형 수용 가능(함수 복잡도가 모델 검증을 초과하지 않는 한) 함수 복잡도 제한 : P, Pay, U의 계산 복잡도가 모델 검증 복잡도를 초과하지 않아야 함Ln은 다항식 시간 계산 가능 필요 SLn은 다항식 공간 계산 가능 필요 VCG의 NP-완전 할당 함수 같은 일부 최적 할당 함수 배제 단일 물품 가정 : 현재 프레임워크는 단일 물품(다중 사본) 경매로 제한완전 정보 : 불완전 정보 및 베이지안 분석 미고려구매자 전략 : 주로 판매자 전략에 초점, 구매자 전략 추론 미충분 탐구유한 예산 가정 : 실제로는 예산이 더 복잡할 수 있음네트워크 구조 : 우정 관계가 대칭이고 고정되어 있다고 가정(확산으로 인한 변화 제외)확률 프레임워크 : 불완전 정보 및 베이지안 분석의 형식 검증(Huang et al. 2025)구매자 전략 : 구매자의 전략적 행동 및 추론 고려공리화 : Ln과 SLn의 완전 공리 체계 탐구다중 물품 경매 : 조합 경매 시나리오로 확장실제 응용 : 실제 소셜 네트워크 데이터에서 검증합성 문제 : 주어진 성질을 만족하는 메커니즘 자동 합성창의성 : 확산 경매 검증에 형식 방법을 처음 적용하여 새로운 연구 방향 개척이론적 깊이 : 완전한 복잡도 분석(P, NP-완전, PSPACE-완전)표현력 분석 : SLn > Ln을 엄격히 증명하고 유한 메커니즘에서 변환 제공모듈식 설계 : Ln은 기본 동역학 포착, SLn은 전략 추론 추가통용 프레임워크 : DAM 정의가 구체적 함수를 고정하지 않아 다양한 메커니즘 적용 가능간결한 구문 : 논리 구성이 직관적이고 복잡한 성질 표현 용이학제 간 융합 : DEL, SNL, CL/ATL 아이디어 성공적 결합동적 네트워크 모델링 : 소셜 네트워크의 동적 변화를 우아하게 처리동시 작업 : •를 통해 동시 및 순차 실행의 통일적 모델링풍부한 실행 예시 제공(단일 판매자, 이중 판매자 경쟁) 사례 분석이 논리 표현 능력을 명확히 시연 내시 균형 등 경제 개념의 형식화가 구체적으로 실행 가능 기술 부록에 모든 정리의 상세 증명 포함 귀약 구성(3-SAT, QBF)이 교육적 가치 있음 알고리즘 의사 코드가 명확하고 구현 가능 경험적 평가 없음 : 실제 또는 합성 데이터에서의 실험 없음확장성 미지 : 대규모 네트워크에서 알고리즘의 실제 성능 불명도구 구현 : 모델 검증기 구현 또는 오픈소스 코드 미제공단일 물품 제약 : 실제 전자상거래 시나리오는 종종 다양한 상품 포함단순화 가정 : 완전 정보, 대칭 우정 등 가정이 과도장려금 모델 : 고정 장려금 값이 충분히 유연하지 않을 수 있음구매자가 장려금을 수동적으로 수용하며 주동적 전략 추론 부재 구매자 간 담합 가능성 미고려 초대 결정이 "모두 초대"로 단순화됨 SLn의 PSPACE-완전 복잡도가 실제 응용 제한 전략 존재성의 NP-완전이 대규모 사례에 부적합 근사 알고리즘 또는 휴리스틱 방법 미탐구 내시 균형 표현 가능하지만 다른 메커니즘 설계 성질 심층 분석 부재 유인 양립성, 개인 합리성 등이 언급만 되고 상세 검증 미흡 경제학 문헌과의 대화 부족 새로운 연구 방향 : 확산 경매의 형식 검증 연구 개척방법론 기여 : 동적 네트워크 상 메커니즘 설계에 논리 방법 적용 방법 시연이론적 기초 : 후속 연구를 위한 견고한 형식적 기초 제공잠재적 응용 : 전자상거래 플랫폼, 소셜 미디어 광고, 바이럴 마케팅검증 도구 : 메커니즘 성질 검증 자동 도구 개발 가능메커니즘 설계 : 설계자에게 규범 언어 및 검증 수단 제공이론 재현성 : 정의 및 증명이 완전하고 명확구현 도전 : 모델 검증기 구현 필요, 작업량 상당데이터 필요 : 소셜 네트워크 데이터 및 경매 매개변수 필요소셜 전자상거래 : 사용자 소셜 관계를 활용한 상품 홍보추천 보상 시스템 : 사용자가 친구 추천으로 보상 획득크라우드펀딩 플랫폼 : 프로젝트가 소셜 네트워크를 통해 전파온라인 광고 : 광고주가 소셜 네트워크 사용자를 놓고 경쟁네트워크 규모 : 중소 규모 네트워크(복잡도 제한으로 인해)단일 물품 시나리오 : 현재 프레임워크 제한완전 정보 : 네트워크 구조 및 평가 알아야 함합리적 에이전트 : 에이전트가 완전히 합리적이라고 가정대규모 네트워크 : 수백만 노드의 소셜 네트워크복잡한 상품 : 다중 속성, 맞춤형 상품동적 평가 : 시간에 따라 변하는 평가불완전 정보 : 에이전트 정보 비대칭Zhao et al. (2018) : 확산 경매의 개척 연구Li et al. (2022) : 확산 경매 설계Pauly (2002) : 연합 논리 기초Alur et al. (2002) : ATL 원본 논문van Ditmarsch et al. (2008) : DEL 교과서Pedersen (2024) : 소셜 네트워크 논리 종합Mittelmann et al. (2023, 2025) : 경매의 전략 논리 검증메커니즘 설계 : Nisan et al. (2007) - Algorithmic Game Theory경매 이론 : Vickrey (1961), Clarke (1971), Groves (1973) - VCG 메커니즘모델 검증 : Clarke et al. (2018) - Handbook of Model Checking소셜 네트워크 : Christoff & Hansen (2015), Baltag et al. (2019)본 논문은 확산 경매 형식 검증의 개척 연구로, Ln과 SLn 논리 체계를 도입하여 이 신흥 분야에 견고한 이론적 기초를 제공한다. 주요 강점은 이론의 완전성, 방법의 통용성, 기술의 혁신성에 있다. 그러나 경험적 평가 부재와 대규모 실제 응용에 대한 고려 부족이 명백한 한계이다. 향후 연구가 실제 데이터 검증, 다중 물품 시나리오로의 확장, 효율적인 근사 알고리즘 개발을 결합한다면 실용적 가치가 크게 증대될 것이다. 전체적으로 이는 메커니즘 설계, 논리학, 소셜 네트워크의 학제 간 연구에 중요한 기여를 한 고품질 이론 논문이다.