Perturbation-Position Scheduling Artifact

This repository contains the implementation and artifacts for perturbation-position scheduling experiments in Transformer robustness certification.

What Is Included

• Models/, Verifiers/, Parser.py, data_utils.py: Transformer model, bound-propagation verifier, configuration, and dataset-loading code.
• experiments/: scripts for verifier cascades, perturbation-position scheduling, pair scheduling, result summarization, and figure generation.
• results/: JSON logs for the reported tables and diagnostics.
• figures/: generated figures.
• ARTIFACT.md: artifact-use guide, archival-release checklist, and notes for connecting alternative verifier backends.
• CITATION.cff: citation metadata for the software artifact.

Large local assets are not committed to normal Git history. To rerun the full experiments, place the dataset files and trained checkpoints in the paths shown by the commands below, or obtain them from the artifact release package.

The implementation uses ordinary PyTorch/CUDA floating point arithmetic. The paper's guarantees are verifier-conditional: the scheduling layer adds no acceptance decisions beyond the underlying verifier outputs.

Reproduce Reported Metrics and Figures

The principal paper-facing work metrics and diagnostic figures can be regenerated from the committed JSON logs with one command:

bash experiments/reproduce_artifact_outputs.sh

This prints the all-position scheduling summary, gradient-ranking overhead, and two-token scheduling summary, then regenerates the per-example speedup and fallback figures in figures/.

Environment

The experiments were run in a Conda environment named pbverify.

conda env create -f environment.yml
conda activate pbverify

If using an existing environment, install the Python dependencies in requirements.txt and ensure pytorch_pretrained_bert, PyTorch, NumPy, NLTK, and tqdm are available.

Core Scripts

• experiments/download_agnews2.py Downloads the AG News CSV files used for the optional binary topic classification check.

• experiments/cascade_verification.py Runs pure Backward and early-exit cascade verification on matched perturbation tasks.

• experiments/sound_token_pruning_verification.py Runs one-token all-valid perturbation-position scheduling.

• experiments/sound_pair_pruning_verification.py Runs two-token pair scheduling, where each unordered pair is a scheduling task.

• experiments/budgeted_position_verification.py Provides the gradient-ranking helper used by scheduling scripts.

• experiments/plot_pruning_diagnostics.py Regenerates the per-example scheduling diagnostics figures.

• experiments/summarize_results.py Utility for summarizing result JSON files.

Reproduce Main One-Token Cascade Runs

SST-2, one-token L2, three matched positions:

conda run -n pbverify python experiments/cascade_verification.py \
  --dir=model_sst_1 \
  --data=sst \
  --samples=30 \
  --max_verify_length=32 \
  --perturbed_words=1 \
  --p=2 \
  --max_positions=3 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/cascade_model_sst_1_s30_pos3_i4.json

Yelp, one-token L2, three matched positions:

conda run -n pbverify python experiments/cascade_verification.py \
  --dir=model_yelp_1_fresh \
  --data=yelp \
  --samples=30 \
  --max_verify_length=32 \
  --perturbed_words=1 \
  --p=2 \
  --max_positions=3 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/cascade_model_yelp_1_fresh_p2_1w_s30_pos3_i4.json

For the L1 and L_inf norm rows, set --p=1 or --p=10, respectively, and use the corresponding result filenames in results/.

Reproduce Exhaustive All-Valid One-Token Cascade Runs

SST-2:

conda run -n pbverify python experiments/cascade_verification.py \
  --dir=model_sst_1 \
  --data=sst \
  --samples=30 \
  --max_verify_length=32 \
  --perturbed_words=1 \
  --p=2 \
  --max_positions=1000 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/cascade_model_sst_1_p2_1w_s30_allvalid_len32_i4.json

Yelp:

conda run -n pbverify python experiments/cascade_verification.py \
  --dir=model_yelp_1_fresh \
  --data=yelp \
  --samples=30 \
  --max_verify_length=32 \
  --perturbed_words=1 \
  --p=2 \
  --max_positions=1000 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/cascade_model_yelp_1_fresh_p2_1w_s30_allvalid_len32_i4.json

Reproduce One-Token Perturbation-Position Scheduling

SST-2, gradient ranking:

conda run -n pbverify python experiments/sound_token_pruning_verification.py \
  --dir=model_sst_1 \
  --data=sst \
  --samples=30 \
  --position_scope=all_valid \
  --on_validation_failure=search_failed \
  --ranker=gradient \
  --budgets 1 2 \
  --p=2 \
  --max_verify_length=32 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/sound_pruning_sst_s30_allvalid_k1_k2_fallback_i4.json

The available SST-2 scheduling results store k=1 and k=2 in separate files:

• results/sound_pruning_sst_s30_allvalid_k1_fallback_i4.json
• results/sound_pruning_sst_s30_allvalid_k2_fallback_i4.json

Yelp, gradient ranking:

conda run -n pbverify python experiments/sound_token_pruning_verification.py \
  --dir=model_yelp_1_fresh \
  --data=yelp \
  --samples=30 \
  --position_scope=all_valid \
  --on_validation_failure=search_failed \
  --ranker=gradient \
  --budgets 1 2 \
  --p=2 \
  --max_verify_length=32 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/sound_pruning_yelp_s30_allvalid_k1_k2_fallback_i4.json

For ranking ablations on SST-2, set --ranker=left_to_right or --ranker=random --ranking_seed=0.

Reproduce Two-Token Runs

Two-token all-pair cascade on SST-2:

conda run -n pbverify python experiments/cascade_verification.py \
  --dir=model_sst_1 \
  --data=sst \
  --samples=30 \
  --max_verify_length=16 \
  --perturbed_words=2 \
  --p=2 \
  --max_positions=1000 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/cascade_model_sst_1_p2_2w_s30_allpairs_len16_i4.json

Two-token pair scheduling on SST-2:

conda run -n pbverify python experiments/sound_pair_pruning_verification.py \
  --dir=model_sst_1 \
  --data=sst \
  --baseline=results/cascade_model_sst_1_p2_2w_s30_allpairs_len16_i4.json \
  --samples=30 \
  --max_verify_length=16 \
  --position_scope=all_valid \
  --on_validation_failure=search_failed \
  --pair_ranker=gradient_sum \
  --budgets 1 2 \
  --p=2 \
  --num_verify_iters=4 \
  --max_eps=0.01 \
  --res=results/sound_pair_pruning_sst_p2_2w_s30_allpairs_len16_k1_k2_fallback_i4.json

Use model_yelp_1_fresh, --data=yelp, and the Yelp cascade baseline filename for the Yelp two-token run.

Regenerate Figure

conda run -n pbverify python experiments/plot_pruning_diagnostics.py

Outputs:

• figures/pruning_per_example_speedup.pdf
• figures/pruning_per_example_fallbacks.pdf

Notes

• Reported timings are verification-work timings, not full end-to-end application latency. Training, preprocessing, model loading, and gradient-ranking overhead are not included in the main scheduling timing totals.
• Result JSON files contain sampled order, tokens, valid positions/tasks, selected tasks, verifier-stage statistics, returned radii, and timing fields.
• The two-token pair-scheduling script may run for a long time because the task set grows quadratically with the number of valid positions.

License

This repository is released under the MIT License. See LICENSE.