And despite that, although they are not like that in practice as there are too many uncontrolled variables, with temperature at zero, for the same input they produce always the same reply.
BS. Run them sequentially on a single core, and without fancy speedups enabled, and they do. The algorithm is determinstic. Any non-determinism present with 0 temperature it's not some mysterious LLM-inherent property, but something that can be seen in any large program taking advantage of multi-core, floating point, and other CPU-based parallelism optimization.
People often assume they are not because they can ask the same query to the same model and get differences in output, but wrongly conclude that this is some inherent LLM trait, instead of non-determinism added on top of it because of implementational choices that were made.
We know what is going inside black holes in other galaxies, we know the details of Israel nuclear program..., the Windows source code got leaked, we got the NSA tools and full details and locations of the Echelon architecture... Phds in Maths warns us daily about the terrible secrets of the evil AI inside their labs. How, their numeric matrices and gradient descent Python scripts, are about to kill 10% of us all, I guess the sick or genetically less interesting ones...and use the rest, as some meat/metal hive drones part of some Borg collective...
There are ONLY TWO Stories and their details, that we collectively will never see.
1) One could come from the these brave souls that warns about an impending death...but their courage falters on another subject.... From Jacob Coxon to Evan Hubinger or Julie Steele, Samuel Marks, Josh Angels, Mrinank Sharma, Dario Amodei, Demis Hassabis, Geoffrey Hinton, Yoshua Bengio, Stuart Russell....The story of the full datasets they used to train the models, the data they stole, how many PB was, the amounts of data, the nights setting up torrents from unsuspicions IPs, where is it currently stored and how many exabytes is now... the massive data cleansing and data quality program to conform all the different formats, the internal discussions on the ethics of the stolen files, how large was the team, the CSAM content they sucked with their automated scripts and who was handling it internally, the porn, the massive amount of porn that is after all 80% of the internet, the leaks their data sucked with their automated scripts...
It will prove the bugs were corrected implemented... :-) And that your mistaken specification of the tax rules in Switzerland, was correctly translated to code, and that your mistaken specification of the process to request a mortgage is mathematically valid...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic...
I wouldn't say it's all rubbish - it's very easy for someone new to theorem proving to presume the equivalent of "strong typing will eliminate the possibility of errors", but the more correct understanding is "strong typing will reduce the number of things you have to keep in your head at any one time thus reducing the possibility of errors".
The thing with ubuntu's rust coreutils is that they, for example, crash when told to recurse because they use actual recursive calls to go into subdirs and run out of stack space if the structure is big enough.
any of the quite many cost-aware logical frameworks. it’s SO. easy. to. do. you fools are just willfully ignorant on how to represent reasoning, despite alleging yourselves to be computer scientists?
I presume you also can't stand people who write software tests for similar reasons? The test is wrong, the code is wrong. The spec is wrong, the code is wrong. What a waste of effort! Just write correct code people! Verification is left as an exercise for the end users. Who cares about them anyways? /s
Tests are guaranteeing that the product doesn't fail under the test conditions. Formal verification is guaranteeing the product doesn't deviate from the formal spec under a given set of assumptions. Both of them are useful but depend on how well the thing being checked actually correlates with what you care about.
Interesting definition of guarantee....what about the people who run millions of them? Well Microsoft: "AS IS." Apple: "WITH ALL FAULTS" Adobe: "no guarantee of error-free operation."
Apparently their lawyers never got the memo that the tests already guaranteed the software...
Well yeah, why would they offer an legal guarantee if they don't have to? They could have a watertight proof that their software works perfectly in all situations (lol) but the lawyers still would prefer to disclaim as much liability as possible.
And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.
That's exactly what testers are selling though. If they aren't guaranteeing the program is correct (up to what is tested) then what purpose do they serve? Same with formal methods, offering guarantees up to what is proven.
> You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-))
>> a man who was a major proponent of formal methods.
No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test.
He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."
An extraordinary statement itself that shows the difference between a proper cloud where they AZs are at least 60 to 100 miles apart...and Google or Microsoft... pretend clouds...where those AZs are just firewalls across the same data center...
reply