Sanjeev Arora called the mathematical model's leaderboard performance unimpressive.
This is not impressive compared to current models on the leaderboard https://trishullab.github.io/PutnamBench/leaderboard.html
Leanstral 1.5 shows the strongest test-time scaling we have seen from a formal-reasoning model. The figure below tracks Pass@8 on PutnamBench as we raise the token budget per attempt from 25k to 4M: performance climbs smoothly the whole way.
No Digg Deeper questions have been answered for this story yet.
@prfsanjeevarora 👀
This is not impressive compared to current models on the leaderboard https://trishullab.github.io/PutnamBench/leaderboard.html
It’s much cheaper than Aleph Prover and Seed Prover high (and beats seed prover high which uses 10 H20 days per problem)!
It’s also better than Goedel Architect without NL solutions provided and a tiny bit worse with, using no special scaffold (you run the code agent with compaction and that’s it)!
Agree that it doesn’t move the frontier in number of Putnam problems solved which is why we put the Aleph Prover in the main plot!
