5 ms·

Depending on the context, it might be a good idea to use the probabilistic approach: feed it a predefined number of variables and see if the results match. A s

by ulucs 9y ago

Depending on the context, it might be a good idea to use the probabilistic approach: feed it a predefined number of variables and see if the results match. A similar method is used in matrices to compute AB =? C in O(n^2) time (you check a predefined number of rows). You get O(n^2.something) if you do the actual multiplication

mlevental 9y ago
>Depending on the context, it might be a good idea to use the probabilistic approach: feed it a predefined number of variables and see if the results match. for any input space in which a finite number of checks has greater than literally 0% (measure zero) of being representative this problem is trivial (finite space).
- Sharlin 9y ago
  Trivial in the math sense. Not trivial in the real-world programming sense. Very different things.
  - tikhonj 9y ago
    This is an important point: even a finite search space quickly gets out of hand in practical terms. I've worked a bit on bounded verification which comes down to comparing loop-free programs with finite inputs for equality. It is not easy in practice! Modern approaches use sophisticated proof search algorithms (ie SMT solvers) and still struggle to scale beyond relatively small and simple programs. I don't know the numbers off-hand because verification was not the bottleneck in my application, but I suspect that even sophisticated modern methods scale poorly beyond a few hundred instructions or for large inputs (ie algorithms with complex behavior over arrays). If you have a function that takes a single 32-bit floating point input and runs in, say, 100 cycles, you can test all the possible inputs in a couple minutes or so. If you have multiple floats as inputs or the function is more complex, you can exhaustively check it with an SMT solver or the like. If your function depends on hundreds or thousands of inputs and has complex looping logic, you probably can't exhaustively check it with any automated solution. Real programs, of course, are orders of magnitude more complex than even the last example. Verifying them automatically is effectively impossible even if they have finite inputs, guaranteed bounds on loops and are "trivial" in the mathematical sense.
brchr 9y ago
One of the key results on the role of randomness in polynomial identity testing is what's called the Schwartz–Zippel lemma.[1] As the wiki article states, "Currently, there is no known sub-exponential time algorithm that can solve this problem deterministically. However, there are randomized polynomial algorithms for testing polynomial identities." [1]https://en.wikipedia.org/wiki/Schwartz–Zippel_lemma https://en.wikipedia.org/wiki/Schwartz–Zippel_lemma (Note that this is in the context specifically of polynomial function equivalence.)
tlb 9y ago
Short functions can be equivalent for all but a vanishingly small subset of inputs: f1(x) = (x==7239829489) ? 0 : x f2(x) = x so randomized tests would probably say they are equivalent.
- quickthrower2 9y ago
  This is the same problem for unit tests even with 100% code coverage.
- dxbydt 9y ago
  very good counterexample, thank you!
sp332 9y ago
From 2014: "There are only 4 billion floats - so test them all!" https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
SilasX 9y ago
To adapt the joke[1]: That's fine if you just need a high enough confidence for military encryption or financial transactions. But what if you're trying to prove a theorem about them, and just can't take any chances? [1] Believe it was in Aaronson's Quantum Computing Since Democritus
hiker 9y ago
The way I see it there's a whole spectrum of methods for checking program correctness. On the one end are "point tests", manually written tests that check correctness in several predetermined cases. That's what most software engineers mean by "testing". Then comes randomized tests/fuzz testing/QuickCheck where properties are defined to hold for all values of some variables and then can be checked on randomly generated values. This offers better correctness guarantees than manually created "point tests" but might still miss failing cases since it's sampling and not exhaustively searching through the whole space. Finally, on the far end are proofs, where one formally proves that the formerly mentioned properties always hold. I cannot imagine a stronger guarantee that something holds than an actual mathematical proof of it. Dependently typed languages (Agda, Idris, Coq, Lean, etc) push software development into that far end where correctness can actually be proved. Imo that's where the future of software lays for certain classes of programs where correctness is a must. Here's a proof of the original question in Lean: def foo : (λ x, 2 * x) = (λ x, x + x) := begin apply funext, intro x, cases x, { refl }, { simp at *, dsimp [has_mul.mul, nat.mul], have zz : Π a : nat, 0 + a = a := by simp at *, rw zz } end

by ulucs 9y ago

mlevental 9y ago

>Depending on the context, it might be a good idea to use the probabilistic approach: feed it a predefined number of variables and see if the results match. for any input space in which a finite number of checks has greater than literally 0% (measure zero) of being representative this problem is trivial (finite space).

Sharlin 9y ago
Trivial in the math sense. Not trivial in the real-world programming sense. Very different things.
- tikhonj 9y ago
  This is an important point: even a finite search space quickly gets out of hand in practical terms. I've worked a bit on bounded verification which comes down to comparing loop-free programs with finite inputs for equality. It is not easy in practice! Modern approaches use sophisticated proof search algorithms (ie SMT solvers) and still struggle to scale beyond relatively small and simple programs. I don't know the numbers off-hand because verification was not the bottleneck in my application, but I suspect that even sophisticated modern methods scale poorly beyond a few hundred instructions or for large inputs (ie algorithms with complex behavior over arrays). If you have a function that takes a single 32-bit floating point input and runs in, say, 100 cycles, you can test all the possible inputs in a couple minutes or so. If you have multiple floats as inputs or the function is more complex, you can exhaustively check it with an SMT solver or the like. If your function depends on hundreds or thousands of inputs and has complex looping logic, you probably can't exhaustively check it with any automated solution. Real programs, of course, are orders of magnitude more complex than even the last example. Verifying them automatically is effectively impossible even if they have finite inputs, guaranteed bounds on loops and are "trivial" in the mathematical sense.

brchr 9y ago

One of the key results on the role of randomness in polynomial identity testing is what's called the Schwartz–Zippel lemma.[1] As the wiki article states, "Currently, there is no known sub-exponential time algorithm that can solve this problem deterministically. However, there are randomized polynomial algorithms for testing polynomial identities." [1]https://en.wikipedia.org/wiki/Schwartz–Zippel_lemma https://en.wikipedia.org/wiki/Schwartz–Zippel_lemma (Note that this is in the context specifically of polynomial function equivalence.)

tlb 9y ago

Short functions can be equivalent for all but a vanishingly small subset of inputs: f1(x) = (x==7239829489) ? 0 : x f2(x) = x so randomized tests would probably say they are equivalent.

quickthrower2 9y ago
This is the same problem for unit tests even with 100% code coverage.
dxbydt 9y ago
very good counterexample, thank you!

sp332 9y ago

From 2014: "There are only 4 billion floats - so test them all!" https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...

SilasX 9y ago

To adapt the joke[1]: That's fine if you just need a high enough confidence for military encryption or financial transactions. But what if you're trying to prove a theorem about them, and just can't take any chances? [1] Believe it was in Aaronson's Quantum Computing Since Democritus

hiker 9y ago

The way I see it there's a whole spectrum of methods for checking program correctness. On the one end are "point tests", manually written tests that check correctness in several predetermined cases. That's what most software engineers mean by "testing". Then comes randomized tests/fuzz testing/QuickCheck where properties are defined to hold for all values of some variables and then can be checked on randomly generated values. This offers better correctness guarantees than manually created "point tests" but might still miss failing cases since it's sampling and not exhaustively searching through the whole space. Finally, on the far end are proofs, where one formally proves that the formerly mentioned properties always hold. I cannot imagine a stronger guarantee that something holds than an actual mathematical proof of it. Dependently typed languages (Agda, Idris, Coq, Lean, etc) push software development into that far end where correctness can actually be proved. Imo that's where the future of software lays for certain classes of programs where correctness is a must. Here's a proof of the original question in Lean: def foo : (λ x, 2 * x) = (λ x, x + x) := begin apply funext, intro x, cases x, { refl }, { simp at *, dsimp [has_mul.mul, nat.mul], have zz : Π a : nat, 0 + a = a := by simp at *, rw zz } end