m1el
m1el on Hacker News
> rather than having to translate the whole program into Rocq
Translating your program to Rocq is vastly easier than to write a proof for a binary.
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.
LowIRSSA is
very different from the SSA in the repo.
LowIRSSA looks way more like SSA-WASM than assembly
Thank you for the suggestion, I will be sure to learn from those!
I understand that formal verification is not panacea.
My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code".
We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.
Self-insert time.
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
https://github.com/m1el/riscv-fv-bootstrap
The project is in quite a bad shape, and I am trying to improve my skills in that direction.
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.
somehow, I suspect openai didn't "buy" all of the articles, books, websites they crawled and torrented.
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.
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.
Artificial neural networks work the following way: you have a bunch of “neurons” which have inputs and an output. Neuron’s inputs have weights associated with them, the larger the weight, the more influence the input has on the neuron. These weights need to be represented in our computers somehow, usually people use IEEE754 floating point numbers. But these numbers take a lot of space (32 or 16 bits).
So one approach people have invented is to use more compact representation of these weights (10, 8, down to 2 bits). This process is called quantisation. Having a smaller representation makes running the model faster because models are currently limited by memory bandwidth (how long it takes to read weights from memory), going from 32 bits to 2 bits potentially leads to 16x speed up. The surprising part is that the models still produce decent results, even when a lot of information from the weights was “thrown away”.
Not a browser, but a PWA. It's a web page, which you can "install" as an "app". Features like storage, background tasks and notifications are important for many applications, for example a messenger. These were available, and there is a market for those, but Apple has decided to kill that market.
I too select the lines that I read. However, I never select the entire page, unless I intend to copy it.
Oh, and to add an insult to the injury, I was using a collaborative editing tool.
So I was able to see the person:
1) Select All (most likely followed by the copy)
2) Type the answer
3) Make an obvious mistake when they type else block, before the if
I've had a displeasure of interviewing someone who used ChatGPT in a live setting.
It was pretty obvious: I ask a short question, and I say that I expect a short answer on which I will expand further. The interviewee sits there in awkward silence for a few seconds, and starts answering in a monotone voice, with sentence structure only seen on Wikipedia. This repeats for each consecutive question.
Of course this will change in the future, with more interactive models, but people who use ChatGPT on the interviews make a disservice to themselves and to the interviewer.
Maybe in the future everybody is going to use LLMs to externalize their thinking. But then why do I interview you? Why would I recommend you as a candidate for a position?
The minimap contains a copy of the content, but with `transform: scale`.
The rest is handling `window.onscroll` and mouse events on the overlay.
I am not scared for AI overflowing the news sites with bullshit. We already have a fire hydrant worth of bullshit content produced for consumption. Lies and fakes have coexisted with humans forever. People did rumours, then we had books, press, radio, television, and now the Internet.
"But it's easier to produce lies/deepfakes today" -- true. However, the absolute cost of producing a lie per consumer already was negligible, and now it's even smaller.
People will recalibrate their level of trust in technology and move on.
You're correct to have a suspicion here. Hypothetically the explainer could omit a neuron or give a wrong explanation for the role of a neuron.
Imagine you're trying to understand a neural network, and you spend enormous amount of time generating hypotheses and validating them.
Well the explainer might give you 90% correct hypotheses, it means you have 10 times less work to produce hypotheses.
So if you have a solid way of testing an explanation, even if the explainer is evil, it's still useful.
I don't understand how the author can write "No, they cannot.",
while the page says "GPT 4: 0 false alarms in 15 good examples. Detects 13 of 13 bugs."
Edit: the post says open-source models.
If you're doing inference on neural networks, each weight has to be read at least once per token. This means you're going to read at least the size of the entire model, per token, at least once during inference.
If your model is 60GB, and you're reading it from the hard drive, then your bare minimum time of inference per token will be limited by your hard drive read throughput. Macbooks have ~4GB/s sequential read speed. Which means your inference time per token will be strictly more than 15 seconds.
If your model is in RAM, then (according to Apple's advertising) your memory speed is 400GB/s, which is 100x your hard drive speed, and just the memory throughput will not be as much of a bottleneck here.
If this was true, how come humans advanced math and philosophy?
The information loss you're describing is going from Flame Charts to Flame Graphs.
Yes, the call ordering, and multiple calls are lost if you're generating a Flame Graph.
As a developer who doesn't use mathematical notation very often, I've had some difficulty reading it.
From my understanding, the paper goes as follows:
2.1 Define FlameGraph
Frame = something that identifies function/location in the code
Stack = Vec<Frame>
FlameGraph = Map<Stack, Real>
FlameGraphPositive = Map<Stack, RealPositive>
2.2 Define FlameChart
FlameChart = Vec<{ start: Real, flame_graph: FlameGraphPositive }>
# such that the start values are strictly ordered
fn to_flamegraph(flame_chart: FlameChart) -> FlameGraphPositive {
flame_chart
.map(|{ start, flame_graph }| flame_graph)
.sum()
}
Personally, I think a better definition of FlameChart is:
FlameChart = Vec<{ end_time: RealPositive, stack: Stack }>
# such that sampling starts at 0 and Vec is strictly ordered by end_time
fn to_flamegraph(flame_chart: FlameChart) -> FlameGraphPositive {
let mut start = 0.0;
flame_chart.map(|{ end_time, stack }| {
let elapsed = end_time - start;
start = end_time;
FlameGraphPositive::from_stack(stack, elapsed)
}).sum()
}
3.1 Define diff
# a,b: FlameGraphPositive
fn diff(a, b) -> FlameGraph;
# such that a + diff = b
# diff: FlameGraph
# add, sub: FlameGraphPositive
fn to_positive(diff) -> { add, sub };
# such that diff = add - sub
3.2 Define a naive diff metric
# a,b: FlameGraphPositive
fn diff_metric(a, b) -> RealPositive {
diff(a, b).size() / (a.size() + b.size())
}
# diff_metric(a, b) \in [0, 1]^Real
3.3 Define a more sophisticated diff metric
Using Hotelling T^2 Test, the author defines a metric, which takes sampling variance into account, and allows to detect performance regression, even when the sampling profile is noisy. (you'd have to read the paper for the exact method)
The code for this test is here:
https://github.com/P403n1x87/flamegraph-experiment/blob/04db...
https://github.com/P403n1x87/flamegraph-experiment/blob/04db...