This is a very common problem with LLM-generated code. 'Agents' run in a loop generating and refining code towards some set of constraints. Some of these are functional (does formal verification pass? Do tests pass?), others are performance goals. It's very common to see someone write a benchmark to test some feature and then see the 'agents' optimise for that microbenchmark at the expense of the common case. The same applies to the functional correctness things: code that is correct for all of the tests, but introduces new corner cases that the tests don't cover, or code that passes formal verification by exploiting some inadequate specification. The last one is not new: I particularly remember EverCrypt accidentally satisfying their 'no memory is accessed after it is deallocated' property by never deallocating memory, but LLMs do this at an impressive scale. They are machines for producing plausible sequences of tokens, not correct sequences.
Thanks for this, I wouldn’t have read it without your comment.
Unfortunately the back and forth isn’t very illuminating. The OP seems excessively dogmatic. But the question is how well the paper author’s approach will work in practice. The idea that you can specialize your DB to the customer is appealing, but even a real world customer isn’t guaranteed to be as predictable as a benchmark. Real users’ requirements are going to change, data distributions will shift.
I have a project of my own that has a risk/opportunity of “cheating in a principled way”—it compiles a separate class per regex, which means that I can theoretically have optimizations that are as narrowly scoped as I want. If the regex \${[a-z]+} turns out to be important for real world software, I could special-case it (and with AI, it’s pretty damn easy).
However, I have no interest in cheating benchmarks for the sake of cheating benchmarks. The goal is to make real world use cases better, and generality and not-micro-optimizing benchmarks helps.
david_chisnall | 10 hours ago
This is a very common problem with LLM-generated code. 'Agents' run in a loop generating and refining code towards some set of constraints. Some of these are functional (does formal verification pass? Do tests pass?), others are performance goals. It's very common to see someone write a benchmark to test some feature and then see the 'agents' optimise for that microbenchmark at the expense of the common case. The same applies to the functional correctness things: code that is correct for all of the tests, but introduces new corner cases that the tests don't cover, or code that passes formal verification by exploiting some inadequate specification. The last one is not new: I particularly remember EverCrypt accidentally satisfying their 'no memory is accessed after it is deallocated' property by never deallocating memory, but LLMs do this at an impressive scale. They are machines for producing plausible sequences of tokens, not correct sequences.
JulianWgs | 11 hours ago
Also look at the comments where the author of GenDB-V defends their work.
hyperpape | 10 hours ago
Thanks for this, I wouldn’t have read it without your comment.
Unfortunately the back and forth isn’t very illuminating. The OP seems excessively dogmatic. But the question is how well the paper author’s approach will work in practice. The idea that you can specialize your DB to the customer is appealing, but even a real world customer isn’t guaranteed to be as predictable as a benchmark. Real users’ requirements are going to change, data distributions will shift.
I have a project of my own that has a risk/opportunity of “cheating in a principled way”—it compiles a separate class per regex, which means that I can theoretically have optimizations that are as narrowly scoped as I want. If the regex
\${[a-z]+}turns out to be important for real world software, I could special-case it (and with AI, it’s pretty damn easy).However, I have no interest in cheating benchmarks for the sake of cheating benchmarks. The goal is to make real world use cases better, and generality and not-micro-optimizing benchmarks helps.