Declarative ablation matrix for the ShotTx prover.
The matrix has three parts:
baseline/1— one row, all components enabled, at whatevertimeoutthe caller specifies.oat/1— one row per component switched off relative to the baseline (one-at-a-time ablation). Answers "how much does component X contribute to what the prover can solve?"sweeps/1— three numeric sweeps at three values each:timeout,initial_gamma_limit,prim_subst_batch_size. Answers "how sensitive is performance to the main tuning knobs?"
matrix/1 concatenates the three, deduplicated on the label. The default
base timeout is 5s; override with base_timeout: 2_000 etc. to reduce the
wall-clock cost.
Each entry is a {label, %Parameters{}} pair, fed straight to
ShotTx.Benchmark.TptpRunner.run_sweep/2.
Typical invocation
# From iex or `mix run -e`
configs = ShotTx.Benchmark.Ablation.matrix(base_timeout: 5_000)
ShotTx.Benchmark.TptpRunner.run_sweep(configs,
output_dir: "bench_results/2026-07-28",
language: :both
)Resume after Ctrl-C simply by re-invoking with the same output_dir — each
per-config CSV is loaded to skip already-completed problems. Pause a live
sweep with touch bench_results/2026-07-28/STOP.
Summary
Functions
Baseline: all components on, default parameters.
Full ablation matrix: baseline + OAT + numeric sweeps.
One-at-a-time ablations. Each entry differs from the baseline by a single component turned off (or a single enum flipped to its most neutral variant).
Convenience wrapper: build the matrix and run it against TPTP, writing to
output_dir. Extra options are forwarded to TptpRunner.run_sweep/2.
Numeric parameter sweeps at three values each.
Types
@type entry() :: {String.t(), ShotTx.Data.Parameters.t()}
Functions
@spec baseline(pos_integer()) :: [entry()]
Baseline: all components on, default parameters.
Full ablation matrix: baseline + OAT + numeric sweeps.
Deduplicated on the %Parameters{} value so that sweep rows equal to
the baseline (typically the middle point of each numeric sweep) drop
out and are not run twice. The first occurrence's label wins.
@spec oat(pos_integer()) :: [entry()]
One-at-a-time ablations. Each entry differs from the baseline by a single component turned off (or a single enum flipped to its most neutral variant).
Off-by-default components (currently only suggestions_enabled) appear
as <name>_on rows that flip them on so their impact still shows up in
the sweep.
@spec run(keyword()) :: :ok | :stopped
Convenience wrapper: build the matrix and run it against TPTP, writing to
output_dir. Extra options are forwarded to TptpRunner.run_sweep/2.
@spec sweeps(pos_integer()) :: [entry()]
Numeric parameter sweeps at three values each.