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.
According to the article, they couldn't find a case where it wasn't correct.
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.
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.)
This trend seems to be everwhere
Stackoverflow was just using 4 db servers in 2016 (https://nickcraver.com/blog/2016/02/17/stack-overflow-the-ar...)
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.
How is this any different? You can still make mistakes in your test code, test data, omit cases that would fail, etc. I think I'd be less confident in a set of unit tests than I would with an automated proof checker.
Complicated proofs I do not understand, without much effort.
And I surely know that you can make mistakes with test cases as well. So I surely do not claim my way to be superior. But it works way better for me.
Especially the test cases needed to trigger some deep bug.
Like humans.
How do we deal with problematic humans?
Retraining or replacement.
That’s... equivocation.
Both humans and ML algorithms are flexible. That is the point of “learning”.
Adaptation.
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?
With black box algorithms, we throw in some new training data and just hope it's enough.
> 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.
Perfect is the enemy of good enough.
I suppose it depends on your end goals.
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) has not been proven but has been shown to hold for all integers less than 4 × 10^18
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.
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