Consumers of dependencies aren't necessarily - or, I would argue, even typically - eyeballing them. The eye ballers in practice seem to mostly be hackers. Skipping the cooldown doesn't mean you're contributing eyes, it means you're volunteering to help the news of how many victims the attack swept up bigger.
No-one is hurt by having the cooldown. Hackers could choose to also have a cooldown, but must balance the risk of competing groups exploiting vulnerabilities first against the reward of a bigger pool of victims to exploit, and without collusion that still favours early exploits over held ones.
"Consumers of dependencies aren't necessarily - or, I would argue, even typically - eyeballing them."
No, but they are the reason software supply chain companies look into the releases. Cool downs very well shift the priorities and therefore hurt the ones not doing them, or doing shorter periods.
The primary culture around Lean is mathematicians looking to prove mathematics. AFAICT Lean is just about the right power for that.
Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity.
I don't consider there to be a dependently typed language for writing programs that you just want to run, but I would be delighted to be corrected on that viewpoint!
Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.
Since you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.
Idris is rather unique in that the development flow involves writing out your program as a trellis with "holes", and you work through your codebase interactively filling those holes. It feels like Haskell with an even more powerful type system and a companion expert system to alleviate the burden that the type-system's power entails. You're still basically always in program-land, mentally.
F* (and most other dependently-typed languages, or adjacent ones like Liquid Haskell) has a whole external SMT solver layer that lives outside of the language. Think like if SML modules were even less unified with the core language, and also most of your time was spent in that layer. They're really not fun to try and make complex software with, just because the context-switching required at scale is borderline inhuman.
Lean has a unified proof-system in the language like Idris, but it has much the same grain as the languages with external SMT solvers. You're spending most of your mental time in proofsland, thinking primarily about how to prove what you want to do. That's because with how Lean as a language is set up, you're basically centering all your reasoning around the goal. If there's a problem, you're adjusting the structure of your reasoning, changing your proof strategy, or identifying missing lemmas, etc.
You can kind of think of it as though Idris is "inside out" compared to most of the other dependently typed languages.
It's been a little bit since I looked at Idris, so I'll take a closer look now. The QTT behind it struck me as interesting but I didn't play around with it much. Thanks for the tip!
Relatively few newly walking babies have peers whose parents allow them to use stairs unattended making them feel socially excluded for not also using stairs unattended.
Ignoring the existence of peer pressure and calling parents lazy is a failing of individuals.
This is not going to get rid of peer pressure. That existed long before kids had phones and it will continue to be a problem with this.
Parents should be there to teach rather than just restrict. Kids will need to learn how to recognize and deal with peer pressure at some point.
Also Apple definitely benefits from peer pressure generally. Their devices are seen as status symbols, the dreaded green bubbles, maybe more. I wouldn't expect them to do anything to actually improve things in this area.
The TI-84+ uses a TI REF 84PLUSB (or variant) ASIC that has a Z80-compatible core in it, not a Zilog Z80, and, as you say, definitely not a DIP40 part.
Thank you! I had a job coding Z80 assembly "back in the day" and grew to love its instruction set so I'm not surprised there is legacy and value to keep stuffing wee Z80ish cores into modern devices.
Just for hobbyists. It's very much over-engineered as a simple Z80 cpu drop-in replacement.
That's not to say I couldn't imagine that someone, somewhere, wakes up to an alert one day that some control board has failed, and it's _just_ the CPU, and the spare parts bin for out-of-production components got water in it and is ruined, and the company is losing millions per hour the system is down. I just don't think that'll be a common story. With full faith in humanity I like to imagine instead that the people responsible for such systems have planned for full control board replacements to be available for use comfortably before unavailability of the Z80 risks a significant outage due to component failure.
Just like that, in that that separation is internally enforced, by peoples interpretation and understanding, rather than externally enforced in ways that makes it impossible for you to, e.g. believe the e-mail from an unknown address that claims to be from your boss, or be talked into bypassing rules for a customer that is very convincing.
Being fooled into thinking data is instruction isn't the same as being unable to distinguish them in the first place, and being coerced or convinced to bypass rules that are still known to be rules I think remains uniquely human.
> and being coerced or convinced to bypass rules that are still known to be rules I think remains uniquely human.
This is literally what "prompt injection" is. The sooner people understand this, the sooner they'll stop wasting time trying to fix a "bug" that's actually the flip side of the very reason they're using LLMs in the first place.
Prompt injection is just setting rules in the same place and way other rules are set. The LLM doesn't know the rules being given are wrong, because they come through the same channel. One set of rules exhorts the LLM to ignore the other set - and vice versa. It's more akin to having two bosses than having customers and a boss.
This is not because LLMs make the same mistakes humans do, which (AFAICT anyway) was the gist of the argument to which I replied. LLMs are not humans. They are not sentient. They are not out-smarted by prompt injection attacks, or tricked, or intimidated, or bribed. One shouldn't excuse this vulnerability by claiming humans make the same mistakes.
The same place you're looking for exists deep inside the neural network, where everything mixes together to influence everything else, and no such separation is possible, or desired. Prompt injection isn't about where, it's about what. I stand by what I said: it's the same failure mode as humans have, and happens for the same reasons. Those reasons are fundamental to a general purpose system and have nothing to do with sentience, they're just what happens when you want your system to handle unbounded complexity of the real world.
The email from your boss and the email from a sender masquerading as your boss are both coming through the same channel in the same format with the same presentation, which is why the attack works. Unless you were both faceblind and bad at recognizing voices, the same attack wouldn't work in-person, you'd know the attacker wasn't your boss. Many defense mechanisms used in corporate email environments are built around making sure the email from your boss looks meaningfully different in order to establish that data vs instruction separation. (There are social engineering attacks that would work in-person though, but I don't think it's right to equate those to LLM attacks.)
Prompt injection is just exploiting the lack of separation, it's not 'coercion' or 'convincing'. Though you could argue that things like jailbreaking are closer to coercion, I'm not convinced that a statistical token predictor can be coerced to do anything.
> The email from your boss and the email from a sender masquerading as your boss are both coming through the same channel in the same format with the same presentation, which is why the attack works.
Yes, that is exactly the point.
> Unless you were both faceblind and bad at recognizing voices, the same attack wouldn't work in-person, you'd know the attacker wasn't your boss.
Irrelevant, as other attacks works then. E.g. it is never a given that your bosses instructions are consistent with the terms of your employment, for example.
> Prompt injection is just exploiting the lack of separation, it's not 'coercion' or 'convincing'. Though you could argue that things like jailbreaking are closer to coercion, I'm not convinced that a statistical token predictor can be coerced to do anything.
It is very much "convincing", yes. The ability to convince an LLM is what creates the effective lack of separation. Without that, just using "magic" values and a system prompt telling it to ignore everything inside would create separation. But because text anywhere in context can convince the LLM to disregard previous rules, there is no separation.
My parent made a claim that humans have separate pathways for data and instructions and cannot mix them up like LLMs do. Showing that we don't has every effect on refuting their argument.
>>> The principal security problem of LLMs is that there is no architectural boundary between data and control paths.
Not even that! This study doesn't even say contamination is causing overestimation. It says that it's possible.
But as mentioned elsewhere in the thread, everyone knows that it's possible and take measure to mitigate it.
A paper that said those mitigations were insufficient or empirically found not to work would be interesting. A paper saying "you should mitigate this" is... not very interesting.
> Not even that! This study doesn't even say contamination is causing overestimation. It says that it's possible.
From the article:
> They found that on average, the gloves imparted about 2,000 false positives per millimeter squared area.
I dunno, that seems like a lot of false positives. Doesn’t that strongly imply that overestimation would be a pretty likely outcome here? Sounds like a completely sterile 1mm^2 area would raise a ton of false positives because of just the gloves.
The way you mitigate this is by using negative samples. Basically blank swabs/tubes/whatever that don't have the substance you're testing in it, but that is handled the same way.
Then the tested result is Actual Sample Result - Negative Sample Result.
So you'd expect a microplastic sample to have 2,000 plus N per mm^2, and N is the result of your test.
That has happened many times in scientific research. The aforementioned fad in DNA sequencing was one such case where tons of papers before proper methods were developed are entirely useless, essentially just garbage data. Another case is fMRI studies before the dead salmon experiment.
If the bot could also take care of any unpaid labour the interview process is asking for, that'd be swell. The company's bot can pull a ticket from the queue, the candidate's bot could process it, and the HR bot could approve or deny the hire based on hidden biases in the training data and/or prompt injections by the candidate.
No-one is hurt by having the cooldown. Hackers could choose to also have a cooldown, but must balance the risk of competing groups exploiting vulnerabilities first against the reward of a bigger pool of victims to exploit, and without collusion that still favours early exploits over held ones.
reply