ekez

I implemented an algorithm for neural network verification called ⍺β-CROWN for a deep-learning library called tinygrad.

https://github.com/0xekez/tinyLIRPA

tinygrad’s small set of operations and laziness made it easy to implement. Tho my overall sense is that neural network verification is currently more of a research interest than something practical.

I wonder if the authors have tried incorporating error feedback from Lean into their models.

Work from 2023 [1] showed general purpose models did better when they were able to incorporate error feedback, humans incorporate error feedback, but none of the SOTA models on minif2f seem to.

[1]: https://arxiv.org/abs/2310.04353

There’s something compelling about these, especially w.r.t. their ability to generalize. But what is the vision here? What might these be able to do in the future? Or even philosophically speaking, what do these teach us about the world? We know a 1D cellular automata is Turing equivalent, so, at least from one perspective, NCA/these aren’t terribly suprising.

If "we" all got together and reduced permitting costs, "our" homes would be much more valuable because a developer can build a highrise where the house is.

Thank you for the response. (I assume you mean "p' < -eps" in the second conditional?)

How often are rational approximations computable within any given tolerance?

why is it impossible to decide whether x<0, x=0, or x>0 as in Example 1?

The metric the authors use confuses me.

Edit distance seems like a strange way to test if the model understands arithmetic ([1], Figure 3). I think `1+3=3` would be equally as correct as `1+1=9`?

Why not consider how far off the model is `abs(actual-expected)`? I wonder if there is an inflection point with that metric.

https://arxiv.org/abs/2206.07682

> ChatGPT specifically seems to absolutely adore the phrase [complex and multifaceted], using it at every opportunity to explain higher level concepts.

I'm curious why this is. Before the echo chamber, did the LLM lean some ontology of speech?

The title is an allusion to the experiment which samples the output of the 12th layer of LLaMA-7b. Surprisingly, there is a fair bit of structure on the principle components of those samples.

Generally agree - the goal here was mostly to illustrate how simple a TCP proxy actually could be.

I shiver to think of how many lines of code actually get run with the tokio macro and green threads.

What are the advantages of tagged memory as opposed to using the unused bits in a regular pointer as a tag?

Hi HN. I wrote this up after feeling frustrated about a lack of information online about compiling closures. My hope is that is is useful to other people who get stuck at that point in writing their compiler.

The Lisp[1] I'm writing that I based this on is actually built on Cranelift[2] which has been a fun experience to work with. I'd love whatever feedback and questions people have.

[1] https://github.com/ZekeMedley/lustc/ [2] https://github.com/bytecodealliance/wasmtime/tree/main/crane...

`prefers-contrast` is important for moving web accessibility forward. Right now, making a website respond to someone's contrast preferences is next to impossible.

Its neat to see Firefox implement it and hopefully this spurs other browsers to follow suit.

The author makes a distinction between the "commercial web" and "small web" but I can't help but wonder if some overlap is possible.

I've recently been tasked with building a website for a small organic food distributor in Oregon. I don't think the traditional image heavy "commercial web" fits well with their company culture and image but am struggling to find examples of "small web" commercial websites to show them as examples of a different way.

It would be nice to see another post discussing how we might bring the small web to the commercial one.

Zeek uses CAF internally for data exchange over networks and workers [1]. It's not quite a "native actor concept", but it is a nice way to interact with the framework. I've used it before and its worked quite smoothly.

[1] https://docs.zeek.org/en/current/frameworks/broker.html

As someone who's been working through the book for the last few months, thanks so much for sticking with it. Your prose is excellent and full of really properly funny stuff sometimes. Reading your book has been my weekly dose of programming I know I'll enjoy.