I feel like most commenters are missing the point. The fact that this issue was finally settled once and for all using a proof assistant is a huge achievement! That's the highest degree of scrutiny that a proof can undergo. This is especially important given the high number of mistakes in prior work—one would be forgiven for distrusting new papers on this topic that don't have machine-certified proofs. I can't believe people think this is just clickbait. Do y'all not recognize the importance of math being...well...correct?
The article doesn't say that the original proof was incorrect. It argues that one of the original theorem's assumptions was not justified. A machine certified proof doesn't help with this. [EDIT: The author points out below that the assumption was not explicit in Bloom's work. An attempt at a machine certified proof would catch this aspect. But not the aspect of the assumption being wrong, if it were added explicitly.]
Now, others later recognized this faulty assumption and produced a new formula and a faulty proof for its correctness. A machine certified proof would help here if an actual proof step is wrong, except note the footnote: "To be fair, the error in Bose et al.'s paper was primarily due to incorrect definitions, rather than an incorrect logical step. As an interesting anecdote, the first version of our work was based off the incorrect definitions by Bose et al. and ended up being rejected by reviewers who then rediscovered this error." So again it was human checking that (re-)discovered an issue. One that appears to have been fixed by humans before this work. And one that the machine wasn't able to find.
So now that all known incorrect assumptions are shaken out (there might be unkown ones, Coq can't tell) this work is a machine checked proof of something that had been proved before. It's an achievement, and it's good to have certainty. Almost anything that gets us closer to more formal math and computer science is good. But this particular result is hardly spectacular.
As for the clickbait aspect, I'm also annoyed by it. The title is clearly factually incorrect. No property of Bloom filters has been debunked. A widely cited formula was replaced by an asymptotically equivalent one 12 years ago, and we now have a machine checked argument that this replacement was correct. This isn't a debunking of anything. No math has been disspelled.
Clear and honest science communication is important. Authors overselling their work in such (obvious) ways just highlights that they themselves don't think the work is sensational (which it doesn't have to be!), and it makes readers wonder in what other ways they are intellectually dishonest.
> The article doesn't say that the original proof was incorrect
Apologies if my wording did not make this clear: the original proof by Bloom is logically incorrect
Bloom derives his expression by performing a transformation that would only be possible if the bits are independent, but nowhere in his proof does he state that he is making this assumption. It just so happens that even if he had explicitly included this assumption, it would not have been justified. So in that sense, the debunking part is correct - we disprove Bloom's original bound by proving the true bound under the same assumptions that he explicitly makes.
> Bloom derives his expression by performing a transformation that would only be possible if the bits are independent, but nowhere in his proof does he state that he is making this assumption.
I see, thanks for this clarification. I read your post as saying that the assumption was explicit. I agree that reasoning from an implicit assumption is a logical error. Still, the real problem was not the assumption being implicit/explicit but rather that one doesn't want to rely on it at all. Which again is an extra-logical issue.
> So in that sense, the debunking part is correct - we disprove Bloom's original bound by proving the true bound under the same assumptions that he explicitly makes.
OK. I don't think that recapitulating something that has been known with more or less certainty for 12 years counts as "debunking". For me "debunking" has a connotation of being original, maybe for you it doesn't.
But I especially think that "the formula was only asymptotically correct" is too weak a statement to count as a "debunking". For me "debunking" an algorithm or a data structure would have to be something much bigger, like "Quicksort doesn't always sort" or "binary search trees can lose data" or "Bloom filters can sometimes have false negatives". Not "the behavior we have been seeing for the last 50 years matches the original formula well, but strictly speaking it matches the new formula a bit better". Your mileage obviously varies.
EDIT: Let me stress again that I'm not pooping on your work. The work appears sound and important, since this was so tricky to get right in the past. But I am pooping on the title.
Given the history of the proofs of the Bloomfilter, I'd argue that the bound was not really "known with more or less certainty" - if so many corrections had to be made, why should we believe that this latest paper was truly correct? it does not seem to be unreasonable to believe that there might be other errors that had been been similarly overlooked. Our research tackles this problem - it provides a guarantee that there are no further hidden errors.
> "the formula was only asymptotically correct"
I have no issues with the behaviors of a data structure being characterized in an asymptotic sense, but I do think that giving a bound that you claim to hold exactly, but then having it turn out to only hold asymptotically is incorrect and worthy of debunking. Furthermore, most citations of Bloom's bound do not claim it is an asymptotic bound, but use it as an exact one, which is clearly incorrect.
I think from an engineering perspective it doesn't feel like a debunking. Nothing we assume about the bloom filter has been fundamentally changed. I think that might be the perspective of most people in here.
At the end of the day, this is primarily a formal result with few direct implications on practical usage. As I mentioned in another post, I tried to make it more relatable to an engineering audience, but it's possible that I may have buried the lede somewhat. However, I still stand by the statement that the title is not incorrect, at least if only from a mathematical perspective.
Good point. The main Bloom filter I use at work is 8 million bits in size, and at that scale, it does seem completely negligible whether you account for bits being selected by multiple hash functions since the odds of that happening are so small. We could add a few bits to the 8 million to correct for the error, but that's not meaningfully changing anything; it's just a drop in the bucket.
> Our research tackles this problem - it provides a guarantee that there are no further hidden errors
Does it? At a glance you seem to have evaluated Bloom's false positive rate against Knuth's version of the filter. I say this because your starting point is Bose, whose result is for Knuth's version.
The popular "Bloom filter" is not, in fact, Bloom's filter. Their different constructions lead to different exact false positive rates, so I suspect you've failed to prove anything about Bloom's original paper.
Of course Bloom was wrong in any case. Grandi's "On the Analysis of Bloom Filters" (2017) is the paper to read there. It was the first to offer an exact account of the false positive rate for Bloom's construction.
> so I suspect you've failed to prove anything about Bloom's original paper
In Bloom's original paper "Space/Time Trade-offs in Hash Coding with Allowable Errors", Bloom proposes multiple variants of these filter structures, and it is true that these variants do have different behaviours.
However, the expression cited as Bloom's bound (equations 16/17 in the paper) are specifically about a data structure (he refers to it as method 2) that works exactly like the standard definition of a Bloom filter (Knuth's version). In this sense, our result holds for Bloom's bound.
For reference, Bloom's description of method 2 is as follows:
> Method 2 competely gets away from the conventional concept of organizing the hash area into cells. The hash area is considered as N individual addressable bits, with addresses 0 through N - 1. It is assumed that all bits in the hash area are first set to 0. Next, each message in the set to be stored is hash coded into a number of distinct bit addresses, say al, a2, ..., ad. Finally, all d bits addressed by al through ad are set to 1.
> To test a new message a sequence of d bit addresses, say al, a2, .. , ad, is generated in the same manner as for storing a message. If all d bits are 1, the new message is accepted. If any of these bits is zero, the message is rejected.
Clearly this method describes the conventional version of the Bloom filter.
This is an easy mistake to make. Note the word distinct:
> each message in the set to be stored is hash coded into a number of distinct bit addresses
In Knuth's filter, the addresses aren't distinct. Bloom's construction requires that they are, thus the probability of a bit being set to 0 from (16) in Bloom's paper is 1−(1−k/m)^n, different from the 1−(1−1/m)^(kn) in your paper.
Cuckoo hashing is commonly simplified in a similar way, indexing into a single table and allowing the hashes to overlap, unlike Pagh's original.
Anyway, from your paper:
> Bloom then claimed that the probability of a false positive was simply the probability of a single bit being set, raised to the power of k, reasoning that a false positive for an element y ∈ bf only occurs when all the k bits corresponding to the hash outputs are set.
> Unfortunately, as was later pointed out by Bose et al.[8], as the bits specified by f_1(x),...,f_k−1(x) may overlap, we cannot guarantee the independence that is required for any simple relation between the probabilities.
You're still right that Bloom is off, but it's not due to overlap in f_1(x),...,f_k−1(x), which his construction doesn't allow.
My broader point though was about your "guarantee that there are no further hidden errors", because a theorem prover is just a tool, tools are used by people, and people make mistakes.
> This is an easy mistake to make. Note the word distinct:
> each message in the set to be stored is hash coded into a number of distinct bit addresses
Good point, You are right that our correction does not address errors in Bloom's original definition, but rather in the definition of the Bloom filter that is typically used - I'll add a note to address this.
> My broader point though was about your "guarantee that there are no further hidden errors", because a theorem prover is just a tool, tools are used by people, and people make mistakes.
Yes, you are right, that's probably too strong a claim, my aim was to emphasize that there is more certainty in the proof, making it unlikely that there are no further hidden errors, but that was not clear.
> the real problem was not the assumption being implicit/explicit but rather that one doesn't want to rely on it at all. Which again is an extra-logical issue.
In a strict sense, yes, the problem with Bloom's proof was due to an implicit unjustified assumption. However, the reason that this assumption was implicitly introduced, was because Bloom accidentally overlooked certain dependencies between the bits - the "real problem" in this sense is the fact that when reasoning about random algorithms, it is hard to keep track of all the various dependencies involved and this can lead to incorrect proofs. This problem of tracking dependencies is a logical issue and one that is solved by proving the bound in a proof assistant.
That's neat! Is the deviation between Bloom's equation and the correct one relevant in pratice? Typical Bloom filters have millions or even billions of bits and a few to a few dozen hash functions, so I think the probability that an entry gets hashed to the same bit more than once should be vanishingly small?
Really cool otherwise, I should really look into Coq more for my own work.
For most practical applications, the sizes involved are such that you're probably dealing with the asymptotic behaviors, so the differences will be negligible and either bound can be used.
In that sense, this work is really more theoretical than practical, but still, I think, a nice result.
> a transformation that would only be possible if the bits are independent, but nowhere in his proof does he state that he is making this assumption.
Am I misunderstanding what you and/or the article means by "independent"? The fact that indexes derived from (non-overlapping) parts of a hash function output are uniformly ((preferably crypographically-secure-)psuedo-)random (and thus uncorrelated with each other and with indexes from other hash invocations) is what the phrase "hash function" means ("avalanche effect" if I remember my terminology correctly).
> The article doesn't say that the original proof was incorrect.
The article very clearly points out an error in the original proof.
The HN community can be so toxic sometimes. Inevitably whenever someone produces a new machine-checked proof, all these commenters come out of the woodwork explaining how assumptions/definitions are not verified and therefore the whole endeavor is somehow worthless.
A researcher being excited about their research is nothing to be ashamed about. I especially appreciate the fact that one of the authors took the time to make an accessible blog post to introduce us to their work.
> The article very clearly points out an error in the original proof.
We're using slightly different notions of "proof": I am talking about (1) the proof steps involved in proving a given, fixed statement. You are talking about (2) a wider notion that includes the formulation of the statement to be proved. Both of these are valid meanings for the word "proof". Coq can only check the details of sense 1, not the additional details of sense 2. The error in the original proof (sense 2) is in these additional parts, not in the proof according to sense 1.
> assumptions/definitions are not verified and therefore the whole endeavor is somehow worthless.
This is not at all what I have done.
> A researcher being excited about their research is nothing to be ashamed about.
Right. And the actual work done here is reason enough for excitement.
> I especially appreciate the fact that one of the authors took the time to make an accessible blog post to introduce us to their work.
So do I. But the fact that the target audience keeps discussing the title shows that the title was not appropriate for the target audience.
> I am talking about (1) the proof steps involved in proving a given, fixed statement. You are talking about (2) a wider notion that includes the formulation of the statement to be proved.
No, I am not. The original proof used an implicit assumption, which is a problem with the proof proper, not the formulation of the statement to be proved. Using a proof assistant guarantees that there are no implicit assumptions, which is one reason why this work is notable. It rules out an entire class of errors which were present in previous work.
>>> The article very clearly points out an error in the original proof.
You didn't say what error you meant here, but later you wrote this:
> The original proof used an implicit assumption, which is a problem with the proof proper
This is true, but this is not pointed out in the article at all, let alone "very clearly".
As established elsethread, the article's problem with the assumption is not it being implict or explicit, the authors simply didn't want to have to use the assumption at all.
It's a nice accomplishment, but even the article footnotes note that getting the definitions right for the paper was as important as verifying the actual proofs. And a proof assistant cannot fully verify your definitions, so these checks are still largely left to human scrutiny.
Just to clarify, Bose et al.'s paper was incorrect due to an incorrect definition of Stirling numbers of the second kind (some of their expressions used the wrong exponents). In our certified work, in light of this error, we ended up deriving the expression for Stirling numbers of the second kind from first principles[1], eliding it as a source of errors. As such, the main definition that needs to be human-verified in our work is the actual implementation of the Bloomfilter[2], which is fairly simple and easy to check as being correct.
> That's the highest degree of scrutiny that a proof can undergo.
No it isn't.
"Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth
The highest degree of scrutiny that a proof can undergo is to run the code and observe that it works.
It's just ('just'), that that's usually computationally intractable, because you're trying to prove things about the entire set of possible inputs, and that set is infinite or at least extremely large. So you have to settle for lower degrees of scrutiny, that can be more easily verified.
