7 ms·
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI
by d0mine 5d ago
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs.
It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
- thaumasiotes 5d agoIt's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".
- stbede 4d agoThe opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.
- whateverboat 5d agoLLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
- margorczynski 5d agoThis is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.