Формальная верификация диффузионных аукционов

Основная информация

• ID статьи: 2511.08765
• Название: Formal Verification of Diffusion Auctions
• Авторы: Рустам Галимуллин (Университет Бергена, Норвегия), Мунике Миттельманн (CNRS, LIPN, Университет Сорбонна Париж Север, Франция), Лоран Перруссель (IRIT, Университет Тулузы Капиталь, Франция)
• Классификация: cs.GT (Теория игр), cs.LO (Логика в информатике)
• Дата публикации/конференция: AAAI 2026
• Ссылка на статью: https://arxiv.org/abs/2511.08765v1

Аннотация

Диффузионные аукционы позволяют продавцам использовать базовую социальную сеть для расширения участия и увеличения потенциального дохода. В частности, продавцы могут стимулировать участников аукциона распространять информацию об аукционе через сеть. Несмотря на множество вариантов таких аукционов, изученных в литературе в последние годы, перспектива формальной верификации и стратегического рассуждения остаётся неисследованной. Тройной вклад данной работы включает: (1) введение логической формализации, которая захватывает динамику диффузии и её стратегические аспекты; (2) предоставление процедур проверки моделей, позволяющих верифицировать свойства, такие как равновесие Нэша, и прокладывающих путь к проверке существования стратегий продавца; (3) установление результатов вычислительной сложности предложенных алгоритмов.

Исследовательский контекст и мотивация

Определение проблемы

В традиционной теории аукционов и проектировании механизмов множество участников обычно фиксировано и социально независимо (то есть не учитывается базовая социальная сеть между агентами). Однако продавцы могут использовать социальную сеть покупателей для продвижения аукциона, и более крупный рынок может содержать участников с более высокой оценкой, что увеличивает общественное благосостояние или доход продавца.

Значимость проблемы

1. Противоречие в стимулировании участников: Покупатели как конкуренты не имеют мотивации приглашать больше участников, так как это увеличивает конкуренцию и снижает вероятность получения товара на аукционе
2. Механизмы диффузионных аукционов: Путём предоставления стимулов покупателям получать выгоду от приглашения соседей, механизм гарантирует, что новая полезность покупателя после распространения информации об аукционе не ниже исходной полезности
3. Неисследованная область: Стратегическое поведение и формальная верификация в сценариях конкуренции между несколькими продавцами остаются неизученными

Ограничения существующих подходов

1. Существующие исследования диффузионных аукционов сосредоточены в основном на сценариях с одним продавцом и экономических свойствах (таких как совместимость стимулов, оптимальность)
2. Отсутствует формальный анализ стратегического поведения в конкурентной среде с несколькими продавцами
3. Нет систематической структуры верификации для проверки свойств этих механизмов

Исследовательская мотивация

Данная работа является первым логическим подходом к формальной верификации диффузионных аукционов, объединяющим идеи логики социальных сетей, динамической эпистемической логики (DEL), логики коалиций (CL) и чередующейся временной темпоральной логики (ATL), предоставляя мощные инструменты для спецификации и верификации диффузионных аукционов.

Основные вклады

1. Логическая формализация: Введена логика диффузионных стимулов для n продавцов L_n и её стратегическая вариация SL_n, способная захватывать динамику распространения информации об аукционе и стратегические аспекты
2. Универсальная модель механизма: Предложена модель механизма диффузионного аукциона (DAM), достаточно универсальная для захвата различных типов механизмов
3. Алгоритмы проверки моделей: Предоставлены процедуры проверки моделей для L_n и SL_n со сложностью P и PSPACE-полнота соответственно
4. Проблема существования стратегии: Формализована и решена проблема существования стратегии, доказана её NP-полнота
5. Анализ выразительности: Доказано, что SL_n строго более выразительна, чем L_n, но может быть эквивалентно преобразована на конечных механизмах

Подробное описание методов

Определение задачи

Исследование проблемы формальной верификации в диффузионных аукционах с несколькими продавцами, где:

• Входные данные: n продавцов, продающих копии одного товара, с покупателями, связанными через социальную сеть
• Динамический процесс: Продавцы стимулируют прямых соседей (покупателей) приглашать своих друзей присоединиться к аукциону
• Цель: Верифицировать свойства механизма (такие как равновесие Нэша) и проверить существование стратегий продавца

Проектирование логического языка

Определение языка L_n

Синтаксис:

φ := α | (z₁t₁ + ... + zₘtₘ) ≥ z | ¬φ | (φ ∧ φ) | □φ | [σ₁:β₁,...,σₙ:βₙ]φ | ♡γ

Основные конструкции:

1. Номиналы (Nominals) α ∈ Nom: ссылка на конкретного агента
2. Линейные неравенства: выражение отношений полезности, например ut_α ≥ 3
3. Модальность друзей □φ: все друзья текущего агента удовлетворяют φ
4. Модальность одновременной диффузии σ:βφ: φ выполняется после того, как продавец σᵢ стимулирует покупателя βᵢ
5. Оператор распределения ♡γ: агент γ получает товар

Стратегическое расширение SL_n

Добавлена модальность коалиции:

⟨[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: функция именования, отображающая имена на агентов

Механизм диффузионного аукциона (DAM)

M = (M, P, Pay, U):

• P: Agt → {0,1}: функция распределения (кто получает товар)
• Pay: B → Q⁺∪{0}: функция платежа
• U: Agt → Q⁺∪{0}: функция полезности

Конкретное определение этих функций не фиксировано, что делает модель универсальной и позволяет вмещать различные типы механизмов.

Правила обновления механизма

Когда продавец σᵢ стимулирует покупателя βᵢ:

1. Если стимул σᵢ наибольший и бюджета достаточно
2. Все друзья βᵢ присоединяются к аукциону σᵢ: F^Upd(s) = F(s) ∪ {b | b ∈ F(N(βᵢ))}
3. Корректировка бюджета:
   • Bdg^Upd(s) = Bdg(s) - I(N(βᵢ), s)
   • Bdg^Upd(N(βᵢ)) = Bdg(N(βᵢ)) + I(N(βᵢ), s)

Технические инновации

1. Моделирование динамической социальной сети: Впервые применены идеи обновления моделей из DEL к диффузии аукционов, структура социальной сети динамически изменяется в зависимости от действий продавца
2. Техника гибридной логики: Использование номиналов для точной ссылки на конкретных агентов, поддержка выражения свойств типа "полезность агента α увеличивается"
3. Операции одновременного стимулирования: Моделирование одновременных действий нескольких продавцов через σ₁:β₁,...,σₙ:βₙ, использование • для реализации последовательного выполнения
4. Интеграция линейных неравенств: Заимствование из вероятностного рассуждения и логики с ограниченными ресурсами для выражения ограничений полезности и бюджета
5. Оператор стратегии коалиции: Вдохновлено CL/ATL, но адаптировано к динамической модели для захвата стратегических возможностей в конкурентной среде

Экспериментальная установка

Пример механизма: аукцион SMF

Статья использует аукцион с первой ценой для одного товара нескольких единиц (SMF) в качестве работающего примера:

Определение функции распределения:

1. Для каждого продавца sᵢ построить упорядоченное множество оценок покупателей, участвующих в его аукционе (от высокой к низкой)
2. Уточнить множество: sᵢ = sᵢ \ {sⱼ(1) | 0 < j < i} (удалить покупателей, уже получивших товар)
3. Если sᵢ непусто, покупатель с наибольшей ставкой получает товар: P(a) = 1 для V(a) = sᵢ(1)

Платежи и полезность:

• Платёж покупателя: Pay(a) = V(a)
• Полезность покупателя: U(a) = Bdg(a) - V(a)·P(a)
• Полезность продавца: U(sᵢ) = V(a) + Bdg(sᵢ) (a — победитель)

Анализ случаев

Случай 1: Сценарий с одним продавцом (Рисунок 2)

• Продавец s с бюджетом 5, покупатели a,b,c,d с оценками 1,2,9,10 соответственно
• Исходное состояние: M,a ⊨ (ut_σ = 7) ∧ ♡β (β побеждает, полезность продавца 7)
• После стимулирования α: M,a ⊨ ⟨α⟩(ut_σ = 9 ∧ ♡γ) (γ присоединяется и побеждает, полезность увеличивается до 9)
• Невозможно продолжить: M,a ⊨ ¬⟨α⟩⟨γ⟩(ut_σ > 9) (недостаточно бюджета для достижения самого богатого покупателя)

Случай 2: Конкуренция двух продавцов (Рисунок 3)

• Два продавца s₁,s₂ с бюджетом 1 каждый, 6 покупателей
• Исходное состояние: ut_σ₁ = 2 ∧ ut_σ₂ = 2
• Координированная диффузия σ₁:δ, σ₂:γ: полезность обоих продавцов увеличивается (3 и 4)
• Конкурирующая диффузия σ₁:α, σ₂:γ: s₁ стимулирует α приглашать покупателя с высокой оценкой b, полезность превышает s₂

Результаты экспериментов

Основные результаты сложности

Теорема 1: Сложность проверки моделей L_n

Заключение: Для конечных DAM с полиномиально вычислимыми функциями P, Pay, U проверка моделей L_n находится в P

Идея доказательства (Алгоритм 1):

1. Проверка динамической модальности σ:βψ: верификация того, что продавец стимулирует покупателя в его аукционе и бюджета достаточно
2. Проверка продавца с наибольшим стимулом (лексикографический порядок разрешает ничьи)
3. Обновление механизма: F^(σ:β), Bdg^(σ:β)
4. Рекурсивная проверка ψ
5. Анализ сложности: размер обновлённого механизма O(|M|²), рекурсия |φ| раз, общая полиномиальная временная сложность

Теорема 2: Проблема существования стратегии

Определение проблемы: Дан конечный механизм M и целевая формула φ∈L_n, существует ли конечная последовательность одновременных стимулов ⟨σ:β⟩* такая, что M,s ⊨ ⟨σ:β⟩*φ?

Заключение: NP-полнота

Доказательство:

• Верхняя граница NP: Длина последовательности ограничена бюджетом полиномиально, можно угадать и верифицировать за полиномиальное время
• NP-трудность: Сведение из 3-SAT
  • Построение механизма M_Ψ: агенты соответствуют предложениям (bᵢ), литералам (cᵢⱼ,ₗ), атомам (dᵢ), истинностным значениям (tᵢ,fᵢ)
  • Иерархическая структура: s → bᵢ → cᵢⱼ,ₗ → dᵢ → eᵢⱼ → {tᵢ,fᵢ}
  • Целевая формула φ_Ψ кодирует ограничения 3-SAT
  • Последовательность стимулов соответствует истинностному назначению

Теорема 3: Выразительность SL_n и L_n

Заключение 1: Для конечного механизма M,a и φ∈SL_n существует ψ∈L_n такая, что M,a ⊨ φ ⟺ M,a ⊨ ψ

Преобразование: t(⟨C⟩φ) = ⋁{βC} ⋀{βS\C} (⟨σC:βC⟩⊤ ∧ σC∪σS\C:βC∪βS\Ct(φ))

Заключение 2: SL_n строго более выразительна, чем L_n (Теорема 4)

Контрпример: ⟨σ⟩♢γ ∈ SL₁ не имеет эквивалентной формулы в L_n

• Построение двух механизмов M₁,M₂ с различными стимулами для покупателя β (2 vs 1)
• β не входит в name(φ), но ⟨σ⟩ квантифицирует все имена покупателей
• M₁,s ⊭ ⟨σ⟩♢γ (недостаточно бюджета), но M₂,s ⊨ ⟨σ⟩♢γ
• Любая формула L_n ведёт себя одинаково на обоих механизмах

Теорема 5: Сложность проверки моделей SL_n

Заключение: 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ᵢ=false, a¹ᵢ,b¹ᵢ моделируют pᵢ=true
  • Формула φ_Ψ кодирует чередование кванторов: ⟨σ⟩ соответствует ∀, ⟨σ⟩ соответствует ∃
  • Охрана fixed_k гарантирует, что первые k атомов уже назначены

Верификация равновесия Нэша

Можно выразить одношаговое равновесие Нэша:

φ ∧ ⋀ᵢ₌₁ⁿ ⋀_{γ∈Nom_M} ⟨σ₁:β₁,...,σᵢ:γ,...,σₙ:βₙ⟩(ut_σᵢ ≤ mᵢ)

где φ := ⟨σ:β⟩⋀_{1≤i≤n} ut_σᵢ = mᵢ

Обобщение на k-шаговое NE: верификация того, что ни один продавец не может увеличить полезность путём одностороннего отклонения в течение k шагов.

Валидность

Некоторые валидные формулы SL_n (унаследованные из CL):

1. ⟨C⟩φ → ⟨C∪D⟩φ (надмножество по крайней мере столь же мощно)
2. ⟨∅⟩φ → ⟨S⟩φ (отношение между пустой коалицией и полной коалицией)
3. ⟨C⟩(φ∧ψ) → ⟨C⟩φ (реализация двух целей влечёт реализацию одной цели)

Связанные работы

Логика аукционов

1. Языки ставок: Языки OR/XOR для выражения предпочтений в комбинаторных аукционах (Nisan 2000)
2. Представление правил аукционов: Лёгкая формализация (Mittelmann et al. 2022)
3. Стратегия повторяющихся аукционов: Представление и рассуждение (Belardinelli et al. 2022)
4. Ограниченная рациональность: Захват ограниченной рациональности в аукционах (Mittelmann et al. 2021)
5. Логика стратегии: Использование вариантов SL для проектирования и синтеза механизмов (Mittelmann et al. 2023, 2025)
   • Примечание: Общая сложность проверки моделей SL является неэлементарной
6. Автоматическая верификация: Формальная верификация протоколов аукционов (Garg et al. 2025; Caminati et al. 2015)

Инновация данной работы: Первое исследование динамики диффузии аукционов с логической точки зрения, где множество агентов не фиксировано.

DEL и логика социальных сетей

1. DEL: Моделирование изменения знаний при событиях, данная работа заимствует идеи обновления моделей
2. Логика социальных сетей (SNL):
   • Распространение информации (Christoff & Hansen 2015; Baltag et al. 2019)
   • Социальное влияние (Christoff et al. 2016)
   • Эхо-камеры (Pedersen et al. 2019)
3. Связанные работы: Видимость и распространение постов в социальных сетях (Galimullin & Pedersen 2024)
4. Гибридная логика: Использование имён для ссылки на агентов (Areces & ten Cate 2007)
5. Объявления коалиций: Операторы коалиций в DEL (Ågotnes & van Ditmarsch 2008)
   • Сложность проверки моделей PSPACE-полнота (Alechina et al. 2021)
6. Параллельные игры: Многошаговые параллельные игры с использованием модальностей DEL для изменения моделей (Maubert et al. 2020)
7. Добавление стрелок в модальную логику (Areces et al. 2015)

Позиционирование данной работы: Объединение идей SNL, DEL, CL/ATL, впервые применённых к верификации диффузионных аукционов.

Заключение и обсуждение

Основные выводы

1. Предложена первая логическая система формальной верификации диффузионных аукционов
2. L_n и SL_n способны захватывать распределение товаров, изменения полезности, локальные свойства сети, равновесие Нэша и т.д.
3. Логика является динамической и может верифицировать свойства после модификации сети
4. Сложность проверки моделей: L_n — P, SL_n — PSPACE-полнота
5. Проблема существования стратегии — NP-полнота
6. Определение DAM универсально и может вмещать различные типы аукционов (при условии, что функции не превышают сложность проверки моделей)

Ограничения

1. Ограничения сложности функций: Требуется, чтобы вычислительная сложность P, Pay, U не превышала сложность проверки моделей
   • L_n требует полиномиального времени
   • SL_n требует полиномиального пространства
   • Исключает некоторые оптимальные функции распределения (например, NP-полное распределение в механизме VCG)
2. Предположение о одном товаре: Текущая структура ограничена аукционами одного товара (несколько копий)
3. Полная информация: Не рассматривается неполная информация и байесовский анализ
4. Стратегия покупателей: Основное внимание уделяется стратегии продавца, стратегическое рассуждение покупателей не полностью исследовано
5. Предположение об ограниченном бюджете: На практике бюджет может быть более сложным
6. Структура сети: Предполагается, что отношения дружбы симметричны и фиксированы (кроме изменений, вызванных диффузией)

Направления будущих исследований

1. Вероятностная структура: Формальная верификация неполной информации и байесовского анализа (Huang et al. 2025)
2. Стратегия покупателей: Рассмотрение стратегического поведения и рассуждения покупателей
3. Аксиоматизация: Исследование полных аксиоматических систем для L_n и SL_n
4. Комбинаторные аукционы: Расширение на сценарии комбинаторных аукционов
5. Практическое применение: Верификация на данных реальных социальных сетей
6. Проблема синтеза: Автоматический синтез механизмов, удовлетворяющих заданным свойствам

Глубокая оценка

Преимущества

1. Значительный теоретический вклад

• Новаторство: Первое применение формальных методов к верификации диффузионных аукционов, открытие нового направления исследований
• Теоретическая глубина: Полный анализ сложности (P, NP-полнота, PSPACE-полнота)
• Анализ выразительности: Строгое доказательство SL_n > L_n с преобразованием на конечных механизмах

2. Элегантное проектирование методов

• Модульное проектирование: L_n захватывает базовую динамику, SL_n добавляет стратегическое рассуждение
• Универсальная структура: Определение DAM не фиксирует конкретные функции, применимо к различным механизмам
• Простой синтаксис: Логические конструкции интуитивны, легко выражают сложные свойства

3. Разнообразные технические инновации

• Кросс-дисциплинарное слияние: Успешное объединение идей DEL, SNL, CL/ATL
• Моделирование динамической сети: Элегантная обработка динамических изменений социальной сети
• Параллельные операции: Унификация параллельного и последовательного выполнения через •

4. Подробные примеры

• Богатые работающие примеры (одиночный продавец, конкуренция двух продавцов)
• Ясный анализ случаев, демонстрирующий выразительность логики
• Конкретная реализуемость формализации экономических концепций, таких как равновесие Нэша

5. Полные доказательства

• Технический приложение содержит подробные доказательства всех теорем
• Конструкции редукций (3-SAT, QBF) имеют педагогическую ценность
• Псевдокод алгоритмов ясен и реализуем

Недостатки

1. Отсутствие экспериментальной верификации

• Нет эмпирической оценки: Отсутствуют эксперименты на реальных или синтетических данных
• Масштабируемость неизвестна: Практическая производительность алгоритмов на крупных сетях неясна
• Отсутствие реализации инструмента: Нет реализации проверки моделей или открытого кода

2. Ограниченные сценарии применения

• Ограничение одного товара: Реальные сценарии электронной коммерции часто включают несколько товаров
• Упрощённые предположения: Полная информация, симметричная дружба и другие предположения слишком сильны
• Простая модель стимулов: Фиксированные значения стимулов могут быть недостаточно гибкими

3. Недостаточное моделирование поведения покупателей

• Покупатели пассивно принимают стимулы, отсутствует активное стратегическое рассуждение
• Не рассмотрена возможность сговора между покупателями
• Решение о приглашении упрощено до "приглашения всех"

4. Стоимость сложности

• PSPACE-полнота SL_n ограничивает практическое применение
• NP-полнота проблемы существования стратегии неприемлема для больших экземпляров
• Не исследованы приближённые алгоритмы или эвристики

5. Поверхностный анализ экономических свойств

• Хотя можно выразить равновесие Нэша, другие свойства проектирования механизмов анализируются поверхностно
• Совместимость стимулов, индивидуальная рациональность только упомянуты, не детально верифицированы
• Диалог с экономической литературой недостаточен

Влияние

Вклад в область

1. Новое направление исследований: Открытие направления формальной верификации диффузионных аукционов
2. Методологический вклад: Демонстрация применения логических методов к динамическим механизмам на сетях
3. Теоретическая база: Предоставление прочной формальной основы для последующих исследований

Практическая ценность

1. Потенциальные приложения: Социальная электронная коммерция, системы вознаграждения за рекомендации, краудфандинг, онлайн-реклама
2. Инструменты верификации: Возможность разработки автоматических проверок моделей для верификации свойств механизмов
3. Проектирование механизмов: Предоставление дизайнерам нормативного языка и средств верификации

Воспроизводимость

• Теоретическая воспроизводимость: Определения и доказательства полные и ясны
• Вызовы реализации: Требуется реализация проверки моделей, значительный объём работы
• Требования данных: Требуются данные социальных сетей и параметры аукциона

Применимые сценарии

Идеальные сценарии применения

1. Социальная электронная коммерция: Использование социальных отношений пользователей для продвижения товаров
2. Системы вознаграждения за рекомендации: Пользователи получают вознаграждение за рекомендацию друзей
3. Платформы краудфандинга: Распространение проектов через социальные сети
4. Онлайн-реклама: Конкуренция рекламодателей за пользователей социальных сетей

Условия ограничения

1. Масштаб сети: Сети среднего размера (из-за ограничений сложности)
2. Сценарии одного товара: Текущая структура ограничена
3. Полная информация: Требуется знание структуры сети и оценок
4. Рациональные агенты: Предположение полной рациональности агентов

Неприменимые сценарии

1. Крупномасштабные сети: Социальные сети с миллионами узлов
2. Сложные товары: Товары с несколькими атрибутами, настраиваемые
3. Динамические оценки: Оценки, изменяющиеся со временем
4. Неполная информация: Асимметричная информация между агентами

Библиография

Основные ссылки

1. Zhao et al. (2018): Пионерская работа по диффузионным аукционам
2. Li et al. (2022): Проектирование диффузионных аукционов
3. Pauly (2002): Основы логики коалиций
4. Alur et al. (2002): Оригинальная статья по ATL
5. van Ditmarsch et al. (2008): Учебник по DEL
6. Pedersen (2024): Обзор логики социальных сетей
7. Mittelmann et al. (2023, 2025): Верификация аукционов логикой стратегии

Связанные направления

1. Проектирование механизмов: Nisan et al. (2007) - Algorithmic Game Theory
2. Теория аукционов: Vickrey (1961), Clarke (1971), Groves (1973) - механизм VCG
3. Проверка моделей: Clarke et al. (2018) - Handbook of Model Checking
4. Социальные сети: Christoff & Hansen (2015), Baltag et al. (2019)

Резюме

Данная работа является новаторским исследованием формальной верификации диффузионных аукционов. Введение логических систем L_n и SL_n обеспечивает прочную теоретическую основу для этой новой области. Основные преимущества заключаются в полноте теории, универсальности методов и разнообразии технических инноваций. Однако отсутствие эмпирической оценки и ограничения на практическое применение в крупномасштабных сценариях являются явными недостатками. Будущие работы, объединяющие верификацию на реальных данных, расширение на многотоварные сценарии и разработку эффективных приближённых алгоритмов, значительно повысят практическую ценность. В целом, это высококачественная теоретическая работа, вносящая важный вклад в кросс-дисциплинарные исследования на пересечении проектирования механизмов, логики и социальных сетей.