Figure:compression vs. correspondence. Each dot is a proof of the network's average loss. Further right means fewer model evaluations (more FLOPs). Higher means closer to the true loss.
For a simple enough toy network [1], can we use a consumer-level agentic setting to independently find arguments that can be translated to theoretical bounds around a quantity for performance?
This post presents the result of an agentic system automatically carrying the following tasks:
searching for arguments that utilises structure related to a quantity we care about (avg_loss) in a trained toy network (outputing the maximum value among all input tokens)
these arguments can be compact proofs fully expressible in mathematical formulas, while
this agentic system allows for the "relaxation" of it, i.e., heuristic argument (see ARC post) [2][3]
Implementing the proof/argument to bound the quantity of concern.
Analysing the result and passing to a gate—finish or to 1.
Each numbered point is the task for one agent.
Result
As shown in the figure, the green dot is an agents-found bound. It uses 8 evaluations instead of 512 (the amount of evaluations needed for a brute force proof); Compared to a known proof—convexity, it is a better approximation of the true value and uses less FLOPs at the same time. The table gives the exact numbers.
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
So we can use agents to automatically search, implement and compute bounds for quantities in a toy network.
Limitations & Further Steps
Generalisability tests on more networks, and the a scaling curve of complexity of these networks that is useful to scale the automated search method, is needed.
Safety-related quantity, under a simple enough setting, is needed to be tested.
This gives me relevant quantity to include in the claim [4]
Relaxing the proof lets the agents try approximate or non-rigorous arguments, which are cheaper to find and check than fully formal ones, as in the heuristic arguments ARC proposes.
Figure: compression vs. correspondence. Each dot is a proof of the network's average loss. Further right means fewer model evaluations (more FLOPs). Higher means closer to the true loss.
For a simple enough toy network [1], can we use a consumer-level agentic setting to independently find arguments that can be translated to theoretical bounds around a quantity for performance?
This post presents the result of an agentic system automatically carrying the following tasks:
Each numbered point is the task for one agent.
Result
As shown in the figure, the green dot is an agents-found bound. It uses 8 evaluations instead of 512 (the amount of evaluations needed for a brute force proof); Compared to a known proof—convexity, it is a better approximation of the true value and uses less FLOPs at the same time. The table gives the exact numbers.
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
So we can use agents to automatically search, implement and compute bounds for quantities in a toy network.
Limitations & Further Steps
Generalisability tests on more networks, and the a scaling curve of complexity of these networks that is useful to scale the automated search method, is needed.
Safety-related quantity, under a simple enough setting, is needed to be tested.
This gives me relevant quantity to include in the claim [4]
How simple it should be should be a function of the network complexity, time, and quality of bound.
However, the said agentic system doesn't estimate a suprise accounting as suggested in the same post.
Relaxing the proof lets the agents try approximate or non-rigorous arguments, which are cheaper to find and check than fully formal ones, as in the heuristic arguments ARC proposes.
Quantity
What it measures
This post
Network complexity
Tokens v, positions k, number of inputs vᵏ
v = 8, k = 3, 512 inputs
Verification cost
Model evaluations the proof needs, or FLOPs
512, 64, 8
Bound quality
Gap = bound − exact loss, plotted as −log₁₀(gap)
0.0060, 0.000013
Search effort
Agents, proposal cycles, implementation fixes, human interventions
3 agents, 1 cycle