HNHacker News
TopNewBestAskShowJobs

thomasahle

6,922 karma · joined February 23, 2013

https://thomasahle.com
submissionscomments
thomasahle··on Dots
Do Dots replace OpenClaw?
thomasahle··on Book review: Is parallel programming hard, and, if so, what can you do about it?
Parallel programming is a great application for LLM correctness proofs in Lean.

You can't unit test your way out, but if you care about the code's correctness, today there's a way.

thomasahle··on Adversarial examples for fast hash functions
Yes, a good example is tabulation hashes which is

    h(x1, x2, ...) = T[1, x1] ^ T[2, x2] ^ ... 
but most fast hashes are actually algebraic, typically using polynomials in some way. I'm not sure they fit into the same pattern?
thomasahle··on Adversarial examples for fast hash functions
Non-cryptographic hashing should not mean "no guarantees". Unfortunately it's very hard to empirically test if a pseudorandom function works well on all inputs.

We analyzed 30 popular hashes and found Key-independent collisions in nearly all of them. E.g. xxh3 has pairs that collide with probability 2^{-10}, much higher than the 2^{-64} you'd expect.

However some fast hashes are good on all inputs, and we were able to verify it in Lean.

thomasahle··on Android 17 is the first since 3.x to add new APIs without releasing to the AOSP
Also Bada
thomasahle··on Bend 2 and the Vibe-Coding Trap
> Where this differs from Bend is that what we have supplied here is everything required to prove the correctness of the program, without having a LLM waste time and tokens on building up a 442 line proof from first principles. We can run GNATprove and get: `Success: all checks proved (12 checks).`

GNATprove uses SMT solvers, meaning it's basically a brute force proof system.

Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don't have to supply a proof. It's all automatic.

But brute-force proofs don't scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write _actual_ proofs.

thomasahle··on Show HN: Compute polynomials twice as fast
Sorry I meant

    P_i = x_{2i} + (x_{2i+1} + z^3)(P_{i-1} + z^2)
thomasahle··on Show HN: Compute polynomials twice as fast
I'm happy to take a PR if you have a good layout in mind!
thomasahle··on Show HN: Compute polynomials twice as fast
> Hopefully that answers your question about why someone might still choose to use heuristic hashing

Not really. Our method is also 2x faster than xxh3.

Sure, AES make the heuristic hashes harder to break, but they still provide (1) slower performance, (2) no guarantees.

thomasahle··on Show HN: Compute polynomials twice as fast
It's true that you can use AES instructions now on some computers, bit I honestly don't see why you'd use a heuristic hash (even if cryptographic) when you can get provable guarantees with k-wise independent hashing. Our paper makes these even faster than they already were.

See section 5.7 and 5.8 in the paper for experiments against other hashes.

thomasahle··on Show HN: Compute polynomials twice as fast
I'm not sure, since we only do univariate polynomials and k-path has lots of variables, right?

But maybe this work can inspire looking for other small, constant factor saving circuits for different classes of polynomials. Would be cool!

thomasahle··on Show HN: Compute polynomials twice as fast
> the "universality" property of such hashes seldom provides any substantial benefit over alternative hash functions that do not have this property

Do you mean hashes like xxh3? We have a section in the paper showing for a bunch of these that they collide much more often than universal hashes on bad inputs.

thomasahle··on Show HN: Compute polynomials twice as fast
It's the blessing and the course of a polynomial inverse: the inverse is the same degree as the polynomial, so its largest coeffecient is large and blows up. Knuth-Eve and Pan use the root of a degree d polynomial, which is slightly less big, but still inpractical.
thomasahle··on Show HN: Compute polynomials twice as fast
> This method requires additional preprocessing of the coefficients, before starting to evaluate the polynomial. That preprocessing would slow the hashing algorithm more than what is gained during evaluation.

There is no preprocessing at hash time in either use.

Universal hashing: the message words are the parameters of the chain, a_i and b_i in P_i = a_i + (b_i + y)(P_{i−1} + u), not coefficients of a target polynomial. Distinct messages give distinct polynomials, which is all a universal hash needs; the decoder never runs. Same as Bernstein's BRW.

k-independent hashing: the key should be a uniformly random monic polynomial of degree k. Our parameterisation is a bijection onto those polynomials, with the rational preprocessing as its inverse, so uniformly random gate constants give a uniformly random polynomial. You draw the ⌊k/2⌋+1 constants and evaluate; the coefficients are never computed. That is why the paper needs bijective rather than just injective constructions, and the Section 5 speedups are for the whole hash.

Preprocessing only appears when a fixed polynomial (a Taylor approximation, a secret-sharing polynomial) is evaluated at many points, and then it runs once.

thomasahle··on Show HN: Compute polynomials twice as fast
See also discussions here https://www.reddit.com/r/programming/comments/1wbgcke/commen... on how the actual math works out.
thomasahle··on Show HN: Compute polynomials twice as fast
Thank you! It was a lot of fun to make the website and see all the methods in practice after having just looked at the theory for a long time :D

> have a separate source node for each x, x^2, x^4 used

Do you mean a graph like this R&W? https://thomasahle.com/fast-polynomials/#ex=bessel&mode=Q&me... there are nodes labeled x2, x4, x8; but it's the output of multiplications, and we want to make the number of mults visually clear.

thomasahle··on Show HN: Compute polynomials twice as fast
FFT multipoint evaluation is great when you know all the evaluation points in advance. However, for many practical applications the input is only streamed to you. E.g. a polynomial hash for a hashmap. Or preprocessing the taylor approximation of exp(x) for a standard library.
thomasahle··on Show HN: Compute polynomials twice as fast
In CRC8 you interpret the input as coefficients of a polynomial, and take mod `x⁸ + x² + x + 1`. The problem we solve here is a bit different: You know the coefficients in advance, and want to preprocess the polynomial to make it fast to evaluate.

However, in section "5.9 Injective Polynomial Hashing" we actually study the problem of universal hashing, which is a lot more like CRC8.

thomasahle··on Show HN: Compute polynomials twice as fast
If you are working over floating point, you probably with to use Estrin's method (see https://en.wikipedia.org/wiki/Estrin%27s_scheme - also tab 3 on the website.)

It takes advantage of FMA (fused multiply add), has good numeric stability and uses pipelining optimally.

A while ago I suggested using Estrin's method in Boost, for functions like std::exp. There's some interesting discussions here: https://github.com/boostorg/math/issues/924 if you are interested in all the practical details.

However, for finite fields (e.g. used for hashing and cryptography) multiplication is much more expensive than addition, which is the main use of this algorithm.

thomasahle··on Show HN: Compute polynomials twice as fast
I don't know what happened to the URL, but it's supposed to link to this paper: https://www.gwizfl.org/email/cr.yp.to/antiforgery/pema-20071...

It's a very nice construction (based on Rabin & Winograd's polynomial multiplication method) for building universal hashes with n/2+O(logn) multiplications.

The annoying part is that it's a tree structure, which is not usually what you want in a fast hash that you're folding over a data stream. Some papers like https://eprint.iacr.org/2017/328.pdf try to fix this, but there are a lot of annoying trade-offs.

A famous fast hash is NH, which is just:

   H(x) = sum_i (x_{2i} + a_{2i}) * (x_{2i+1} + a_{2i+1})
where `a_i` are random keys. No modulus needed. The issue is that you need as many random keys as the length of the input.

Our construction (section 5.9 Injective Polynomial Hashing) shows that you can do something a bit similar with polynomials:

    P_0 = z
    P_i = x_{2i} + (x_{2i+1} + z^3)(x_{2i} + z^2)
this is a lot simpler than Bernstein's, and is still n/2 multiplications.
thomasahle··on Show HN: Compute polynomials twice as fast
WyHash and xxh3 are not polynomial, in fact this is one of the issues we try to solve in the paper.

Many "practical" hashes use heuristics instead of real field multiplications to be faster. But it means they are vulnerable to adversarial inputs. That means, it's possible to design a set of keys that have much higher probability (under random hash seeds/keys) to collide than you'd expect under a correct hash function.

We actually analyze both WyHash and xxh3 in this setting in section "Adversarial inputs for heuristic hashes" - https://arxiv.org/pdf/2609.06022#page=165

thomasahle··on Apple Watch Ultra 4
It's surprising that in 2026 they still haven't figured out how to remove the bezels. They are smaller than they used to be, but On something as compact a watch, all screen estate counts.
thomasahle··on What do Visa and Mastercard do? An intro to card networks
They charge you 23%?

I thought in the EU the maximum interchange fee for consumer credit cards is capped at 0.3% of the transaction value.

thomasahle··on Research acceleration: The view inside OpenAI
1) That's maybe $180,000 per year, so much less than median OpenAI employee wages.

2) OpenAI doesn't pay API prices.

3) Compute costs are likely already their biggest expense, dwarfing wages.

thomasahle··on The Real Luxuries In Life
Do you want people here to try to convince you to have kids?
thomasahle··on Finite time blowup for an averaged three-dimensional Navier-Stokes equation (2014)
Yes please. For a moment I thought Terrence Tao had scooped Anthropic.
thomasahle··on GPT-6 Astra
• 98.6% on ARC-AGI-3

• 97.6% on frontier math

• 95.9% on CAD

• 100% on ExploitBench

Nothing modest about it

thomasahle··on AI boosted homework scores, then exam scores dropped: study
> Grades should come from hard randomized exams with unlimited retakes

Exams will have to be a lot longer if you allow unlimited retakes. Generally exams work on a sample principle, but this breaks with retakes.

thomasahle··on AI boosted homework scores, then exam scores dropped: study
> had similar (slightly higher) performance.

The data point around 80 minutes seems like noise to me. Looks like there isn't enough data/students who spend that much time and also used AI.

It would be nice if AI was a force for good as well as bad, but the data here doesn't support it

thomasahle··on Docker Sandboxes – Disposable, isolated sandboxes for AI agents
Has anyone started proving their sandboxes in Lean (or Coq, etc.)?
Page 1 of 34Next →