Adversarial time series

Crystal Clear

This demo classifies overlapping windows from a synthetic crystal-alignment scan and checks a temporal requirement on the resulting score trace. Draw a small perturbation, or run PGD and inspect the one it finds.

Try the attack What am I looking at?
Window 32 Stride 2 3 classes

01 / Experiment

Find a temporal counterexample

The plots start from a seeded synthetic scan. Edit it by hand, sample random noise, or search the perturbation set with projected gradient descent.

Loading the demonstration models…

02 / Method

How the windows are coupled

A window begins every two samples, so neighboring 32-sample windows share 30 samples. All 81 predictions are evaluated from the same perturbed scan.

A

Synthetic signal

Two seeded detector channels describe a stylized transition into and out of a channeling-like region.

B

Sliding windows

A small ReLU network classifies overlapping 32-sample windows every two samples.

C

Temporal property

The requirement passes when five consecutive channeling scores reach 0.78. STL robustness gives the distance from that threshold.

A two-window example

Both windows use the middle sample

Take a signal with three samples. The classifier first reads [x0, x1] and then [x1, x2]. An attack may change the shared sample x1 by at most 0.060.

In this local toy model, raising x1 lowers the first score; lowering x1 lowers the second. Optimizing the windows separately therefore asks the same sample to move in opposite directions.

The slider applies one shared perturbation and recomputes both scores.

Optimize the windows separately

Toy requirement: at least one of the two scores must reach 0.780.

window 0

x0x1
δ1 = +0.060
score0.8400.720

window 1

x1x2
δ1 = −0.060
score0.8400.720
scores joined after separate optimization [0.720, 0.720] apparent violation

Choose one value for the shared sample

x0x1 + δ1x2

y0 = 0.840 − 2δ1 y1 = 0.840 + 2δ1

window 0 0.720 below threshold
window 1 0.960 above threshold
toy requirement: at least one score ≥ 0.780 holds

With δ1 = +0.060, window 0 falls to 0.720, while window 1 rises to 0.960. The toy requirement still holds.

The pair [0.720, 0.720] needs δ1 = +0.060 and δ1 = −0.060 at the same time.

This two-window sketch isolates the shared-variable issue. The main attack uses one 192 × 2 perturbation for all 81 windows before evaluating the F G property.

What does the optimizer minimize?

Projected gradient descent follows a smooth approximation of the temporal robustness value. Every step is projected into the channel-normalized L∞ budget. After the search, the page recomputes the exact STL margin and checks the perturbation bound; a feasible negative margin is reported as a counterexample.

Why not attack each window independently?

With stride two, adjacent windows share 30 samples. The actual attack maintains one 192 × 2 perturbation array. Gradients from every window accumulate into that array, and the score trace is recomputed from the resulting sensor signal.

What is the model?

Each window is average-pooled into four temporal bins per channel, passed through a 12-unit ReLU layer, and mapped to three softmax scores. Both sets of weights come from reproducible training on synthetic windows. The page evaluates the fixed weights in JavaScript.

What would verification add?

A sound verifier would over-approximate all neural-network score traces reachable inside the perturbation set, evaluate interval STL robustness, search abstract violations for a concrete witness, and refine loose bounds. It would return Verified, a concrete counterexample, or Unknown. This version stops at falsification.

03 / Context

Research context

The demo connects two lines of work: adversarial robustness in crystal alignment and STL verification of neural-network score traces.

NASA Formal Methods 2026

Adversarial Robustness of Time-Series Classification for Crystal Collimator Alignment

How bounded perturbations affect a time-series classification task motivated by crystal alignment.

Read the preprint

NFM 2026 RE×AI workshop

Verifying STL Properties of Neural-Network Classification Traces

Relating local classifier robustness to temporal requirements over a complete prediction trace.

Read the paper