Test and verification technique effectiveness with GPT-6 Astra

When we looked at how well agents used test/verification techniques in August¹, 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:

1. Astra's capability has increased by enough that we need a more difficult eval (on the Zstd implementation eval, almost every condition gets 100% correctness almost every time on medium regardless of technique)
2. Agents seemed to use test and verification techniques more effectively

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 did².

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:

1. Almost no condition outperformed Default
2. On other evals (not discussed in detail), similar prompts also did not outperform Default
3. The tests produced by non-Default conditions were mostly ridiculous and didn't capture the value of the technique

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 large number of conditions that outperform default makes it plausible that many conditions outperform 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:

1. To what extent can these results be extrapolated to running more turns to get to near-complete correctness for Pandoc? In general, conditions do maintain something like their rank order with additional turns, so it's plausible the ranking will continue as-is, but this is untested
2. How much of the results are due to a small sample size (with respect to each condition)? For the Pandoc eval, we "only" ran each condition 25 times. Many different turns were run, but we know from previous experiments as well as just using agents that there's a high degree of path dependence when looping over generated code
3. How much of the results are due to a small sample size (with respect to minute / trivial variations)? From having run a few silly evals, I know that it's possible to get very different results when asking for the same thing due to trivial changes (such as changing sentence structure, changing capitalization, etc.); how much of the current results are due to something arbitrary like this?
4. How much of the results are due to a small sample size (with respect to the problem being solved)?

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/mo of MSRP token spend. Getting to 100x isn't plausible with a setup like that, but 2x to 3x could be done with testing expanded in a limited fashion and some guesswork and extrapolation. I don't know that it really makes sense for me to do that given how much time it would take and how little spare time I have, but considering what kinds of things academics have looked at when studying programming productivity, maybe it makes sense for a grad student to do this, since it would be more informative than a number of widely cited studies. But, in industry, I'm not sure who would do this outside of an AI lab. That being said, if you keep in mind that we don't know how well any of these results generalize, I'll note a few things that I thought were interesting.

1. Differential testing caused agents to examine tests and invariants in a way that engendered better "understanding" than other conditions
2. TDD once again underperformed, but not all conditions that caused agents to write a lot of small tests underperformed
3. ACL2 (a theorem prover) performed well (it also performed well in the 5.6 Sol Zstd eval )
4. Property-based testing (not the named condition, but a number of libraries that force the use of the technique) finally resulted in tests that do what one might hope from PBT

(1): I tried to get agents to do this with the hastily written skill I wrote for the 5.6 Sol Zstd eval; although the skill performed decently, agents basically didn't do this. However, for the Pandoc eval, differential testing did cause agents to closely examine boundary conditions and figure out how to write tests (and therefore how to write code) that correctly implements both sides of the boundary. I'm not confident that this generalize, but it would be interesting to see if it does generalize and what else can get agents to do this kind of thing systematically.

(2): Although TDD underperforming is exactly what I'd expect (recall that I added TDD to the 5.6 Sol eval because I thought it would underperform), the lack of underperformance of other conditions that cause many small tests to get generated should reduce confidence in the plausible sounding reason that writing many small tests underperforms.

(3): I've felt for a long time that ACL2 is underrated relative to other verification tools (it was heavily used to good effect in industry in some areas relative to the amount of academic work on it). I had low confidence in this opinion and continue to have low confidence, but it has performed well in evals I've done so far. Given how much effort is being poured into getting agents to use Lean effectively, I'd expect that Lean will eventually outperform ACL2 even if ACL2 outperforms today, but ACL2 doesn't seem like a bad choice today. For people doing verification or proofs with Lean 4, I'd be curious how the results compare to using ACL2.

(4): Yay (perhaps). For all the reasons I noted above, I have low confidence that this generalizes, but Proptest once again performed well. And, this time, the testing was a lot better than we saw in the 5.6 Sol Zstd eval. I have no inside information on this, but I would guess that there wasn't a major effort on improving PBT / fuzzing / etc. between 5.6 Sol and 6 Astra and that this comes out of better generalization and higher capability. If that's true (and this isn't just some artifact of my only spending $90k MSRP and not $9M MSRP), this bodes well for better testing in the future in that we should expect models to get better at testing without any particular effort to improve testing capabilities.

Between my running these tests and publishing this post, a claim that you should tell agents not to write tests (based on running DeepSWE) went viral. The specific claim was

ok it's official...[ellipses from original quote] AI-written unit tests and integration tests are empirically proven to be unhelpful. you should tell your agents to stop writing tests by themselves

As we previously noted, I find DeepSWE unrepresentative of work that I do and therefore meaningless to me personally. Additionally, that was done with Sonnet 5.5 High, so it generally only passed on problems that are much easier than the problems discussed here, and as observed here and in other recent evals, which techniques are effective often doesn't generalize across problem size or problem difficulty. I find it plausible that for problems coding agents find very easy, telling them not to test reduces cost (which is what was actually shown conditional on someone caring about DeepSWE). Generalizing this to "AI-written unit tests and integration tests are empirically proven to be unhelpful" based on the test that was run seems wrong regardless of whether or not this holds for other problems, and it seems unlikely that the claim holds. The claim was based on asking for no tests, which resulted in similar correctness and a small cost savings (9%, on average). In our tests here as well as before, we find differences in correctness as well as a larger than 9% difference in cost, so it seems unlikely that a claim like "AI-written unit tests and integration tests are empirically proven to be unhelpful" based on a 9% difference in cost on a benchmark of small problems is correct. Another thing to note is that DeepSWE's grader is broken with respect to testing because (among other issues), an agent can add a test name that conflicts with a grader's secret test name, which will then cause a failure. Given issues like that, adding tests is inherently penalized in a way that isn't representative of real-world usage.

You can argue the claim was highly effective, in that making overstated claims that something is empirically proven is a good way to go viral or get a lot of citations, but it's not a good way to figure out how to use coding agents effectively.

In Nolan Lawson's recent post on how JavaScript framework choice impacts agents, he noted: My goal here is not to write the end-all-be-all benchmark for “I’m a vibe-coder, which framework should I choose?” The point of this post is to demonstrate that it’s possible in the era of AI coding to still make decisions based on evidence rather than vibes.

I feel the same way here, in that I think it's valuable to run some toy evals and see what the results are. Even if someone had the resources of an AI lab available to them, I don't think they could say that X or Y are "empirically proven to be unhelpful [or helpful]", but we can still get some kind of information.

From what we've seen in our testing evals, I'd be inclined to try proptest if I wanted a property-based testing library in Rust, and for any problem that I'd use Lean on, I'd be inclined to try ACL2 as well to see how results vary and if I get better results, and there's also a fair amount of information that fits into some kind of vibes-based feel for things. As I've noted in my N most recent posts, I've been trying to write up each of these in 30 minutes because there are too many results to write up and not enough time, so I'm not going to provide an accounting of what happened for each condition like I did for the 5.6 Sol Zstd eval. I'm already over 30 minutes on this post, so I'll stop here and perhaps we'll look more into testing and verification in a future post.

Thanks to Laurence Tratt and Marco Primi for comments/corrections/discussion.

Appendix: why don't AI labs publish more comparisons on what techniques are effective?

Unlike us randos, they actually have the resources to run relatively comprehensive evals and there's a general lack of information about what's effective. If people understood how to use AI better, it seems like that would result in more AI usage. Also, my experience has been that different techniques are effective with OpenAI's models vs. Anthropic's models. If one of these companies published good information about what works with their models, that could move people towards interacting with agents in a way that's advantageous for them.

I guess the case against this is something like, revenue growth is so rapid that more money can be made by doing other work and/or differences in how people prompt don't really matter anyway. As someone on the outside of these labs, the former seems plausible to me, whereas the latter doesn't seem like it can be true (because I've repeatedly observed reasonable people who aren't doing obviously silly things get very different results, to the point where one person might fail to get a working solution to a problem where another person easily makes things work).

Appendix: agentic testing comments

David R. MacIver noted:

Btw one thing I'm noticing in my evaluations on the skill is that ChatGPT is way less into PBT than Claude is. Claude will pretty eagerly write property-based tests and seems to benefit from them during development in my current benchmarks, but ChatGPT sol doesn't do that unless you're really insistent. So there might be some prompt sensitivity going on here, or it might be model specific.

I haven't done the same breadth of testing with Claude. Given what MacIver said, it's plausible that Claude is better at property-based testing. Also, given that he develops Hegel and is generally using Claude, it's also plausible that Hegel works better with Claude than with Codex and we'd see better results from Hegel if we tried with Claude.

Roman Leventov commented:

Hi Dan, I was encouraged by your post about ai-coding to try fuzz/generated testing.

A part of a system I develop has a statechart-like architecture. Think of it as a support chat where automation could suggest actions or messages for support agent (human) to send to the user. LLM is not used to author messages, but just to classify some of the support intents, but state transitions are deterministic. There could also external events about the subject of the ticket that materially affect possible next actions or decisions. All of this gives rise to a rich statechart system. It is written in TypeScript.

So I had to rewrite a significant chunk of that system so to derisk rewrite but also to try fuzzing I decided to go with it during the rewrite. I used sol xhigh for the first 5 days of the rewrite, then mostly astra medium or high for 4-5 days more (it was around astra release). I instructed agent to develop generate traces of all the possible kinds of events and effects that affect the logic.

For the first 4 days it couldn't make the generated testing system find a single de novo defect that agent reviewers themselves didn't find first. I always use my approach where I define many angles/scopes/areas of review (for this rewrite there were about 15), make agents generate quite detailed prompt for these areas based on my templates, then start subagents in these areas with verbatim prompts in the areas as long as they find any defects or things to fix. In total throughout the whole rewrite, agent reviewers found about 210 bugs/defects, generated tests took off the ground a bit towards the end and produced about 20 de novo defects that agents themselves didn't notice. In total about 230.

Production code change was about 30k lines, the generated testing harness and everything that was written specifically to support this generated testing approach was about 300k lines at the end. Probably it was very ineffective, but I didn't look into it.

After the deploy, there were a few (4-5) very "stupid" bugs that you would think a process that run well over 100 agent reviewers and found 230 bugs couldn't have missed. Still, I consider this a good result for a rewrite of such a complex statechart system.

Overall I consider this a negative result because generated tests helped find just 10% of the defects, and required gargantuan amount of code (300k lines) and agent tokens to develop and support.

I think this is interesting and I would love to see more people writing up case studies of what they observe.

1. The post was published in September, but the tests were run in August. ^[return]
2. One I heard recently is that Rust is particularly good for agents because it has nice errors that guide agents toward the correct solution. I've seen this mentioned a few times and, while I'm not going to say this absolutely can't be true as, perhaps, a large scale set of evals that I can't really afford to run might be able to find some kind of effect, I've looked a lot harder at this than anyone who I've seen make this statement and it doesn't seem to be true for any problem that I've looked at, at least at a sample size that I can afford to run. If the statement is true, its effect seems dominated by other factors in most circumstances, so it shouldn't be a reason to choose a language; it seems like the wrong thing to mention if you're going to give a single reason Rust is a good agentic language (which is what happened when I last saw this come up). Another thing to note here is that the plausible "human sounding" reasons for effectiveness are probably just as untrue when evaluating humans; it's just that we can't afford to run the human eval, so people pass around these irrefutable but also unsupported reasons. Recall that we looked at the literature on the effectiveness of static vs. dynamic types because people frequently said that studies show that static types are more effective than dynamic types, but the evidence for this claim was nearly non-existent when we looked at the major studies that had been published at the time.^[return]

source & further reading

danluu.com — original article Bad benchmarks and evals: Senior SWE-Bench, napkin math, and winter tires How well do agents use test/verification techniques? How accurate have Ed Zitron's AI skeptic predictions been?