This is an automated rejection. No LLM generated, assisted/co-written, or edited work.
Read full explanation
Figure:compression vs. correspondence. Each dot is a proof of the network's average loss. Further right means fewer model evaluations. Higher means closer to the true loss.
Three AI agents proposed, implemented and checked a proof about a small neural network. The proof is an upper bound on the network's average loss over all 512 possible inputs. Loss is the penalty for giving the correct answer a low probability. A brute-force proof would run the network on all 512 inputs. This one runs it 8 times.
The trick is to group the inputs by their largest token.
See the trick
Each group is then added up with a formula instead of listing its members. The formula works because each term is a product with one factor per token position. Summing a product over all combinations just multiplies the per-position sums. For example, a×b×c summed over every choice of a, b, c from {1, 2} is 3×3×3 = 27, which is eight products added in one step. A standard inequality (the average of a logarithm is at most the logarithm of the average) turns the result into a guaranteed bound.
The bound is within 0.000013 of the true loss.
The Count-Softmax network
The input is three tokens, each one of 8 values (0–7), so there are 8³ = 512 inputs. The output is eight scores, one per candidate for "the maximum". Softmax turns them into probabilities. The network is hand-built and untrained. A token's score is its count divided by four. For input (2,2,7), token 2 scores 0.5, token 7 scores 0.25, and the rest score 0.
It does not compute the maximum. It favors tokens that appear, and repeated ones most. The true maximum always appears, so it gets a small boost. It receives 15.3% probability on average, against 12.5% for random guessing. The average loss is 1.885, against 2.079 for random guessing.
Results
Method
Mathematical step
Proven loss bound
Model evaluations
Brute force (all inputs)
Average the loss over all 512 inputs
1.885261388
512
Convexity
Replace distinct smaller tokens by repeated-token endpoints
1.891214817
64
Factorization
Sum each group by formula, then apply Jensen's inequality
1.885274023
8
Bounds are rounded up. Factorization uses 8 times fewer evaluations than convexity. Its error is about 471 times smaller.
Arguments
Brute force averages the loss over every input.
Convexity. Take three different tokens a < b < m, where m is the maximum. Their scores are the average of the scores for (a,a,m) and (b,b,m). Loss is convex in the scores, which means a bowl-shaped curve. So loss(a,b,m) ≤ [loss(a,a,m) + loss(b,b,m)] / 2. When we know convexity is there, we have 64 inputs to run.
Factorization. Let Z be the sum of exp(score) over the eight tokens, which is softmax's denominator. Because exp(a+b) = exp(a)·exp(b), Z splits into products with one factor per position. The inputs whose maximum is exactly m are those with every token ≤ m, minus those with every token ≤ m−1. Each group is summed by formula. The loss contains log Z, and the log of an average is at least the average of the log. The upper bound is:
L ≤ Σₘ pₘ · log E[Z | max = m] − T
Here pₘ is the probability that the maximum is m, E[Z | max = m] is the average of Z over inputs whose maximum is m, and T is the average score of the correct answer.
Automated Search
Proposer: writes the argument and records predicted numbers before any experiment.
Implementer: writes the code, checks it on a tiny brute-force case, and measures the bound and the cost.
Reviewer: checks the mathematics and code, diagnoses mismatches, and asks for fixes.
One proposal went through one full cycle. The reviewer caught three implementation problems. The idea itself needed no change.
Limits
A simpler exact argument beats this one on this network. It sorts inputs into three repetition patterns: all equal, two equal, all different. It runs one example of each and counts. That is exact with 3 evaluations. So this result shows that the process works, not that this is the best proof.
The identity relies on scores that add across tokens. Attention and other nonlinear networks breaks this.
A tighter proof is also not automatically a better explanation. ARC's surprise accounting scores explanations in bits. By my count, using my own conventions, just stating a single number like this loss is cheapest, at about 15 bits. An explanation pays off only when it explains more than it costs.
Next steps are to test on trained models, and
Where this comes from
The ILIAD Intensive worst-case interpretability course (exercise notebook) supplies the brute-force baseline, the convexity method and the idea behind the three-pattern comparison. The course builds on the Compact Proofs paper. ARC's post supplies surprise accounting. The Count-Softmax network and the agent setup are the author's. The factorization argument was produced by Codex. AI use. Text inside Arguments block was drafted by Claude and edited by me. I have checked the numbers. The factorization argument and its implementation were produced by Codex agents.
Figure: compression vs. correspondence. Each dot is a proof of the network's average loss. Further right means fewer model evaluations. Higher means closer to the true loss.
Three AI agents proposed, implemented and checked a proof about a small neural network. The proof is an upper bound on the network's average loss over all 512 possible inputs. Loss is the penalty for giving the correct answer a low probability. A brute-force proof would run the network on all 512 inputs. This one runs it 8 times.
The trick is to group the inputs by their largest token.
See the trick
Each group is then added up with a formula instead of listing its members. The formula works because each term is a product with one factor per token position. Summing a product over all combinations just multiplies the per-position sums. For example, a×b×c summed over every choice of a, b, c from {1, 2} is 3×3×3 = 27, which is eight products added in one step. A standard inequality (the average of a logarithm is at most the logarithm of the average) turns the result into a guaranteed bound.
The bound is within 0.000013 of the true loss.
The Count-Softmax network
The input is three tokens, each one of 8 values (0–7), so there are 8³ = 512 inputs. The output is eight scores, one per candidate for "the maximum". Softmax turns them into probabilities. The network is hand-built and untrained. A token's score is its count divided by four. For input
(2,2,7), token 2 scores 0.5, token 7 scores 0.25, and the rest score 0.It does not compute the maximum. It favors tokens that appear, and repeated ones most. The true maximum always appears, so it gets a small boost. It receives 15.3% probability on average, against 12.5% for random guessing. The average loss is 1.885, against 2.079 for random guessing.
Results
Method
Mathematical step
Proven loss bound
Model evaluations
Brute force (all inputs)
Average the loss over all 512 inputs
1.885261388
512
Convexity
Replace distinct smaller tokens by repeated-token endpoints
1.891214817
64
Factorization
Sum each group by formula, then apply Jensen's inequality
1.885274023
8
Bounds are rounded up. Factorization uses 8 times fewer evaluations than convexity. Its error is about 471 times smaller.
Arguments
Brute force averages the loss over every input.
Convexity. Take three different tokens a < b < m, where m is the maximum. Their scores are the average of the scores for (a,a,m) and (b,b,m). Loss is convex in the scores, which means a bowl-shaped curve. So loss(a,b,m) ≤ [loss(a,a,m) + loss(b,b,m)] / 2. When we know convexity is there, we have 64 inputs to run.
Factorization. Let Z be the sum of exp(score) over the eight tokens, which is softmax's denominator. Because exp(a+b) = exp(a)·exp(b), Z splits into products with one factor per position. The inputs whose maximum is exactly m are those with every token ≤ m, minus those with every token ≤ m−1. Each group is summed by formula. The loss contains log Z, and the log of an average is at least the average of the log. The upper bound is:
L ≤ Σₘ pₘ · log E[Z | max = m] − T
Here pₘ is the probability that the maximum is m, E[Z | max = m] is the average of Z over inputs whose maximum is m, and T is the average score of the correct answer.
Automated Search
One proposal went through one full cycle. The reviewer caught three implementation problems. The idea itself needed no change.
Limits
A simpler exact argument beats this one on this network. It sorts inputs into three repetition patterns: all equal, two equal, all different. It runs one example of each and counts. That is exact with 3 evaluations. So this result shows that the process works, not that this is the best proof.
The identity relies on scores that add across tokens. Attention and other nonlinear networks breaks this.
A tighter proof is also not automatically a better explanation. ARC's surprise accounting scores explanations in bits. By my count, using my own conventions, just stating a single number like this loss is cheapest, at about 15 bits. An explanation pays off only when it explains more than it costs.
Next steps are to test on trained models, and
Where this comes from
The ILIAD Intensive worst-case interpretability course (exercise notebook) supplies the brute-force baseline, the convexity method and the idea behind the three-pattern comparison. The course builds on the Compact Proofs paper. ARC's post supplies surprise accounting. The Count-Softmax network and the agent setup are the author's. The factorization argument was produced by Codex. AI use. Text inside Arguments block was drafted by Claude and edited by me. I have checked the numbers. The factorization argument and its implementation were produced by Codex agents.