Everyone doesn’t seem to know that, because tests are often cited as a way to ensure that AI-generated code is correct.
back
1 comments
I was very excited about formal proofs, which are now very cheap to produce, in service of validating AI generated code.
But I had a funny experience recently where an agent implemented an entire feature completely wrong (exactly backwards, actually, in a way that defeated the purpose, introduced security issues etc.).
It happily supplied tests for the new functionality, and all the tests passed.
What I realized was, even formal verification wouldn't have helped here -- it would have just written a mathematical proof that the incorrect functionality was correctly implemented!
So there's a gap here, where first, the human's intention needs to be formally specified (by the human, or at least the human needs to be able and willing to verify it), and then the slopswarm can hack away at it...
> the human's intention needs to be formally specified
Yes, that has always been the case with formal proofs. Even a mathematical proof with Lean is useless if the proven formal statement doesn’t match what the mathematician meant. And that’s why humans working with formal languages won’t be going away. Natural language is imprecise by nature, even when we have precise ideas in mind. In that case, it’s often better to specify what we mean in a formal language than in natural language.
> first, the human's intention needs to be formally specified
This never changed with AI; in fact, I think it made this need more visible than it ever had been before. You can't get away with not being able to describe in detail what you want. As with working with humans, any ambiguities will be interpreted, and not always in the way you hoped.