No LLM can help companies that didn't care about software quality in the first place. If they did, they wouldn't have fired QA testers. And now that they've been gone for a decade while revenues have soared, why would they bother using LLMs for QA testing when they could execute on the stakeholder's vision instead!
You'd expect to see the majority of benefit to independent devs who previously _couldn't afford_ QA or a full team, and now can. But since the target audience for this stuff is niche, you're less likely to hear about it unless you're plugged into the subcommunities (see e.g. how LLMs have helped with game preservation, retrogaming).
I think incompleteness theorem means that you can't guarantee the agents will always be able to converge on a proof, since you can't have both completeness and soundness (and we obviously need soundness since that's the whole point of a theorem prover).
But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).
And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)
While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.
I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).
That's a good point, although couldn't you usually black-box those and assume the invariants we expect of those primitives are in fact true? E.g. you don't need to bother trying to prove properties about your prng itself, you can just prove how your program behaves under a random oracle model.
If you're able to detect where you use these hard-to-analyse functions, then yes. This is feasible on source level, and maybe known compiler binary level. I think ultimately people will want to validate properties of binary code against the model specification of their hardware.
Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).
How would certificate transparency logs have helped here though? If the private key leaks and anyone can mint a valid certificate that gets accepted, those logs aren't going to reveal it.
If an attacker takes the CA key and issues a valid certificate, but does not log it to CT, mainstream browser clients will not accept it.
When a certificate is logged to CT, you get back an SCT, and the issuing CA will normally include that in the certificate. The browser will then accept this certificate as it has the correct SCTs (there are always at least two).
The attacker issued certificate hasn't been logged, so can't have an SCT, so won't be accepted by the browser.
We can't say that no certificates have been issued by an attacker. We can say that no certificates have been issued by an attacker that a modern browser client would accept.
The way he describes the model of neural nets almost reminds me of a decision tree, with the positive/negative poles and stuff. There's another quote from the article about the "textbook" intuition of convnets
>neurons generalize, work together, and build abstractions over layers. Somewhere along the way we overcomplicated that picture, but looking harder brought it back.
and it does seem that if what the article claims is true, then it really is that simple. To clssify e.g. fruit they first detect curves/shape, then the neurons downstream of say the "circle" detector may distinguish based on color, then the ones downstream of a specific color distinguish by texture, and so on. By the end, what you have are neurons that activate only on very specific combination of features, which map to each fruit.
It's about as difficult as describing vectors in math. Vectors aren't really "little arrows" or "things with magnitude and direction" (because then functions wouldn't count), I think there's a similarly cryptic saying that "a vector is just an element of a vector space" or "a tensor is anything that transforms like a tensor".
In both cases what they really are is an abstract concept defined by things that satisfy some definitions, but in practice it's easier to just look at a few concrete examples like Maybe.
Oh I know. Actually it's even worse than not having "infinite money reserves"; the tables almost always have max bets meaning you can get to a situation where a single win will not recover your gambling, even if you had a money printer right next to you.
I almost never gamble, the last time being ~2012. I figured it might be fun to set aside like $100 and try the strategy regardless, content with walking away if I won the minimum bet. I actually won on my first bet and cashed out immediately.
You can run LLMs inside the shaping engine, so maybe you can use more advanced segmenting and transliteration algorithms? https://fuglede.github.io/llama.ttf/
It can depend on implied information, e.g. 方 can be hou or kata depending on if you're talking about about direction or a person. And that information can be before it, after it, on some image next to it, etc.
There aren't good datasets for that. Even neural TTS for Japanese struggles with it since Japanese transcriptions used to train models don't preserve pronunciations used.
(or maybe it could be theoretically done, just the mechanism to automatically classify wildly different pronunciations mapped to the same literal expressions don't yet exist)
That's surprising. I'd have thought that a multimodal LLM like openai's would "just work", at the very least enough to generate enough data to distill down to a simpler model.
Even professional native voice actors get a reading wrong in audiobooks sometimes so it's not surprising to me that LLMs are not quite reliable enough either at this point
Yeah. Either there's just not enough annotated text in existence, or frontier LLMs aren't trained with enough such text.
I think the latter is a possibility too; the Japanese language share little from syntax to vocabulary to memes with other languages, including Chinese(Japanese is NOT a dialect of Chinese; arguably it was SUPPOSED TO in the ancient times, but Japan was simply unable to achieve that status), despite sharing Unicode codepoint ranges with the Chinese language due to Han Unification. So there might be some chance that Japanese part of the dataset is inconsistent and contradictory to other parts, in some ways such that, it would make sense to include just the bare minimum to achieve best use of resources available at this point. Chinese models seem to do this, and dataset fractions of Japanese content is always tiny. Some of Chinese image models even straight up un-support Japanese.
As to what teshigahara said in the sibling comment - I think that shows the readings are arbitrary rather than being simply complicated and hard to infer for beginners. It must be that the Japanese written-spoken convergence movement began in the early modern times never reached its goals, beyond the written language having its own tone like in many languages, and so the verbal Japanese expressed in Japanese writings is simply not complete.
Hm that's clever. You're basically taking the classic "queue using two stacks" algorithm but then replacing each stack with a min-stack (like in that leetcode problem where each element also tracks the aggregate of all elements below it) to get a "min queue".
And then unlike the usual monotone queue for sliding max/min, this works for any monoid since you're never comparing two elements.
Yeah, I mean, a lot of things can express attention, because attention is mechanically extremely simple. The "trick" of attention is that it's "relatively easy" to train. Or if not "relatively easy", we at least have a lot of collective experience doing it.
No LLM can help companies that didn't care about software quality in the first place. If they did, they wouldn't have fired QA testers. And now that they've been gone for a decade while revenues have soared, why would they bother using LLMs for QA testing when they could execute on the stakeholder's vision instead!
You'd expect to see the majority of benefit to independent devs who previously _couldn't afford_ QA or a full team, and now can. But since the target audience for this stuff is niche, you're less likely to hear about it unless you're plugged into the subcommunities (see e.g. how LLMs have helped with game preservation, retrogaming).
reply