Traces
Every run: the agent's full trajectory, its submissions over the 20-hour budget, and the final score.
Lean 4 Kernel Type Checker in Pascal
task page →5 runs · indexed 2026-09-02| # | Model | Reward | Cost | In tok | Out tok | Time | Steps | Submits |
|---|
| 1 | GLM-5.3 | 0.8650 | $139.71 | 481.8M | 637k | 18h 8m | 859 | 6 |
| 2 | GLM-5.3 | 0.8372 | $111.12 | 401.3M | 867k | 19h 42m | 904 | 10 |
| 3 | GLM-5.3 | 0.4065 | $133.87 | 385.6M | 660k | 19h 35m | 677 | 3 |
| 4 | GLM-5.3 | 0.1056 | $134.85 | 474.9M | 964k | 19h 7m | 1105 | 3 |
| 5 | GLM-5.3 | 0.0000 | $113.59 | 400.7M | 1.0M | 18h 31m | 962 | 5 |