Technical Summary: Diffusion-Guided Search via Exponential Tilting (DIFFTILT)

Problem Statement

The verification and validation of autonomous and cyber-physical systems (CPS) face a fundamental challenge: discovering rare, safety-critical failures. These failures are often characterized by multiplicative rarity, where a failure event requires the simultaneous occurrence of a rare input scenario and a rare system execution trace.

Existing falsification approaches typically rely on conditional sampling strategies. These methods factor the joint distribution of environments and executions, sampling inputs first and then generating traces conditioned on those inputs. The paper argues that this approach suffers from a multiplicative rarity effect: even with accurate conditional models, the probability of observing a failure is the product of the rarity of the input ($\delta$) and the rarity of the trace given that input ($\epsilon$). Consequently, the expected number of samples required to find a failure scales as $O(1/(\delta\epsilon))$, making exhaustive search prohibitively expensive. Furthermore, classical importance sampling (IS) methods often require access to ideal reference distributions or explicit likelihood models, which are rarely available in realistic black-box testing pipelines.

Methodology: DIFFTILT

The paper proposes DIFFTILT (Diffusion-Guided Search via Exponential Tilting), a framework that reframes falsification as the exponential tilting of a learned joint distribution over environments and executions.

1. Joint Generative Modeling

Instead of modeling inputs and traces separately, DIFFTILT learns a joint diffusion model $p_\theta(x, y)$, where $x$ represents environment inputs and $y$ represents system execution traces. This model serves as a reusable prior over scenarios. Crucially, the generative model acts as a base density and need not faithfully represent the true system dynamics; it merely provides a support for the sampler.

2. Exponential Tilting as Importance Sampling

The core mechanism involves reweighting the joint distribution using a surrogate score function $S(x, y)$ (e.g., a robustness predictor or reward function) that correlates with failure. The tilted distribution is defined as:
$$p_{\theta, \beta}(x, y) \propto p_\theta(x, y) \exp(\beta S(x, y))$$
where $\beta$ is the tilting parameter.

The paper establishes that this diffusion-guided sampling admits an exact interpretation as importance sampling in the joint space. The guidance scores act as likelihood-ratio tilts that reallocate probability mass toward failure-relevant behaviors. The authors prove that this reweighting is the KL-optimal (Kullback-Leibler divergence minimizing) biased distribution that satisfies a constraint on the expected score, thereby amplifying the probability of failure under mild assumptions.

3. Theoretical Guarantees

• Amplification of Failure Probability: The paper proves that exponential tilting provably increases the probability of sampling a failure if the score function $S$ ranks failing behaviors higher than non-failing ones in a distributional sense (specifically, under a First-Order Stochastic Dominance assumption).
• Overcoming Multiplicative Rarity: Unlike conditional sampling, which is capped by the failure rate within a specific input, joint tilting can reweight the entire joint space. This allows the method to overcome the multiplicative rarity bottleneck by shifting mass directly toward the joint regions where failures are likely.
• Deterministic Systems: For deterministic dynamical systems where $y = \Phi(x)$, the joint tilting reduces to optimal importance sampling over inputs along the dynamics manifold. This ensures that even if the predicted trace $\hat{y}$ is imperfect, the method remains valid because the true simulator is only invoked on the selected input $x$.

4. Algorithmic Pipeline

The DIFFTILT pipeline operates in two phases:

• Offline: A joint diffusion model is trained on paired $(x, y)$ data. This prior is frozen and reused across different specifications without retraining.
• Online:
  1. A surrogate score function $S_k$ is trained on accumulated simulation data to approximate failure likelihood.
  2. Candidates are generated via gradient-guided reverse diffusion, where the score gradient $\nabla S_k$ biases the denoising process toward high-score (failure-prone) regions.
  3. A candidate is selected, executed in the black-box simulator to obtain the true trace and robustness, and the result is used to refine the surrogate.
  4. This loop continues until a falsification is found or the simulation budget is exhausted.

Key Contributions

1. Formal Foundation: The paper provides a formal foundation for diffusion-guided falsification, interpreting it as principled counterexample generation via exponential tilting of a joint distribution.
2. Theoretical Analysis: It establishes sufficient and necessary conditions under which exponential tilting amplifies failure probability, demonstrating via First-Order Stochastic Dominance (FOSD) that the method is effective when the score ranks failures above non-failures.
3. Limitation of Conditional Sampling: The work characterizes the fundamental limitation of conditional sampling (multiplicative rarity) and shows that joint tilting overcomes this by reallocating mass in the joint space.
4. Reduction to Input-Space IS: For deterministic systems, the authors show that joint tilting reduces to optimal importance sampling over inputs, bridging the framework with existing simulation-based verification workflows.
5. New Benchmark: The paper introduces the TT2D tractor-trailer benchmark, adapted from existing work, to evaluate falsification under well-defined specifications and trajectory-level objectives, highlighting scenarios where specification-based rewards differ from trajectory-level costs.

Experimental Results

The authors evaluated DIFFTILT against FReaK, a state-of-the-art falsification method based on Koopman operator linearization, across three benchmark suites: Automatic Transmission (AT), Chasing Cars (CC), and the proposed Tractor-Trailer (TT2D).

• Automatic Transmission (AT): DIFFTILT was less competitive than FReaK on specifications involving discrete gear signals (e.g., AT51, AT54). The authors attribute this to the "flattened" robustness landscape caused by discrete dynamics, which renders gradient-based guidance uninformative. However, it performed competitively on continuous specifications.
• Chasing Cars (CC): On long-horizon and nested specifications (CC4, CC5, CCx), DIFFTILT demonstrated significant advantages. While FReaK's optimization becomes expensive and less accurate as the horizon and nesting depth increase, DIFFTILT maintained high falsification rates with fewer simulations, as it relies on the surrogate score of realized traces rather than logical formula encoding.
• Tractor-Trailer (TT2D): DIFFTILT achieved a 100% falsification rate across all six scenarios (including those with obstacles and tight tolerances) using 4000 training points, significantly outperforming FReaK in both success rate and simulation efficiency. The results suggest that DIFFTILT benefits from richer trajectory-level guidance signals (goal-reaching costs) that are difficult to encode in standard STL-based optimization frameworks.

Significance and Claims

The paper claims that DIFFTILT offers a sound, distribution-aware enhancement to counterexample generation. Its primary significance lies in:

• Decoupling the Prior from the System: The generative model serves only as a base density and need not be a perfect model of the system under test. True system evaluations are limited to the learning of the scoring function, enabling selective and adaptive use of expensive simulations.
• Generalizability: While focused on falsification, the framework is general and applicable to other scenario-generation problems such as planning and synthesis. It allows for distribution-aware exploration of complex scenario spaces beyond simple safety violations.
• Theoretical Rigor: By grounding diffusion-guided search in importance sampling theory and stochastic order analysis, the paper provides provable guarantees regarding the amplification of failure probabilities, moving beyond heuristic search strategies.

The authors acknowledge limitations, particularly regarding the performance on systems with discrete dynamics where gradients vanish, and note that the tilting strength $\beta$ currently requires manual tuning. They suggest future work in adaptive tuning of $\beta$, handling hybrid dynamics, and extending the analysis to stochastic systems.