from the GH page:
> Developed and tested on AMD Family 16h CPUs, the last generation whose datasheets document the DRAM controller's translation registers — and show that they can't be locked. 17h and beyond simply leave this information out.
I spent some time exploring this topic.
Here's my thesis:
Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes.
The cost of finding and developing exploits also was high.
That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost.
We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point)
So the cost of finding and developing exploits has dropped dramatically.
On the other hand, formal verification is now much easier, since LLMs can automate the proof.
You don't even need to worry about hallucinations, you merely need to trust Lean core.
If the LLM is wrong, the proof will get rejected!
The problem of exploits gets bigger, and the solution of formal verification gets cheaper.
As a result, the needle is now moving in the direction of "more formal verification".
I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time.
My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly.
I have not achieved that goal yet.
What I have so far:
- one (non-optimized) compiler step which is formally verified
- three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR
You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords.
Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else.
I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.
I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually:
* Understandable
* Portable across projects, you could imagine something like
from specs import no_stealing_secrets
no_stealing_secrets(secret_table)
* Implicitly proves the absence of RCE, though I suppose
it could allow something truly crazy like an interpreter
that will run any attacker supplied program that can
be proven not to steal the specified secrets
Don't we still need to verify that what the LLM proved is actually the stated system?If agents cutting corners (like deleting tests) is a concern, how can we be sure that the verification corresponds to the software and that every _load bearing_ assumption is true? I don't think that simply trusting the Lean core is enough.
Of course, and correct verification assumptions were always a challenge, and they are a possible failure point - but 95%(?) of labour was then proving the code, and now that part can be largely automated.
Speaking of how difficult can it be to write a proper spec, I think a few years ago someone found a bug in spec in a helloworld-like example in a book about formal methods, and a bug in the code.
Yes, this is a challenge, but I don't think it's as damning as it sounds.
First, the same kind of issue exists with any kind of testing. We all know that having unit tests and integration tests doesn't mean the software is correct and bug-free. Yet we still often believe it's worth investing in writing and maintaining a test suite. Formal methods is an additional level of assurance that I suspect we'd generally find worth it for critical software if it were easy enough to implement, even if it's not perfect.
Second, because formal verification has been so hard, nobody has really bothered making a serious attempt at solving the spec problem before (at least not to my knowledge). We've spent decades building frameworks that make writing tests really easy. We really have not come close to investing the same kind of effort into building frameworks and tools to make writing formal specs easy. I can imagine a world where we have sophisticated tools that help us create specs, plus real-time verification infrastructure that automatically reverifies code against the spec on each PR.
Third, and perhaps most importantly, there are many industries where this is actually low-hanging fruit: aerospace, medical devices, etc., actually already have formal specs that are verified manually by human engineers to satisfy certification requirements. I believe that's a more natural starting point vs. trying to scale formal methods for all software in general.
While that is true, just having LLMs "think about it" may discover unintended behavior and exploits, and you can choose to what extent you want to verify that the claims are correct.
Just as an addendum to some of the other fine replies you've got, one of the things I'm interested in for formal verification is security assertions, and those don't necessarily need lots of comprehension to apply. If you can assert "this code never hits the network again" or "this code will never execute arbitrary code", the proof of that may be nontrivial but the comprehension of it is easy.
Proving that some complicated algorithm is actually what you think it is, even after you've proved that it does whatever it is it does, is hard. But to me, and me personally so not necessarily what everyone else thinks, that's not really what I'm interested in from proofs. I'm really more interested in these overarching declarations of what the code definitely doesn't do, or putting bounds on what it does, rather than proving that my billing code bills the customers precisely in the way I expect, when, frankly, the best specification of it I have is already what is in the unproved code base anyhow. I believe those have a very sensible story as to how both humans and AIs can use those assertions.
The LLM does not prove anything (it cannot reason). It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system.
You still need to verify that the generated code is what you asked for, though.
> I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time.
I don't know. It seems to match the general futility of pedantry that exists in all professions. Yes, you can try to optimize for absolute 0 flaws in your code, but in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point.
> software is 1/10, reducing that to 1/100 makes a bog difference
I fully agree! I'm all for moving the needle towards moving the needle towards more formal verification, but what GP is suggesting is full verification of programs, which is more akin to trying to achieve a 1/10^6 bug rate.
I had claude spend about 2 hours friday modeling one of our kubernetes operators in TLA, and it found 8 bugs, including 2 that could cause data loss, and one of the other bugs was one we had been trying to figure out why it was happening for literally months.
Thank you, I've heard of it. It is indeed very close to what I want to have.
CakeML project also has a language Pancake, which has interesting properties.
> We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point)
But... if that's not the point, the claim is obviously untrue. The security industry includes public-facing bug bounty platforms. Those find far more vulnerabilities than Mythos ever will, if you're not even worried about what counts as a vulnerability.
There were many prototyoes of certifying compilers and proof-carrying code in academia. The FLINT group by themselves had many. Maybe try building on those.
I'm so amazed to find out just how close we are to the start trek voice computer.
I used to use Dragon Dictation to draft my first novel, had to learn a 'language' to tell the rudimentary engine how to recognize my speech.
And then I discovered [1] and have been using it for some basic speech recognition, amazed at what a local model can do.
But it can't transcribe any text until I finish recording a file, and then it starts work, so very slow batches in terms of feedback latency cycles.
And now you've posted this cool solution which streams audio chunks to a model in infinite small pieces, amazing, just amazing.
Now if only I can figure out how to contribute to Handy or similar to do that Speech To Text in a streaming mode, STT locally will be a solved problem for me.
Happy to answer questions about this (or work with people on further optimizing the open source inference code here). NVIDIA has more inference tooling coming, but it's also fun to hack on the PyTorch/etc stuff they've released so far.
Thank you for sharing! Does your implementation allow running the Nemotron model on Vulkan? Like whisper.cpp? I'm curious to try other models, but I don't have Nvidia, so my choices are limited.
It's an artifact of the camera. The camera shutter is long enough that it averages the images over 33ms.
At some point in the video you can see that a high speed camera can see the correct display.
At the 7 minute mark the industrial 14k FPS camera shows essentially zero rollover. The earlier rollover does appear to be an artifact of the cheap consumer grade high speed camera used.
when it comes to real people, they get sued into oblivion for downloading copyrighted content, even for the purpose of learning.
but when facebook & openai do it, at a much larger scale, suddenly the laws must be changed.
Swartz wasn’t “downloading copyrighted content…for the purpose of learning,” he was downloading with the intent to distribute. That doesn’t justify how he was treated. But it’s not analogous to the limited argument for LLMs that don’t regurgitate the copyrighted content.
This is not about memory or training. The LLM training process is not being run on books streamed directly off the internet or from real-time footage of a book.
What these companies are doing is:
1. Obtain a free copy of a work in some way.
2. Store this copy in a format that's amenable to training.
3. Train their models on the stored copy, months or years after step 1 happened.
The illegal part happens in steps 1 and/or 2. Step 3 is perhaps debatable - maybe it's fair to argue that the model is learning in the same sense as a human reading a book, so the model is perhaps not illegally created.
But the training set that the company is storing is full of illegally obtained or at least illegally copied works.
What they're doing before the training step is exactly like building a library by going with a portable copier into bookshops and creating copies of every book in that bookshop.
But making copies for yourself, without distributing them, is different than making copies for others. Google is downloading copyrighted content from everywhere online, but they don't redistribute their scraped content.
Even web browsing implies making copies of copyrighted pages, we can't tell the copyright status of a page without loading it, at which point a copy has been made in memory.
Making copies of an original you don't own/didn't obtain legally is not fair use. Also, this type of personal copying doesn't apply to corporations making copies to be distributed among their employees (it might apply to a company making a copy for archival, though).
> when it comes to real people, they get sued into oblivion for downloading copyrighted content, even for the purpose of learning.
Really? Or do they get sued for sharing as in republishing without transformation? Arguably a URL providing copyrighted content, is you offering a xerox machine.
It seems most "sued into oblivion" are the reshare problem, not the get one for myself problem.
From my observations: cold start, ease of patching.
If you're running a lot of different JS code or restarting the code frequently, it's faster than node.
Where it's useful: fuzzing. If you have a library/codebase you want to fuzz, you need to restart the code from a snapshot, and other engines seem to do it slower.
It's also really easy to patch the code, because of the codebase size. If you need to trace/observe some behavior, just do it.
Salesforce sandboxing is too easy to escape. Last time I needed to implement some feature for Salesforce, I've encountered 4 different escapes. It was also horrible dev experience.
It's not about being poor.
First, the climate didn't require AC in most of the Europe, until ~10 years ago. You had a few hot days, and that's it.
Second, thermal isolation in the US is extremely bad quality. I think people could cut their AC usage by half if they had proper thermal isolation in their houses.
Third, northern Europe countries still don't have a climate to justify buying an AC.
Specifically, American houses lack thermal mass due to being constructed mainly from wood. Concrete and brick will buffer over a week or so of heat before it warms up too much.
In Florida, most of the homes are built from concrete brick with wood trusses. There are apartments made from wood and concrete.
It’s not the heat completely - it is also the humidity. You can bear up to 80 F before it starts to feel uncomfortable. Humidity will make even 75F uncomfortable.
Relative humidity isn't a great indicator of comfort. It's better to look at dew point. The Netherlands is not only cooler on average but also has a lower dew point. This shouldn't be surprising given each country's latitudes.
Both regions have high humidity, but Florida tends to have higher average humidity levels, particularly in the summer months. Florida has a subtropical to tropical climate, characterized by high temperatures and humidity, especially in the summer. Florida experiences high humidity levels throughout the year, often ranging from 70% to 90%. Summer months are particularly humid, with frequent afternoon thunderstorms.
The Netherlands has a temperate maritime climate, influenced by the North Sea.
Florida and the Netherlands are not close in comparison.
I’m sorry, but it is just mind boggling to suggest that Netherlands and Florida have comparable weather in any sense. You wouldn’t suggest that the weather in Netherlands is as hot as in, say, Italy or Greece, and Florida is even hotter than these two.
I'm not saying it's as hot here as it is in Florida. But we've been breaking records left and right up to the point where I've purchased an AC (a crappy mobile one for lack of better options here for rented apartments) because we go through months every summer now where I can barely sleep without one anymore.
My point was that people often don't realize how humid it is here. You apparently also can't believe it. And how our buildings are not made to keep heat out, but rather in. So I expect many more ACs to be sold here as well in the coming years.
It might just be a month or two each year. And it might be worse for you. But it's also getting pretty bad here already thanks to climate change. And that's not going to improve anytime soon thanks to all of us.
Yes, mostly by using insulating (double) glass to let warmth in in the form of light that then warms up the interior. Think greenhouses. Surround that with poorly insulated walls and limited ventilation and in cold weather they'll leak out heat while in warm weather they'll also heat up in the sun and radiate that in.
Any home with an ACH nat of 1 that's attempting to condition the air (heating or cooling) is wasting a mind boggling percentage of the energy. Surely that's not the natural ventilation rate of the _typical_ home? That would imply that 50% of homes are worse.
