← All papers
Universality and Convergence of Generative Flows
cs.LG
Oct 4, 2026 · v1
math.PR
TL;DR
Theorems about GFlowNet loss certification, existence and convergence are machine-checked in a Lean 4/Mathlib development with an axiom audit; each theorem is tagged certified.
Abstract
Generative flows sample from an unnormalized target by training a flow to be balanced, and the training loss is the signal a practitioner watches. We ask what that signal is worth: whether a small loss certifies an accurate sampler, whether the loss can be driven to zero, and how fast gradient descent does so. The loss decides the first. Losses that compare the two sides of the balance by their difference bound, in total variation, the error of the sampler the flow implies, with explicit constants that do not involve the policy; flow-matching losses that compare them through a ratio admit no such bound, already on a single cycle, whenever their generator is continuous at balance. On graphs, the backward policy decides the other two. Once it is frozen, balance becomes invariance under the backward chain, so that existence is free on finite graphs, and one constant — the norm of that chain's Green operator, which plays the role of an inverse spectral gap — fixes the order of the curvature of the loss around the balanced flow, from above and below, and sets a floor under the rate at which training converges near it. The mechanism is that gradient descent diffuses the flow along the backward policy. For the squared-logarithm generator of detailed and trajectory balance, training the balance loss on states converges globally on every finite path-connected graph, from every positive initialization. The constant can be infinite while backward trajectories are short on average, and exact flow matching can then fail. The bounds and rates are tested by exact computation on enumerable state spaces, and every theorem carries a certification status computed from a Lean 4 development.
Problem
The question is what the training loss of a generative flow (GFlowNet) is worth. It splits into three parts: whether a small loss certifies an accurate sampler, whether the loss can be driven to zero, and how fast gradient descent converges.
Approach
Difference losses are shown to bound the sampler's total-variation error with explicit constants. Ratio-based flow-matching losses are shown to admit no such bound. With the backward policy frozen, balance becomes invariance under the backward chain, and the norm of that chain's Green operator controls both the curvature of the loss and the convergence rate. Results are formalized in a strict Lean 4 library pinned to a Mathlib release, which allows only the standard axioms.
