mkarrmann
Joined 4 years ago
Joined 4 years ago
1. I responded to the quote and thread tokepi posted. I stand by that response—the supposed "prompt injection" was a trivial misunderstanding which Meta had already publicly clarified.
2. You sarcastically replied by linking me to another comment that said "pop up to that -er- blog's top level, scroll back until you find the start of the investigation, and then start reading." I read that as the top of the linked thread. You meant his profile page, which would have meant reading everything he'd posted since the investigation began to find the posts you had in mind, which came days later in separate threads. I noted I didn't read everything he wrote, clarified what I did read, and asked you to state your specific concern.
3. You didn't state it. You linked five more posts on issues unrelated to the thread I'd responded to. I acknowledged I hadn't seen those, said they were at least not trivially confused the way the first thread was, and bowed out because I shouldn’t discuss specifics of my employer’s security setup beyond what's been publicly disclosed (for obvious reasons).
4. You responded with more sarcasm and a lecture on "netiquette". Then you finished by explaining "prompt injection", which is strange: even @jonny acknowledged the supposed prompt injection from the initial thread was intended behavior, and the posts you linked provide no evidence of prompt injection. So you bringing it up calls into question whether you were actually parsing our conversation and jonny's investigation.
5. I tried twice to end this amicably. Both times you came back with insults and more lectures.
Do you think you upheld your own standards of "netiquette" and "healthy discourse" here? How is being simultaneously antagonistic while refusing to articulate your own perspective helpful to anyone?
I agree with Jtarii that it's very unlikely a Lean bug is critical to most of these proofs. But we're in strange times, so I agree wtih the sentiment that we should wait for further analysis before declaring complete confidence in the proofs.
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.
Nice Aurelius quote, I'll remember that one
Like I mentioned I don't work on Muse, and I suppose it'd wouldn't be appropriate for me (self-identified Meta employee) to publicly speculate on what defenses do and don't exist or what is intended. (sorry kinda a cop-out, I know).
Thanks for providing specific links to the specific concerns being raised.
TBH I saw none of those comments by scrolling forward or backwards from the original link. Now it turns out I supposed to be checking quote tweets, not just scrolling like you said above? (tbf I'm not familiar with the neuromatch UI, could be user error on my part).
Again, I think this would've gone smoother if you actually articulated the problem you're concerned about, instead of linking to a "personal notepad" which you acknowledge has mistakes and isn't easily intelligible, and then blaming me for missing the actual point.
I'll look through these new comments later.
Edit: I see from your original comment what you meant by "top-level". I originally assumed you just meant top of the thread. I'll take the L here.
a) More being surprised the muse will just provide internal details (which again, as intended) b) the bash scripts are ugly (okay? I don't think that's what we're arguing about) c) surprise that muse runs as root (then realizing this is explained by the VM-in-VM model and linking to the blog which explains this) d) surprise that muse can run as a seed box (idk is this supposed to be the security concern?)
Could you please be more specific about which part you're concerned about? I think that'd be more productive than linking to a long thread, me responding to what I see, then being told that it's just a scratch pad and I'm silly for taking it seriously but also if I look closer I'll see the deeper truth.
I think you're saying that prior actions justify the beliefs you hold. Fair enough, I'll concede that for the sake of argument.
My above comment still stands. Even if your beliefs are justified, that doesn't mean you should treat non-evidence as evidence supporting your beliefs. (Tbh my point is kinda trivial/pedantic. But I feel like folks just always want to double down that every criticism of meta is correct).
You're free to believe whatever you want about Meta. But no, you shouldn't point to non-evidence, interpret it through the lens of your prior beliefs, and then claim that it's actually evidence supporting your beliefs.
> Aside, if “a skill file organizing purchase history in markdown format” is the only thing you took away from that thread, you might want to take a closer look.
That's what that specific quote I was referencing was referring to. I already responded to the supposed prompt injection/security concerns above.
But if someone posts the thread with no other context than "check this out", then it seems appropriate explain this missing context.
And for the record, I did scroll back read through what he's saying as you suggested. The broader context is exactly what makes it clear he's just a bit confused about what he's "uncovered". (Obvious caveat: I haven't read through everything this guy has written, I could be missing something)
How much of this progress do you honestly think is explained by scooping unreleased work? Feels strange to still be bringing up this theory.
[^1] Obviously this is somewhat debatable, especially for P = NP, depending on how one defines "toward a solution". Without quibbling over semantics, something along these lines clearly holds.