5 ms·
Next step is to prove the ML-produced algorithm is correct. I can see a world where we generate algorithms and then automatically prove they're correct based on
by nardi 6y ago
Next step is to prove the ML-produced algorithm is correct. I can see a world where we generate algorithms and then automatically prove they're correct based on a formal description of the problem being solved.
- rusticpenn 6y agoWell designed ML techniques are always correct 99% of the time. Its the 1% that is the problem.
- ukj 6y ago99% of the time it works all of the time. Like humans. How do we deal with problematic humans? Retraining or replacement.
- adrianN 6y agoNo, we deal with 99% accuracy in humans by designing all our human-based algorithms to be resilient against mistake (and still mistakes in the end result happen very frequently). This is completely different from the way we have designed our computer systems, because it's way easier to do this with flexible agents like humans than with inflexible agents like computers.
- ukj 6y agoSo, the mistakes algorithms make are different to the mistakes humans make? That’s... equivocation. Both humans and ML algorithms are flexible. That is the point of “learning”. Adaptation.
- Random_ernest 6y agoBut the problems where we apply human labour are vastly different from the ones where we apply machine labour. In (most) tasks where we apply human labour a few errors are tolerated.
- ukj 6y agoThis seems irrelevant. Neither humans nor ML make zero errors. Ceteris paribus, if an ML algorithm makes fewer errors at a task which with low error tolerance - you would use the algorithm instead of the human, no?
- mtrower 6y agoI would expect that might depend on what sort of errors each make, no?
- bryanrasmussen 6y agowhat's the promote option in this analogy?
- ukj 6y agoML took your job.
- fiblye 6y agoWith humans, we can ask what went wrong and fix the problem. With black box algorithms, we throw in some new training data and just hope it's enough.
- andybak 6y ago> With humans, we can ask what went wrong and just hope we've fixed the problem. > With black box algorithms, we throw in some new training data and just hope it's enough. A small wording change and they're equivalent again. To some extent human beings are also a black box - with some very peculiar failure conditions and side-channel weaknesses.
- bufferoverflow 6y agoNo, we don't do anything against the humans who are 99% correct. 99% is good enough in most real world cases.
- rusticpenn 6y agoThat is not practical when you expect the system to be correct 100% of the time and make decisions based on that. There are many situations where this is critical. You would never want your car's safety system to be correct only 99% of the time.
- AlphENsign_Tech 6y agofrom the volumetric standpoint, the 99% is their huge specially curated training and test data.
- adrianN 6y agoWe suck really hard at proving code correct that was written explicitly with the goal in mind to be formally verified. The techniques there are still quite immature. I wonder how long it will take until we have a reasonably working pipeline of ML+formal verification. Maybe it's just easier to generate correct code from the spec than to learn it from examples and then verifying it with the specification?
- hutzlibu 6y ago"We suck really hard at proving code correct that was written explicitly with the goal in mind to be formally verified." That is why I am not a huge fan of proving code in the first place. If you have a really complicated proof of formal correctness, then who guarantees you, there is no misstake in the proof itself? At least this is what I have seen in university, lots of complicated stuff on the whiteboard, with a result. And then someone figured out, it was wrong. So I rather do lots of testing, for all known test cases.
- adrianN 6y agoYour automatic proof checker guarantees that there is no mistake in the proof. That's the easy part! The real question is who guarantees that your specification is what you actually want?
- infinity0 6y agoAutomatic proof checkers still have bugs in them. However, one nice characteristic is that, since its algorithms are so general, i.e. about the language rather than about the problem you're solving (e.g. sorting), any bugs in the checker are either so common they hit every problem solution and are easily discovered and fixed, or so rare that it affects no real-world problem solutions.
- adrianN 6y agoThe kernel of an automatic proof checker is much easier to test and verify than the programs you verify using a proof checker though.
- Cthulhu_ 6y agoCall me naive but, wouldn't feeding it random input and expected output sorted by existing and proven (but slower) sorting algorithms do the trick?
- Scea91 6y agoFor an exact proof of correctness no, because that would only show the algorithm is correct for a selected set of input-output pairs. However, it is true that validating it for a very large number of inputs and outputs has value. This is not uncommon even in mathematics. For example, Goldbach's Conjecture (https://www.wikiwand.com/en/Goldbach%27s_conjecture https://www.wikiwand.com/en/Goldbach%27s_conjecture) has not been proven but has been shown to hold for all integers less than 4 × 10^18
- exdsq 6y agoThis is done! The existing correct algorithm is called the oracle and it’s used to validate the generated algorithm. There’s some cool work on using neural program induction in compilers to try generate faster implementations based off the ‘oracle’ program that’s being compiled.
- algo_trader 6y ago> neural program induction in compilers to try generate faster implementations Can u provide more details? I am familiar with garden-variety ML-optimization-of-combinatorical-space in compilers. How would u even "measure" the expected performance unless these are gradual greedy changes
- bufferoverflow 6y agoIt doesn't need to be 100% correct. There's a place for fast sorting algorithms which are correct most of the time - basically anything non-critical, like sorting comments by upvotes. According to the article, they couldn't find a case where it wasn't correct.
- jcelerier 6y ago> There's a place for fast sorting algorithms which are correct most of the time - basically anything non-critical, like sorting comments by upvotes. Nothing saddens me more than this trend of the modern web where everything works semi-probabilistically (even if it's likely for "good" technical reasons, such as, "we wrote our server backend in Ruby which is slow as molasses so now we need 230 CDN and 800 databases instances around the whole world and transformed our simple centralized problem into an horrendous decentralized one). The central reason for me to use computers is that they are (or at least were) deterministic to a much higher degree that normal life, and so many things in the 10 last years becoming much more non-deterministic in particular on social websites is something that frustrates me every single day as it just makes the whole experience and process of using computers & the web very unreliable compared to what it used to be.
- diegoperini 6y agoToday's perfections are yesterday's "good enoughs". Don't be sad for the trend. In 10 years, you will have new perfections to enjoy.
- UncleOxidant 6y agoLike the probabilistic bank account balance. "You have between $10 and $1000 with the greatest likelihood being $537 (52% chance)."
- FabHK 6y agoThere was this thread a while ago with HSBC switching to MongoDB... so, yeah, distinct possibility :-) https://news.ycombinator.com/item?id=23507197 https://news.ycombinator.com/item?id=23507197 (The article was very light on details though, and it was probably just one team that consolidated to MongoDB, not the accounts itself... one hopes.)