Comment by y1n0
6 hours ago
A little before that was:
> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.
> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.
- - -
This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.
If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.
One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people
Nobody (sane) does that.
Lots of people have the implementer write the tests. But this only seems like a bad thing because of an unfortunate terminology collision:
- Microsoft culture: tests are adversarial verification.
- Google culture: tests are executable documentation.
Both of these things are important. It's really unfortunate we call both of them "tests".
At Microsoft, (verification) tests are written by a different engineer than the one who wrote the code under test. VLSI/Hardware works like this too.
At Google, (documentation) tests are written by the person who wrote the code, because it's their job to document it, and because the point of documentation-tests is to make sure other people who modify your code don't break it.