Conjectures.io

Entry #59

Completed
Hotkey
5ETigs…PwyKzz
Sent
11 Nov 2026, 16:33 UTC
Source
df356e9c8ca6

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 #50Done2 of 2 runs0.986×Generated 0.999×, real models 0.974×Above the barGain lower bound -7.6%Guard passed
MLPvs #44Done2 of 2 runs1.135×Generated 0.964×, real models 1.336×Above the barGain lower bound -38.5%Guard passed
ResNetvs #45Done2 of 2 runs0.942×Generated 0.941×, real models 0.944×QualifiesGain lower bound 2.6%Guard passed
MobileNetvs #42Done2 of 2 runs0.962×Generated 0.972×, real models 0.953×Not significantGain lower bound -0.7%Guard passed
Normalized MLPvs #48Done2 of 2 runs0.962×Generated 0.952×, real models 0.973×Not significantGain lower bound -18.7%Guard passed
Mixervs #47Done2 of 2 runs1.081×Generated 0.984×, real models 1.189×Above the barGain lower bound -26.3%Guard passed
Recurrentvs #49Done2 of 2 runs0.959×Generated 0.978×, real models 0.939×QualifiesGain lower bound 2.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 0.999× · real models 0.974×

MachineTime
  1. prod-amd64Seed 434141111.005×Done1 attempt0.009× of the baseline kernels' time
  2. prod-arm64Seed 434141110.968×Done1 attempt0.011× of the baseline kernels' time

By model and inputGuard at 1.100×

MLP

  • Batch 1, normal0.998×
  • Batch 1, sparse0.864×
  • Batch 1, wide0.834×

Mixer

  • Batch 1, normal1.019×
  • Batch 1, sparse1.129×
  • Batch 1, wide0.983×

ResNet

  • Batch 1, normal1.010×
  • Batch 1, sparse1.011×
  • Batch 1, wide0.965×

MobileNet

  • Batch 1, normal1.030×
  • Batch 1, sparse1.019×
  • Batch 1, wide0.981×

Recurrent

  • Batch 1, normal0.968×
  • Batch 1, sparse0.986×
  • Batch 1, wide0.982×

Normalized MLP

  • Batch 1, normal1.012×
  • Batch 1, sparse1.220×
  • Batch 1, wide1.012×

Real models

  • appliance-energy-mixer on Appliance Energy Prediction1.219×
  • compact-mixer on digits0.663×
  • compact-mixer on fashion1.015×
  • compact-mixer on mnist1.018×
  • compact-mlp on digits0.762×
  • compact-mlp on fashion0.810×
  • compact-mlp on mnist1.179×
  • compact-mobilenet on digits0.968×
  • compact-mobilenet on fashion1.000×
  • compact-mobilenet on mnist0.997×
  • compact-normalized_mlp on digits0.885×
  • compact-normalized_mlp on fashion0.821×
  • compact-normalized_mlp on mnist1.003×
  • compact-resnet on digits1.201×
  • compact-resnet on fashion1.000×
  • compact-resnet on mnist0.990×
  • appliance-gru on appliance-energy0.968×
  • mitbih-gru on mitbih0.984×
  • mnist-rows-lstm on mnist-rows0.984×
  • speech-commands-gru on speech-commands0.982×
  • speech-commands-lstm-gru on speech-commands0.972×
  • spoken-arabic-digit-lstm on spoken-arabic-digit0.984×
  • tiny-shakespeare-lstm on tiny-shakespeare0.977×
  • uci-har-gru on uci-har0.976×
  • uci-har-lstm on uci-har0.981×
  • uci-har-mixer on UCI-HAR1.017×
  • uci-har-mlp on UCI-HAR0.994×
  • uci-har-mobilenet on UCI-HAR0.991×
  • uci-har-normalized_mlp on UCI-HAR0.962×
  • uci-har-resnet on UCI-HAR1.144×
MLP2 runs

RunsGenerated 0.964× · real models 1.336×

MachineTime
  1. prod-amd64Seed 434141111.010×Done1 attempt0.014× of the baseline kernels' time
  2. prod-arm64Seed 434141111.275×Done1 attempt0.022× of the baseline kernels' time

By model and inputGuard at 1.100×

MLP

  • Batch 1, normal0.997×
  • Batch 1, sparse0.987×
  • Batch 1, wide1.003×

Real models

  • compact-mlp on digits0.794×
  • compact-mlp on fashion2.199×
  • compact-mlp on mnist1.957×
  • uci-har-mlp on UCI-HAR0.933×
ResNet2 runs

RunsGenerated 0.941× · real models 0.944×

MachineTime
  1. prod-amd64Seed 434141110.976×Done1 attempt0.007× of the baseline kernels' time
  2. prod-arm64Seed 434141110.910×Done1 attempt0.009× of the baseline kernels' time

By model and inputGuard at 1.100×

ResNet

  • Batch 1, normal0.941×
  • Batch 1, sparse0.959×
  • Batch 1, wide0.947×

Real models

  • compact-resnet on digits0.914×
  • compact-resnet on fashion0.933×
  • compact-resnet on mnist0.945×
  • uci-har-resnet on UCI-HAR0.985×
MobileNet2 runs

RunsGenerated 0.972× · real models 0.953×

MachineTime
  1. prod-amd64Seed 434141110.964×Done1 attempt0.012× of the baseline kernels' time
  2. prod-arm64Seed 434141110.961×Done1 attempt0.012× of the baseline kernels' time

By model and inputGuard at 1.100×

MobileNet

  • Batch 1, normal0.967×
  • Batch 1, sparse0.997×
  • Batch 1, wide0.976×

Real models

  • compact-mobilenet on digits0.897×
  • compact-mobilenet on fashion0.921×
  • compact-mobilenet on mnist0.960×
  • uci-har-mobilenet on UCI-HAR1.038×
Normalized MLP2 runs

RunsGenerated 0.952× · real models 0.973×

MachineTime
  1. prod-amd64Seed 434141110.965×Done1 attempt0.007× of the baseline kernels' time
  2. prod-arm64Seed 434141110.959×Done1 attempt0.013× of the baseline kernels' time

By model and inputGuard at 1.100×

Normalized MLP

  • Batch 1, normal0.929×
  • Batch 1, sparse1.021×
  • Batch 1, wide0.971×

Real models

  • compact-normalized_mlp on digits0.959×
  • compact-normalized_mlp on fashion0.996×
  • compact-normalized_mlp on mnist0.999×
  • uci-har-normalized_mlp on UCI-HAR0.939×
Mixer2 runs

RunsGenerated 0.984× · real models 1.189×

MachineTime
  1. prod-amd64Seed 434141111.006×Done1 attempt0.005× of the baseline kernels' time
  2. prod-arm64Seed 434141111.163×Done1 attempt0.005× of the baseline kernels' time

By model and inputGuard at 1.100×

Mixer

  • Batch 1, normal1.064×
  • Batch 1, sparse1.058×
  • Batch 1, wide0.994×

Real models

  • appliance-energy-mixer on Appliance Energy Prediction1.027×
  • compact-mixer on digits2.723×
  • compact-mixer on fashion0.980×
  • compact-mixer on mnist0.990×
  • uci-har-mixer on UCI-HAR0.876×
Recurrent2 runs

RunsGenerated 0.978× · real models 0.939×

MachineTime
  1. prod-amd64Seed 434141110.931×Done1 attempt0.010× of the baseline kernels' time
  2. prod-arm64Seed 434141110.987×Done1 attempt0.012× of the baseline kernels' time

By model and inputGuard at 1.100×

Recurrent

  • Batch 1, normal0.977×
  • Batch 1, sparse0.992×
  • Batch 1, wide0.991×

Real models

  • appliance-gru on appliance-energy0.905×
  • mitbih-gru on mitbih0.896×
  • mnist-rows-lstm on mnist-rows0.989×
  • speech-commands-gru on speech-commands0.865×
  • speech-commands-lstm-gru on speech-commands0.938×
  • spoken-arabic-digit-lstm on spoken-arabic-digit0.993×
  • tiny-shakespeare-lstm on tiny-shakespeare1.000×
  • uci-har-gru on uci-har0.891×
  • uci-har-lstm on uci-har0.989×