How well do agents use test/verification techniques?

Overall, I think the IMAP results were less interesting. I thought it might be more interesting to try since it's more of a "business logic" problem, but not as huge and expensive to run as the pandoc eval we look at when we looked at languages, which costs over $1k in API costs per run for some of the less effective languages, and was still $700/run in Rust to get to only 30% passing tests (note that this eval uses a much harder metric, of fraction of runs that achieve a perfect score). In the IMAP eval, only a single run achieved a perfect score ("Make no mistakes", on medium). In general, there were some bits of logic that were, apparently, too tricky for 5.6 Sol to one-shot. I suppose one way to look at it would be that Make no mistakes dominated with a 2.5% score on medium vs 0% for all other conditions. Finally, evidence that "Make no mistakes" works! If we instead look at average score which, prima facie, sounds more reasonable, formal methods conditions do somewhat better than the various property based testing conditions. However, we didn't look at this in detail because I was trying to write this post in half an hour and went way over budget. And it turns out that, overall, average score is less meaningful for the IMAP condition than in the Zstd condition because the tests weren't independent (the tests are series of operations, and failing an early operation in the series would then render a 0 score to the rest of the operations). That's not a great way to score if you want to compare functionality, but I asked agents to come up with the tests and, as we've noted in many other recent posts, SOTA models aren't good at coming up with benchmarks and the time it would take to fix this would be well beyond what I want to put into this at the moment. In order to get remotely reasonable scoring out of the Zstd eval, I had to fix up a bunch of incorrect things agents set up (I re-used this eval here because that saves having to do more that kind of work), and from looking at the raw score of the IMAP eval, the score is close to meaningless and it would take probably take a substantial amount of work to make the score meaningful. However, we can look at what agents actually did, in which case we see something like we saw here, that agents failed to use each technique effectively just as in the Zstd eval. I already noted how, for the Zstd eval, you shouldn't read too much into the score/ranking and the part that I find interesting is how agents failed to used named libraries and techniques reasonably; the same thing is true of the IMAP eval, but even more so, and I think the interesting part of the story there is on a more "business logic" / "protocol" problem, agents also failed to use testing and formal methods effectively without guidance. One thing that's true of all the evals I tried for this is that they're RFCs, which are highly unrealistic, but the way in which they're highly unrealistic is that the specs are much clearer, more detailed, and less ambiguous than the specs virtually all programmers give to agents when they ask an agent to implement something. I would expect that the failure modes we've seen here are the same or worse on most real-world problems. [return] Overall, I think the IMAP results were less interesting. I thought it might be more interesting to try since it's more of a "business logic" problem, but not as huge and expensive to run as the pandoc eval we look at when we looked at languages, which costs over $1k in API costs per run for some of the less effective languages, and was still $700/run in Rust to get to only 30% passing tests (note that this eval uses a much harder metric, of fraction of runs that achieve a perfect score). In the IMAP eval, only a single run achieved a perfect score ("Make no mistakes", on medium). In general, there were some bits of logic that were, apparently, too tricky for 5.6 Sol to one-shot. I suppose one way to look at it would be that Make no mistakes dominated with a 2.5% score on medium vs 0% for all other conditions. Finally, evidence that "Make no mistakes" works! If we instead look at average score which, prima facie, sounds more reasonable, formal methods conditions do somewhat better than the various property based testing conditions. However, we didn't look at this in detail because I was trying to write this post in half an hour and went way over budget. And it turns out that, overall, average score is less meaningful for the IMAP condition than in the Zstd condition because the tests weren't independent (the tests are series of operations, and failing an early operation in the series would then render a 0 score to the rest of the operations). That's not a great way to score if you want to compare functionality, but I asked agents to come up with the tests and, as we've noted in many other recent posts, SOTA models aren't good at coming up with benchmarks and the time it would take to fix this would be well beyond what I want to put into this at the moment. In order to get remotely reasonable scoring out of the Zstd eval, I had to fix up a bunch of incorrect things agents set up (I re-used this eval here because that saves having to do more that kind of work), and from looking at the raw score of the IMAP eval, the score is close to meaningless and it would take probably take a substantial amount of work to make the score meaningful. However, we can look at what agents actually did, in which case we see something like we saw here, that agents failed to use each technique effectively just as in the Zstd eval. I already noted how, for the Zstd eval, you shouldn't read too much into the score/ranking and the part that I find interesting is how agents failed to used named libraries and techniques reasonably; the same thing is true of the IMAP eval, but even more so, and I think the interesting part of the story there is on a more "business logic" / "protocol" problem, agents also failed to use testing and formal methods effectively without guidance. One thing that's true of all the evals I tried for this is that they're RFCs, which are highly unrealistic, but the way in which they're highly unrealistic is that the specs are much clearer, more detailed, and less ambiguous than the specs virtually all programmers give to agents when they ask an agent to implement something. I would expect that the failure modes we've seen here are the same or worse on most real-world problems. Funnily enough, when I asked ChatGPT to fact check this, it told me that this paragraph was wrong because there are papers that show that people have used RL environments to train agents to test, and then linked to three papers that trained agents to write poor tests by training them to write unit tests like most programmers do. That's exactly the kind of thing that I would expect to lead to the kind of poor testing we see LLMs do today, where it takes a human who understands more effective test techniques to steer the agent. In multiple independent subfields where people care about correctness, folks have independently converged to a few sets of related techniques that are generally the opposite of writing small unit tests. Of course training agents to do this thing that's the opposite of what people do when they're serious about correctness isn't likely to result in good correctness. There is some work related to RL environments and randomized testing, such as this paper, but based on how ineffective models are at any of {PBT, fuzzing, randomized testing, etc.} without specific guidance, it doesn't seem that this has made it into the training of the models from the big AI labs in a serious way. [return] Funnily enough, when I asked ChatGPT to fact check this, it told me that this paragraph was wrong because there are papers that show that people have used RL environments to train agents to test, and then linked to three papers that trained agents to write poor tests by training them to write unit tests like most programmers do. That's exactly the kind of thing that I would expect to lead to the kind of poor testing we see LLMs do today, where it takes a human who understands more effective test techniques to steer the agent. In multiple independent subfields where people care about correctness, folks have independently converged to a few sets of related techniques that are generally the opposite of writing small unit tests. Of course training agents to do this thing that's the opposite of what people do when they're serious about correctness isn't likely to result in good correctness. There is some work related to RL environments and randomized testing, such as this paper, but based on how ineffective models are at any of {PBT, fuzzing, randomized testing, etc.} without specific guidance, it doesn't seem that this has made it into the training of the models from the big AI labs in a serious way.