"... the strongest configuration fully solves only 27 of 43 instances in code-and-proof mode and 10 instances resist every configuration in both modes. The gap is not local proof skill but repository-scale organization. The strongest agent pass over 80% of individual specifications yet fails to discover shared invariants, build the reusable lemma libraries that deep specifications require, and keep the whole repository consistent and buildable."
3
Replies
0
Boosts
@regehr I tried something analogous recently with a newer model (GPT-5.6 Sol, various effort levels) and a variety of libraries/techniques (test libraries like Hegel, Insta, QuickCheck, etc., as well as things like Lean, ACL2, various SMT solvers, Verus, Spin, etc.) and agents were pretty bad at using these things effectively without explicit instructions.
I guess I should write this up, but my to-do list is overflowing with things I should write up.
@regehr I thought this was interesting. This will depend on the problem, but except for problems where you go from zero to non-zero or near zero to not-near zero, where this almost has to be the case, I've found the opposite.
I'm not sure why this is the case; we're using fairly different setups, so maybe it has something to do with that? It could also be a coincidence.
@danluu yeah I don't know! but super interesting
