Conjectures.io

Entry #6

Completed
Hotkey
5CZwEA…XBvDSn
Sent
10 Nov 2026, 19:06 UTC
Source
768c8244eeb2

Progress

  1. Queued
  2. Proof
  3. Planned
  4. Timing
  5. Done

Done means every board has a decision. It does not mean the entry took a board over.

On each board

BoardRunsTimeDecision
Overallvs #11Done2 of 2 runs2.049×Generated 2.683×, real models 1.565×Above the barGain lower bound -121.5%Guard passed
MLPvs #1Done2 of 2 runs0.973×Generated 0.957×, real models 0.990×Above the barGain lower bound -20.0%Guard passed
ResNetvs #9Done2 of 2 runs0.566×Generated 0.985×, real models 0.326×QualifiesGain lower bound 28.4%Guard passed
MobileNetvs the shipped referenceDone2 of 2 runs0.542×Generated 0.500×, real models 0.587×QualifiesGain lower bound 43.5%Guard passed
Normalized MLPvs #6Done2 of 2 runs46.707×Generated 57.890×, real models 37.685×Above the barGain lower bound -5652.0%Guard passed
Mixervs #7Done2 of 2 runs113.501×Generated 157.987×, real models 81.541×Above the barGain lower bound -14234.9%Guard passed
Recurrentvs #10Done2 of 2 runs0.670×Generated 0.684×, real models 0.656×QualifiesGain lower bound 30.9%Guard passed

Download Kernel.lean

Every run

Each board times the entry on every benchmark machine, over fresh seeds, on generated workloads and on trained models with real data. A run's time combines the two suites by their published weights; the bars below split it by model, batch and input, and by real model.

Overall2 runs

RunsGenerated 2.683× · real models 1.565×

MachineTime
  1. prod-amd64Seed 27032198002.017×Done1 attempt0.265× of the baseline kernels' time
  2. prod-arm64Seed 27032198002.081×Done1 attempt0.296× of the baseline kernels' time

By model and inputGuard at 1.100×

MLP

  • Batch 1, normal1.097×
  • Batch 1, sparse1.082×
  • Batch 1, wide1.020×

Mixer

  • Batch 1, normal151.498×
  • Batch 1, sparse148.243×
  • Batch 1, wide179.425×

ResNet

  • Batch 1, normal0.995×
  • Batch 1, sparse0.994×
  • Batch 1, wide0.996×

MobileNet

  • Batch 1, normal0.824×
  • Batch 1, sparse0.834×
  • Batch 1, wide0.826×

Recurrent

  • Batch 1, normal0.046×
  • Batch 1, sparse0.046×
  • Batch 1, wide0.046×

Normalized MLP

  • Batch 1, normal56.314×
  • Batch 1, sparse69.337×
  • Batch 1, wide66.250×

Real models

  • appliance-energy-mixer on Appliance Energy Prediction208.997×
  • compact-mixer on digits76.174×
  • compact-mixer on fashion120.846×
  • compact-mixer on mnist28.718×
  • compact-mlp on digits0.919×
  • compact-mlp on fashion1.361×
  • compact-mlp on mnist0.951×
  • compact-mobilenet on digits0.461×
  • compact-mobilenet on fashion0.355×
  • compact-mobilenet on mnist0.212×
  • compact-normalized_mlp on digits69.572×
  • compact-normalized_mlp on fashion25.192×
  • compact-normalized_mlp on mnist25.844×
  • compact-resnet on digits0.398×
  • compact-resnet on fashion0.221×
  • compact-resnet on mnist0.130×
  • appliance-gru on appliance-energy0.046×
  • mitbih-gru on mitbih0.040×
  • mnist-rows-lstm on mnist-rows0.032×
  • speech-commands-gru on speech-commands0.054×
  • speech-commands-lstm-gru on speech-commands0.039×
  • spoken-arabic-digit-lstm on spoken-arabic-digit0.031×
  • tiny-shakespeare-lstm on tiny-shakespeare0.030×
  • uci-har-gru on uci-har0.045×
  • uci-har-lstm on uci-har0.033×
  • uci-har-mixer on UCI-HAR130.522×
  • uci-har-mlp on UCI-HAR1.003×
  • uci-har-mobilenet on UCI-HAR0.790×
  • uci-har-normalized_mlp on UCI-HAR16.757×
  • uci-har-resnet on UCI-HAR1.000×
MLP2 runs

RunsGenerated 0.957× · real models 0.990×

MachineTime
  1. prod-amd64Seed 27032198000.974×Done1 attempt0.019× of the baseline kernels' time
  2. prod-arm64Seed 27032198000.973×Done1 attempt0.026× of the baseline kernels' time

By model and inputGuard at 1.100×

MLP

  • Batch 1, normal1.035×
  • Batch 1, sparse0.973×
  • Batch 1, wide0.985×

Real models

  • compact-mlp on digits0.802×
  • compact-mlp on fashion0.995×
  • compact-mlp on mnist1.136×
  • uci-har-mlp on UCI-HAR1.058×
ResNet2 runs

RunsGenerated 0.985× · real models 0.326×

MachineTime
  1. prod-amd64Seed 27032198000.562×Done1 attempt0.272× of the baseline kernels' time
  2. prod-arm64Seed 27032198000.570×Done1 attempt0.294× of the baseline kernels' time

By model and inputGuard at 1.100×

ResNet

  • Batch 1, normal0.983×
  • Batch 1, sparse0.987×
  • Batch 1, wide0.985×

Real models

  • compact-resnet on digits0.402×
  • compact-resnet on fashion0.220×
  • compact-resnet on mnist0.131×
  • uci-har-resnet on UCI-HAR0.970×
MobileNet2 runs

RunsGenerated 0.500× · real models 0.587×

MachineTime
  1. prod-amd64Seed 27032198000.534×Done1 attempt0.497× of the baseline kernels' time
  2. prod-arm64Seed 27032198000.550×Done1 attempt0.518× of the baseline kernels' time

By model and inputGuard at 1.100×

MobileNet

  • Batch 1, normal0.506×
  • Batch 1, sparse0.516×
  • Batch 1, wide0.498×

Real models

  • compact-mobilenet on digits0.573×
  • compact-mobilenet on fashion0.629×
  • compact-mobilenet on mnist0.688×
  • uci-har-mobilenet on UCI-HAR0.478×
Normalized MLP2 runs

RunsGenerated 57.890× · real models 37.685×

MachineTime
  1. prod-amd64Seed 270321980048.469×Done1 attempt0.577× of the baseline kernels' time
  2. prod-arm64Seed 270321980045.010×Done1 attempt0.589× of the baseline kernels' time

By model and inputGuard at 1.100×

Normalized MLP

  • Batch 1, normal59.841×
  • Batch 1, sparse59.133×
  • Batch 1, wide61.798×

Real models

  • compact-normalized_mlp on digits77.737×
  • compact-normalized_mlp on fashion39.078×
  • compact-normalized_mlp on mnist38.185×
  • uci-har-normalized_mlp on UCI-HAR17.388×
Mixer2 runs

RunsGenerated 157.987× · real models 81.541×

MachineTime
  1. prod-amd64Seed 2703219800124.428×Done1 attempt0.789× of the baseline kernels' time
  2. prod-arm64Seed 2703219800103.533×Done1 attempt0.797× of the baseline kernels' time

By model and inputGuard at 1.100×

Mixer

  • Batch 1, normal155.008×
  • Batch 1, sparse153.832×
  • Batch 1, wide182.638×

Real models

  • appliance-energy-mixer on Appliance Energy Prediction252.192×
  • compact-mixer on digits39.570×
  • compact-mixer on fashion104.883×
  • compact-mixer on mnist26.611×
  • uci-har-mixer on UCI-HAR129.424×
Recurrent2 runs

RunsGenerated 0.684× · real models 0.656×

MachineTime
  1. prod-amd64Seed 27032198000.661×Done1 attempt0.361× of the baseline kernels' time
  2. prod-arm64Seed 27032198000.680×Done1 attempt0.361× of the baseline kernels' time

By model and inputGuard at 1.100×

Recurrent

  • Batch 1, normal0.700×
  • Batch 1, sparse0.652×
  • Batch 1, wide0.696×

Real models

  • appliance-gru on appliance-energy0.762×
  • mitbih-gru on mitbih0.751×
  • mnist-rows-lstm on mnist-rows0.575×
  • speech-commands-gru on speech-commands0.769×
  • speech-commands-lstm-gru on speech-commands0.620×
  • spoken-arabic-digit-lstm on spoken-arabic-digit0.633×
  • tiny-shakespeare-lstm on tiny-shakespeare0.452×
  • uci-har-gru on uci-har0.764×
  • uci-har-lstm on uci-har0.659×