4 ms·

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 p

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.

gopiandcode 6y ago
> 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.
- ThePhysicist 6y ago
  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.
  - gopiandcode 6y ago
    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.
    - deleted 6y ago
      [deleted]
- tom_mellior 6y ago
  > 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.
curryhoward 6y ago
> 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.
- tom_mellior 6y ago
  > 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.
  - curryhoward 6y ago
    > 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.

gopiandcode 6y ago

> 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.

ThePhysicist 6y ago
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.
- gopiandcode 6y ago
  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.
  - deleted 6y ago
    [deleted]
tom_mellior 6y ago
> 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.

curryhoward 6y ago

> 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.

tom_mellior 6y ago
> 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.
- curryhoward 6y ago
  > 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.