5 ms·

Proofs are a pretty important part of algorithm development. Proofs of correctness as well as proofs of algorithmic complexity bounds. At the moment that doesn'

Proofs are a pretty important part of algorithm development. Proofs of correctness as well as proofs of algorithmic complexity bounds. At the moment that doesn't seem like something this type of approach can do much for, though perhaps it could be combined with work on automated theorem proving.

alexmolas 4y ago
but in this case, it's extremely easy to prove that the algorithm that they propose is correct, or am i missing something?
- eigenket 4y ago
  "Correct" means different things in different contexts. In a fairly standard application of matrix multiplication you don't multiply matrices A and B to get AB, instead you have some floating point approximation to A, and some floating point approximation to B, and you want something that you can be confident approximates AB with some bounds. The two most important characteristics of an algorithm are the runtime and the error bounds you can prove. Someone smart once said getting the wrong answer in time O(1) is very easy.
  - bheadmaster 4y ago
    > Someone smart once said getting the wrong answer in time O(1) is very easy. Reminds me of a joke about a guy at a job interview: "So, what kind of skills do you have?" "I can do mental multiplication really fast." "Ok, what's 102 times 376?" "87843" [enters numbers in calculator] "That wasn't even close to correct." "Yeah, but it was fast."
  - DannyBee 4y ago
    Sorry, but this simply does not make any sense. Algorithmic correctness does not vary in different contexts. Algorithmic usefulness/applicability does. You are confusing the two. Correctness here means that it provably generates a result that meets the definition of correct matrix multiplication. In this case, they prove that all algorithms generated do (and that the system will actually only generate provably correct algorithms). Applicability here is whether, when applied to a particular {not-infinite precision computer, use case}, it is viable to use it. That does not affect whether the algorithm is correct or not, only whether you can use it to achieve a particular result. If i have a computer with 1 bit of floating point precision, that does not make the algorithms all suddenly incorrect. Within the bounds of the what i can provide (not a lot), they still function exactly as they are supposed to. If i need 75 significant digits on this computer, it simply means that they are not useful for my computer because it cannot generate enough significant digits from them to be useful. That is totally orthogonal to whether the algorithms function as designed.
    - deleted 4y ago
      [deleted]
    - eigenket 4y ago
      An algorithm for "matrix multiplication" that assumes infinite precision arithmetic is used is essentially useless (there are some niche uses for matrices with entries in finite fields/rings). An algorithm for matrix multiplication usually comes with more than that, in particular some sort of error bound. Note that these bounds are mathematical, part of the abstract algorithm, and not something that is a property of any particular implementation (your last paragraph suggests you might be confused by this). You want a statement that says if A' is close to A (in some relevant distance measure), and B' is close to B, then your algorithm gives something close to AB. The correctness you have to prove includes proving that your error bounds are what you say they are.
      - DannyBee 4y ago
        Again, useless is not the same as incorrect. It is still correct whether it can be used somewhere due to implementation limitations or not. I'm really unsure how you can possibly argue otherwise. It's like arguing that a string algorithm is incorrect because it doesn't run fast enough on strings to be usable on any current computer. It's still correct. It's just not usable. Unlike correctness, useless is very context specific. 100 years from now, an infinite precision arithmetic algorithm may be entirely useful.
        eigenket 4y ago
        I am arguing that a matrix multiplication algorithm, like essentially any other numerical algorithm, consists of (at least) the following two parts 1. The actual steps you have to follow. 2. Some form of error bounds/analysis that tell you how good/bad the output will be given approximate inputs. In order to prove correctness you have to prove that the procedure gives the error bounds you claim. The error bounds are something you mathematically have to prove.
        4y ago
  - topaz0 4y ago
    I haven't read the paper, but from the blog post I get the sense that finite fields is one of the main claims of usefulness for this result. I do agree that "'correct' means different things in different contexts."
DannyBee 4y ago
These algorithms are provably correct, and it will only generate provably correct algorithms (as the paper goes into).

alexmolas 4y ago

but in this case, it's extremely easy to prove that the algorithm that they propose is correct, or am i missing something?

eigenket 4y ago
"Correct" means different things in different contexts. In a fairly standard application of matrix multiplication you don't multiply matrices A and B to get AB, instead you have some floating point approximation to A, and some floating point approximation to B, and you want something that you can be confident approximates AB with some bounds. The two most important characteristics of an algorithm are the runtime and the error bounds you can prove. Someone smart once said getting the wrong answer in time O(1) is very easy.
- bheadmaster 4y ago
  > Someone smart once said getting the wrong answer in time O(1) is very easy. Reminds me of a joke about a guy at a job interview: "So, what kind of skills do you have?" "I can do mental multiplication really fast." "Ok, what's 102 times 376?" "87843" [enters numbers in calculator] "That wasn't even close to correct." "Yeah, but it was fast."
- DannyBee 4y ago
  Sorry, but this simply does not make any sense. Algorithmic correctness does not vary in different contexts. Algorithmic usefulness/applicability does. You are confusing the two. Correctness here means that it provably generates a result that meets the definition of correct matrix multiplication. In this case, they prove that all algorithms generated do (and that the system will actually only generate provably correct algorithms). Applicability here is whether, when applied to a particular {not-infinite precision computer, use case}, it is viable to use it. That does not affect whether the algorithm is correct or not, only whether you can use it to achieve a particular result. If i have a computer with 1 bit of floating point precision, that does not make the algorithms all suddenly incorrect. Within the bounds of the what i can provide (not a lot), they still function exactly as they are supposed to. If i need 75 significant digits on this computer, it simply means that they are not useful for my computer because it cannot generate enough significant digits from them to be useful. That is totally orthogonal to whether the algorithms function as designed.
  - deleted 4y ago
    [deleted]
  - eigenket 4y ago
    An algorithm for "matrix multiplication" that assumes infinite precision arithmetic is used is essentially useless (there are some niche uses for matrices with entries in finite fields/rings). An algorithm for matrix multiplication usually comes with more than that, in particular some sort of error bound. Note that these bounds are mathematical, part of the abstract algorithm, and not something that is a property of any particular implementation (your last paragraph suggests you might be confused by this). You want a statement that says if A' is close to A (in some relevant distance measure), and B' is close to B, then your algorithm gives something close to AB. The correctness you have to prove includes proving that your error bounds are what you say they are.
    - DannyBee 4y ago
      Again, useless is not the same as incorrect. It is still correct whether it can be used somewhere due to implementation limitations or not. I'm really unsure how you can possibly argue otherwise. It's like arguing that a string algorithm is incorrect because it doesn't run fast enough on strings to be usable on any current computer. It's still correct. It's just not usable. Unlike correctness, useless is very context specific. 100 years from now, an infinite precision arithmetic algorithm may be entirely useful.
      - eigenket 4y ago
        I am arguing that a matrix multiplication algorithm, like essentially any other numerical algorithm, consists of (at least) the following two parts 1. The actual steps you have to follow. 2. Some form of error bounds/analysis that tell you how good/bad the output will be given approximate inputs. In order to prove correctness you have to prove that the procedure gives the error bounds you claim. The error bounds are something you mathematically have to prove.
        4y ago
- topaz0 4y ago
  I haven't read the paper, but from the blog post I get the sense that finite fields is one of the main claims of usefulness for this result. I do agree that "'correct' means different things in different contexts."

DannyBee 4y ago

These algorithms are provably correct, and it will only generate provably correct algorithms (as the paper goes into).