Live data from Hacker News

Neural programmer better than Quicksort

arxiv.org

41–50 of 132 posts

Re: Neural programmer better than Quicksort

#41
post #12

Earlier quoted context omitted.

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.

Call me naive but, wouldn't feeding it random input and expected output sorted by existing and proven (but slower) sorting algorithms do the trick?

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

Re: Neural programmer better than Quicksort

#42
post #21
post #12

Earlier quoted context omitted.

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.

We 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?

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

Re: Neural programmer better than Quicksort

#44
post #6

It's really hard to write correct code. Sorting was broken in java and nobody noticed for a long time: http://envisage-project.eu/wp-content/uploads/2015/02/sortin... The same was true for java's binary search: https://ai.googleblog.com/2006/06/extra-extra-read-all-about... So I am not sure I will ever trust an ML algorithm trained on inputs/outputs only (which is what I think "neural program induction" means). The a…

> "just run a final pass of insertion sort to make it useful!"

(And if this insertion sort won't complete in O(n), say <= 3n, then, fallback to Quicksort, so won't turn into O(n^2) just because the ML alg hit a corner case)

Re: Neural programmer better than Quicksort

#45

Earlier quoted context omitted.

The question is how does the algorithm perform on average, what are the pathological cases and how slow are they? How do you prove that with an algorithm that no human can reason about? Basically this paper looks like they've found an algorithm which is efficient for given sets or given classes of sets. Whether that generalizes is a different problem. It's basically a cool automatic heuristic generator.

Exactly, that’s what I thought. Although, they should be able to look at the set of instructions that generated the output, which is basically an algorithm in itself. Then they could try to prove whether that algorithm would really generalise.

[deleted]

Re: Neural programmer better than Quicksort

#46

Quite dull research wrapped in fancy words. Essentially they generate functions that map a program state to another program state and counts those function calls and compares with e.g. the number of function calls in quick sort. They "cheat" by feeding how all elements compares the their neighbours at each step. Like, if you give the algorithm that input for free what's the point. Notably, none of the popular sorting…

> They "cheat" by feeding how all elements compares the their neighbours at each step. Like, if you give the algorithm that input for free what's the point.

How is that "cheating"? The algorithm is still learning how to do a comparison-sort, which has direct applications (assuming it performs well).

Re: Neural programmer better than Quicksort

#47
post #28

The code (which is a few percent faster than quicksort) is on the last page: procedure QUICKSORTAGENT(input state) 2: Let i = 1, j = 2, l = 3, h = 4 3: if FunctionID = None then 4: return vh ← Function1(vl ← vl, vh ← vh) 5: else if FunctionID = 1 then . QuickSort 6: if vl vl then 15: return vi ← Function1(vl ← vl, vh ← vi) 16: else 17: return MoveVar(j, +1) 18: end if 19: else if prev = (vi ← Function1(vl ← vl, vh ←…

This reminds me of programming basic on an Acorn Electron. Line numbers and I don't remember indentation, though it was a few decades ago.

Ready for that COPY key!

Re: Neural programmer better than Quicksort

#48
post #46

Quite dull research wrapped in fancy words. Essentially they generate functions that map a program state to another program state and counts those function calls and compares with e.g. the number of function calls in quick sort. They "cheat" by feeding how all elements compares the their neighbours at each step. Like, if you give the algorithm that input for free what's the point. Notably, none of the popular sorting…

> They "cheat" by feeding how all elements compares the their neighbours at each step. Like, if you give the algorithm that input for free what's the point. How is that "cheating"? The algorithm is still learning how to do a comparison-sort, which has direct applications (assuming it performs well).

So do they feed such information only when training the system?

Re: Neural programmer better than Quicksort

#49
post #21

Earlier quoted context omitted.

We 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?

"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 r…

Your 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?

Re: Neural programmer better than Quicksort

#50
post #46

Earlier quoted context omitted.

> They "cheat" by feeding how all elements compares the their neighbours at each step. Like, if you give the algorithm that input for free what's the point. How is that "cheating"? The algorithm is still learning how to do a comparison-sort, which has direct applications (assuming it performs well).

So do they feed such information only when training the system?

You can generate that input only when needed. So whenever the sorting algorithm asks whether A[i] > A[i+1], you can perform the comparison there and then. So the answer to your question is yes.
Post reply on HN