6 ms·

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!

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?

zozbot234 6y ago
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.
- gopiandcode 6y ago
  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. [1] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7dbd5b8e38b48041dfd4bd261a/Utils/stirling.v#L341 https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d... [2] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7dbd5b8e38b48041dfd4bd261a/Structures/BloomFilter/BloomFilter_Definitions.v#L98 https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d...
tom_mellior 6y ago
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.
a1369209993 6y ago
> 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.

zozbot234 6y ago

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.

gopiandcode 6y ago
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. [1] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7dbd5b8e38b48041dfd4bd261a/Utils/stirling.v#L341 https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d... [2] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7dbd5b8e38b48041dfd4bd261a/Structures/BloomFilter/BloomFilter_Definitions.v#L98 https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d...

tom_mellior 6y ago

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.

a1369209993 6y ago

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