| paper | d4-conf-ijcai-2020-0061 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | low |
| authors would recognise it | unclear |
Theorem 23 is a clear computational result, and the proposed weighted model-checking problem is stated concretely over a population distribution. The unresolved issue is whether changing an entire cohort-pair relation is a recognizable high-multiplicity version of LAE’s single-dyad update, or a new bloc-level dynamic. That issue determines whether the mirror passes the recognition gate.
fails bit b-changes — the continuum limit changes the question
A single-dyad update can split a cohort and vanish at population scale, while flipping a whole cohort-pair block changes (n^2) dyads and adds synchronized update semantics.
fatal: False
It is undecided whether the authors would regard synchronized cohort-pair updates as the natural high-multiplicity version of LAE’s single-dyad dynamics; an explicit modeling commitment from the authors or a principled limiting derivation of those updates would settle this.
The proposed mirror covers Theorem 23’s model-checking result; it leaves Theorem 26’s validity-checking result and the balance and stability results untreated.
I would make one focused case: Mass-LAE model checking, a continuous cohort version of the paper’s LAE model. Its anchor is Theorem 23, proved in this paper: given a finite social network \(N\) and an LAE formula \(\varphi\), deciding whether \(N\models\varphi\) is PSPACE-complete. The result holds whether the agent set is part of the input or fixed. The paper proves hardness by reducing quantified Boolean formula satisfiability, and proves membership by a polynomial-space search through the network’s evolution. The hardness reduction uses a network with one positive edge and all other edges neutral; the Boolean choices are made by quantified variables. The theorem, rather than the particular proof encoding, is the problem I would mirror.
Here is the mirror. Take a finite support \(T\) of social types, with positive rational masses \(\mu_t\) summing to \(1\), and a symmetric relation matrix \(R:T\times T\to\{+,-,0\}\). A type is a cohort whose members have the same LAE-relevant relations to every cohort and undergo the same updates. \(R(t,u)\) gives the tie between cohorts \(t\) and \(u\); \(R(t,t)\) gives the tie within a cohort. Constants in a formula name cohorts. A variable ranges over the support, and \(\exists_{\ge q}x\,\varphi\), for rational \(q\in[0,1]\), holds when the mass of types satisfying \(\varphi\) is at least \(q\). Thus \(\exists x\) means positive satisfying mass, and \(\forall x\) means mass \(1\).
The dynamics preserve the paper’s pressure rule, replacing counts of third parties with their mass. For types \(t,u\), define
\[
A_\mu(t,u)=\sum_{v\in T}\mu_v\,
\mathbf 1[R(t,v)=R(u,v)\in\{+,-\}],
\qquad
D_\mu(t,u)=\sum_{v\in T}\mu_v\,
\mathbf 1[\{R(t,v),R(u,v)\}=\{+,-\}].
\]
Use these as attraction and repulsion in the paper’s stability-score definition. A successor either leaves a stable state unchanged or changes one type-pair relation in the direction prescribed by its weighted pressure. A change to \(R(t,u)\) updates the whole cohort-pair block. Temporal operators use the ordinary path semantics over the resulting finite state graph.
Call the decision problem Mass-LAE Model Checking: given \(T,\mu,R\), any named cohort constants, and a Mass-LAE formula \(\varphi\), decide whether the current weighted network satisfies \(\varphi\). The support is explicit; complexity is measured in \(\tau=|T|\), formula length, and the bit length of the rational masses and thresholds. This is a continuous-population question: \(\mu_t\) is a fraction of society, and attraction and repulsion are population fractions.
A plausible regime is a large organization or online community with a few stable blocs, where members of a bloc share the same alliance pattern toward other blocs. There may be millions of people but only a small number \(\tau\) of relation types. The mirror treats a bloc as a type because its members are indistinguishable for the relations and dynamics being modeled. Cohort-wide relation updates are the macroscopic counterpart of changing one edge in the original finite network. The paper’s authors could reasonably recognize this as their pressure-driven network evolution and temporal verification question, with mass replacing counts.
I expect hardness to persist, in the Class B spirit. In the paper’s QBF reduction, let three cohorts \(A,B,C\) have positive mass, and let \(R(A,B)=+\) with all other relations neutral. Under the mass semantics, a quantified variable can choose \(B\) for true and \(A\) or \(C\) for false; universal quantification checks both truth values. The translated formulas use the current relation atoms and quantifiers, not temporal operators, so later changes in the network do not affect the reduction. This preserves the PSPACE-hardness with fixed support and macroscopic masses. It suggests the hard core comes from alternation in the logic, not population multiplicity; I would not claim PSPACE-completeness of the full weighted problem without a separate membership proof.
This mirrors Theorem 23 only. It generates useful follow-up questions: whether the full weighted problem is PSPACE-complete when \(\tau\) and binary-encoded masses are inputs; which restricted formula fragments become tractable; and whether weighted pressure preserves the paper’s termination bound.
The weakest point is that cohort constants and block-wide updates change LAE’s individual-agent semantics. If the authors or a referee require constants to name individual people and each transition to change exactly one individual dyad, this is a group-level LAE variant rather than their direct continuous analogue. The case survives only in regimes where cohorts are genuinely homogeneous. Within that regime, it retains the paper’s distinctive ingredients—signed ties, pressure from third parties, greedy updates, and temporal model checking—while making the society itself a mass distribution.
The sole anchor is Theorem 23, and it is a real computational result. The strongest case against mirroring it is that the proposed finite-support model does not preserve the paper’s transition system.
In the paper, a successor changes one individual dyad. If a finite society is compressed into types whose members have identical relations to everyone else, changing one dyad can split two types. With \(n\) agents, that affects only \(O(1/n)\) of the population; in the continuum limit, the step disappears. But changing an entire type-pair block to keep the step visible changes \(\Theta(n^2)\) dyads at once. That may describe a bloc-level consensus process, but it is a different update rule. The distinction matters to model checking because LAE’s temporal operators quantify over paths of those individual-edge updates.
A graphon-style model can retain the full pattern of pairwise ties, but a single-dyad update changes a measure-zero part of it and leaves the continuum state unchanged. Making the dynamics nontrivial would require a time scaling and a rule for which positive-measure sets of dyads update. That supplies new scheduling semantics, rather than a direct limit of the paper’s branching transition system. Keeping individual identities avoids that problem, but then a bounded support of complete types generally cannot represent the evolving network: one-edge changes can keep producing new relation profiles.
The proponent’s cohort interpretation is the strongest repair. Constants can name blocs, and a relation can hold uniformly between blocs; weighted pressure then makes sense. But it asks whether *blocs* change their relations as a unit. The paper asks whether one pair of agents changes its relation. Unless the authors recognize bloc-level updates as their problem, this is an adjacent model rather than a high-multiplicity mirror. The type-level constants also change what \(P_{aa}\) means: it now describes relations between distinct members of one bloc, not an agent’s relation to itself.
That said, this negative case is weak at the programme’s recognition gate. The QBF reduction survives the proposed mass semantics: with positive mass for two cohorts, an existential quantifier requiring positive satisfying mass can choose either Boolean value, while a universal quantifier with threshold \(1\) checks both. So neither the computational anchor nor its hardness disappears. If the authors accept bloc-wide updates as a natural version of LAE, Mass-LAE model checking is a worthwhile mirror. I can argue that this changes the dynamics; I cannot honestly rule out that they would recognize the resulting question as theirs.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.