Middle may be wrong (it is a marketing trick to add 3rd outragesly expensive option, to make 2nd option look reasonable). The correct answer is “it depends” (even how long you should spend on choosing may depend on context too).
For example, write in whatever language you know best, then translate to a more appropriate language using LLMs once the desired behavior can be checked automatically. It is a tactic that works in some cases.
It can be used as a marketing trick, possibly because of the logic in GP post. Marketing people use this to trick people, which is different from it being a marketing trick in and of itself.
At the moment, the hurdle is [missing] context [aka shared model/understanding of the business, common sense].
Though it is not hard to imagine that any and all communications being recorded for AI consumption in the future.
The Next one is the relative lack of prompt feedback (expect the blowup in finite time like Navier-Stokes ;) [there is not much feedback even for humans at middle management positions].
The cost [tokens] might become prohibitive unless LLMs improve further [not a guarantee].
Is the implication that those who impose these sanctions can MITM anybody in the world except for countries under sanctions (which have to use their own root CAs)?
I've only heard of OpenAI and Anthropic agents hacking during training. Are open weights model not smart enough to hack Hugging Face to copy solutions? (doubtful)
MAD is a belief system. It doesn't matter whether AI can effectively stop the retaliation, it is enough that people making the decisions believed that it can (are we there already?).
It is not “worst-case” (as the post demonstrates, you can get worse results by using specifically crafted data that exploits hash collisions). There are algorithms that can get you O(logN) instead of O(N) even on such data.
> 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.
This 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.
The 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.
It won't be surprising if the requirement comes from some alphabet agency.
reply