Table of Contents
Fetching ...

Logical GANs: Adversarial Learning through Ehrenfeucht Fraisse Games

Mirco A. Mannucci

TL;DR

LOGAN introduces a framework that imposes bounded-depth logical constraints on the GAN discriminator, recasting adversarial learning as an Ehrenfeucht--Fraïssé game to ensure generated structures satisfy formal properties. By coupling a depth-$k$ observer with an EF-based loss and cheap certificates, LOGAN delivers interpretable failure witnesses and a controllable complexity budget for training. Four reproducible experiments show high property satisfaction in simulations (92%–98%) and measurable improvements (5%–14%) during real neural GAN training, with connectivity reaching 98% satisfaction. The approach offers a practical path toward trustworthy, logic-bounded generation across domains like protein design, network topology, and molecular graphs, and is released as open-source for broader adoption and extension.

Abstract

GANs promise indistinguishability, logic explains it. We put the two on a budget: a discriminator that can only ``see'' up to a logical depth $k$, and a generator that must look correct to that bounded observer. \textbf{LOGAN} (LOGical GANs) casts the discriminator as a depth-$k$ Ehrenfeucht--Fraïssé (EF) \emph{Opponent} that searches for small, legible faults (odd cycles, nonplanar crossings, directed bridges), while the generator plays \emph{Builder}, producing samples that admit a $k$-round matching to a target theory $T$. We ship a minimal toolkit -- an EF-probe simulator and MSO-style graph checkers -- and four experiments including real neural GAN training with PyTorch. Beyond verification, we score samples with a \emph{logical loss} that mixes budgeted EF round-resilience with cheap certificate terms, enabling a practical curriculum on depth. Framework validation demonstrates $92\%$--$98\%$ property satisfaction via simulation (Exp.~3), while real neural GAN training achieves $5\%$--$14\%$ improvements on challenging properties and $98\%$ satisfaction on connectivity (matching simulation) through adversarial learning (Exp.~4). LOGAN is a compact, reproducible path toward logic-bounded generation with interpretable failures, proven effectiveness (both simulated and real training), and dials for control.

Logical GANs: Adversarial Learning through Ehrenfeucht Fraisse Games

TL;DR

LOGAN introduces a framework that imposes bounded-depth logical constraints on the GAN discriminator, recasting adversarial learning as an Ehrenfeucht--Fraïssé game to ensure generated structures satisfy formal properties. By coupling a depth- observer with an EF-based loss and cheap certificates, LOGAN delivers interpretable failure witnesses and a controllable complexity budget for training. Four reproducible experiments show high property satisfaction in simulations (92%–98%) and measurable improvements (5%–14%) during real neural GAN training, with connectivity reaching 98% satisfaction. The approach offers a practical path toward trustworthy, logic-bounded generation across domains like protein design, network topology, and molecular graphs, and is released as open-source for broader adoption and extension.

Abstract

GANs promise indistinguishability, logic explains it. We put the two on a budget: a discriminator that can only ``see'' up to a logical depth , and a generator that must look correct to that bounded observer. \textbf{LOGAN} (LOGical GANs) casts the discriminator as a depth- Ehrenfeucht--Fraïssé (EF) \emph{Opponent} that searches for small, legible faults (odd cycles, nonplanar crossings, directed bridges), while the generator plays \emph{Builder}, producing samples that admit a -round matching to a target theory . We ship a minimal toolkit -- an EF-probe simulator and MSO-style graph checkers -- and four experiments including real neural GAN training with PyTorch. Beyond verification, we score samples with a \emph{logical loss} that mixes budgeted EF round-resilience with cheap certificate terms, enabling a practical curriculum on depth. Framework validation demonstrates -- property satisfaction via simulation (Exp.~3), while real neural GAN training achieves -- improvements on challenging properties and satisfaction on connectivity (matching simulation) through adversarial learning (Exp.~4). LOGAN is a compact, reproducible path toward logic-bounded generation with interpretable failures, proven effectiveness (both simulated and real training), and dials for control.
Paper Structure (63 sections, 3 theorems, 2 equations, 4 tables, 1 algorithm)

This paper contains 63 sections, 3 theorems, 2 equations, 4 tables, 1 algorithm.

Key Result

Theorem 3.2

Two structures are indistinguishable by any FO sentence of quantifier depth up to $r$ iff Duplicator has a winning strategy in $EF_r$.

Theorems & Definitions (7)

  • Definition 3.1: EF Game
  • Theorem 3.2: EF Characterization
  • Definition 4.1: Extension-Probe Game $\mathrm{EP}_k(T)$
  • Proposition 4.2: Equivalence to bounded EF
  • Definition 4.3: Logical GAN
  • Proposition 4.4: Equilibrium under idealized assumptions
  • Remark B.1