Test and verification technique effectiveness with Astra

When we looked at how well agents used test/verification techniques in August1, we saw that GPT-5.6 Sol generally did what you might call a caricature of various techniques when asked to use a technique or library such as TDD, QuickCheck, Lean 4, etc.; not specifying any particular test method (which we'll call Default) resulted in many worthless unit tests, which was one of the best performing conditions because asking agents to test in specific ways mostly made them worse. In that eval, we gave agents the Zstd RFC and asked them to implement Zstd (with an addendum for how they should test for all conditions other than Default).
On re-running the same eval with GPT-6 Astra, we see two big differences:
On (1), we previously saw that, when implementing Zstd from the RFC with 5.6 Sol, on average, agents spent $3.50 on medium effort and $5.50 on xhigh effort to get full (holdout) test correctness about 63% and 77% of the time, respectively. With Astra, agents cost $1 to get full test correctness over 99% of the time at medium effort.
On (2), an example would be that when we asked 5.6 Sol to do fuzzing, it would generate many worthless random inputs, which would mostly hit the same code paths and not test anything interesting. With 6 Astra, we see agents that are asked to do fuzzing in a structured way that actually exercises code paths and finds non-trivial bugs, but we can't tell if this improved correctness or not because the Zstd implementation benchmark is saturated.
We also tried giving 5.6 Sol the IMAP RFC, but it was too hard for 5.6 Sol. When trying again with 6 Astra, we get the following distribution of results (the y-axis is the percent of runs where all tests pass; agents are not given the tests and the points are the results across 80 runs of each condition).
Default once again looks pretty good. Some conditions result in somewhat better correctness, but also with higher cost. Although the IMAP RFC isn't saturated, it would be nice to also see results on a harder task since most of my time goes to tasks that agents can't one-shot most of the time. To test this, we'll try the pandoc eval we looked at when comparing programming languages. A reason I want to see results on larger evals is that, as we observed when looking at caveman mode and as we saw with languages, models often perform fairly differently on larger tasks. With caveman mode, the large wins that people reported became smaller or disappeared and with languages, we saw this in multiple ways, such as C and C++ implementations of Zstd being at least somewhat ok on memory safety, whereas C and C++ implementations of Pandoc were plagued by memory safety issues.
Pandoc is significantly harder, and even after running multiple turns (roughly 14 on average), no condition reached 100% correctness, so we'll look at the fraction of tests passed instead of fraction of runs that got to 100%.
For this, we only ran each condition 25 times due to the cost involved. At MSRP, this cost about $90k.
Recall that, in past evals we ran on languages and test/verification techniques, the failures were often idiosyncratic results of how agents operate, such as agents using Clojure writing incorrect byte conversion code by default or agents using Verus writing vacuous proofs. This kind of thing is quite different from the reasons I've seen people say that agents should use some particular language or test/verification technique, which are generally nice-sounding explanations for why something ought to be better that sound appealing in a very human way but appear to be unrelated to reality when we look at what agents actually did2.
Because we "only" ran $90k worth of evals here, we don't really have enough information to say why almost anything happened. We can observe that some conditions performed better than others, but it's difficult to say what it means. As a result, we shouldn't read too much into this, but we do see some things that seem consistent with what one might expect, in that we might expect most of the test techniques and libraries suggested to give better generalization, which would then give better holdout vs. test scores (result is up and to the left of the Default line when viewing visible vs. holdout test scores), with TDD giving worse generalization (down and to the right of the Default line).
But, if it's true that testing properties gives us better generalization and conditions like TDD that result in a lot of small tests give less general results, we'd expect the built-in condition to also have a low holdout:visible relative to Default and that's not what we saw. Why this is is unclear and I don't think we can really determine this without a lot more runs.
For the actual results, the line shown for cost vs. holdout and cost vs. visible show curves fitted to the shape of all graph trajectories across multiple turns, fit to Default. Things that are below / right of the line can be thought of as worse and above / left can be considered better. With 5.6 Sol, it was clear that the test conditions generally weren't doing useful work for a combination of reasons:
Here, we have a situation where many different techniques have a better result than Default. The conceptual error bars on each condition are quite wide (more so than indicated by the bootstrap intervals shown on the plots), but the number of conditions that outperform Default makes it plausible that one or more conditions truly outperforms Default even if we don't know which ones exactly. Furthermore, some conditions likely truly outperform other conditions, but we don't really have sufficient data to tell which conditions are generally better. It's much simpler when almost everything looks bad across a wide variety of techniques.
Here are some questions I have about the results:
If I really wanted to answer these questions, I'd want to run at least 100x what was run here to run the full matrix. Steve Yegge has mentioned using ~20 Claude subscriptions to spend ~$120k/