Live data from Hacker News

Neural programmer better than Quicksort

arxiv.org

51–60 of 132 posts

Re: Neural programmer better than Quicksort

#51
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.

The Electron had a new enough version of BBC Basic that "proper" procedures and UDFs were supported (in a limited fashion, but well enough considering the constraints of the machine) so you could pretty much ignore line numbers, in fact by using a text editor and TYPEing the result into BASIC you could write code without them (the interpreter needed them, the TYPE trick made it put them in for itself).

But yes, this was uncommon so line numbers were a major thing.

And indentation was optional, you could add extra spaces to the start of lines and they would be kept and would have no effect on execution, but you would be wasting precious bytes of RAM and if using one of the heavier display modes (0, 1 or 2) you would only have 8.5Kbyte to play with for all the code and run-time storage (your variables, BASIC's call stack).

Re: Neural programmer better than Quicksort

#52
post #17

Evolving sorting networks was cool. This is not cool.

"We don't have a formal proof for this, and only have empirical evidence, measured on a large number of test instances. More on this in the paper. The learned algorithm is not entirely opaque. I'd argue it is easier to understand its behavior than that of a neural net." https://mobile.twitter.com/liyuajia/status/12815201991083089...

agreed, this is kind of backwards research

Re: Neural programmer better than Quicksort

#53

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…

This is absolutely not cheating; every hand designed algorithm can access and compare everything in the array!

The real point of what they’re saying in your italicized quote is actually that giving the net full access hinders efficiency, so they actually restrict it. Almost like the opposite of cheating.

Re: Neural programmer better than Quicksort

#54
post #49

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

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

Re: Neural programmer better than Quicksort

#55
post #49

Earlier quoted context omitted.

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?

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

The kernel of an automatic proof checker is much easier to test and verify than the programs you verify using a proof checker though.

Re: Neural programmer better than Quicksort

#56
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…

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

Re: Neural programmer better than Quicksort

#57

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 ←…

Was this "discovered" by their system or was it hand-crafted by the authors from their custom instruction set elements ?

Re: Neural programmer better than Quicksort

#58
post #56

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

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

Tests are simple to unterstand.

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.

Re: Neural programmer better than Quicksort

#59
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)

Possibly better would be Timsort (used in Python, Java, V8, etc.), as it's "designed to take advantage of runs of consecutive ordered elements that already exist": https://en.wikipedia.org/wiki/Timsort

Re: Neural programmer better than Quicksort

#60
post #57

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 ←…

Was this "discovered" by their system or was it hand-crafted by the authors from their custom instruction set elements ?

As I understand it they designed quicksort like that to be able to train with it. It is quite clear from the video where it is called "quick sort agent" compared to the model one and function1 and function2 is in the stack trace.

"We found adding the previously executed action to the input state st is sufficient to handle dis-ambiguation for this quick sort implementation. Alg. 8 shows the converted quick sort scripted agent"

Post reply on HN