6 ms·

Programming will turn towards proofing correctness of trained Neural Nets. http://oregonstate.edu/ua/ncs/archives/2017/jun/research-aims-make-artificial-intelli

Programming will turn towards proofing correctness of trained Neural Nets. http://oregonstate.edu/ua/ncs/archives/2017/jun/research-aims-make-artificial-intelligence-explain-itself http://oregonstate.edu/ua/ncs/archives/2017/jun/research-aim... Until there exists a Neural Net proofen to be able to validate any contract specified for a NN to uphold. After that its unemployment, like the rest of humanity.

seanmcdirmid 9y ago
As if they would have a formally defined contract in the first place. We can't even get those for the vast majority of software we write by hand!
- emodendroket 9y ago
  And, really, what would you call writing such a thing if not a form of programming? But now we've come full circle and I'm just parroting the article.
skywhopper 9y ago
Assuming neural nets could solve every problem, who writes the formal contracts and validates the proofs? I would call the person writing the contract the "software engineer" and the prover the "QA engineer", and we're back to the status quo.
- swiley 9y ago
  You can represent any function with a neural net, it's just a matter of figuring out how to get it to learn the function. But at the end of the day you need something human (or equivalent) to validate it, and as any programmer knows it's a lot easier to understand and validate something you've written than something someone (or something) else has written.
chriswarbo 9y ago
I do think machine learning will become more mainstream, like the saying "Google uses Bayesian filtering the way Microsoft uses the if statement". Even so, if statements tend to be written by humans, compartmentalised into functions/modules/methods/etc. and plugged together to form whole systems. Microsoft software (presumably) isn't one huge `if/elif/elif/...` in a single `while` loop, even though that would suffice in theory. Likewise, I imagine Google's software isn't one giant formula, conditioned on inputs and sampled for outputs. Although many of their user-facing applications do contain a black box of this form (e.g. for translation, text-to-speech, etc.), they're only used in very narrow, well-defined tasks, and are surrounded by a huge amount of "normal" code.
falcolas 9y ago
Your comment is being dismissed (and downvoted) pretty thoroughly; but I think there's a grain of truth to it. As has been said by others, we don't get complete specs as it is, and our industry has moved towards "release often and fix the bugs or mistaken assumptions." The only real difference between the output of a NN and a human is the inference of the context to drive those assumptions. Seeding a NN would be a simple listing of invariants: Headers are at the top of the screen, footers at the bottom, there exists a name field in the page and the datastore; the name field on the page corresponds to the name field in the datastore. Once those invariants are defined, the intermediate product is released to the customers and they directly drive further development of the NN by simply saying "this is not the expected behavior" in some easy drop-down. I think the biggest hurdle will be that a human's assumptions are going to be more palatable than a NN's assumptions. But once a number of those assumptions are codified (or a statistical preference is determined), this weakness may be effectively mitigated. This "crowd-sourced" definition of correctness has already been proven - in chatbots. People have been able to coerce chat bots into providing their desired output without touching a line of code.
yoav_hollander 9y ago
Cleanly connecting NNs to contracts / rules is indeed a hard problem, which many people would like to see solved. Please see my post about that [1], and the corresponding HN comment thread [2]. [1] http://blog.foretellix.com/2017/07/06/where-machine-learning-meets-rule-based-verification/ http://blog.foretellix.com/2017/07/06/where-machine-learning... [2] https://news.ycombinator.com/item?id=14717692 https://news.ycombinator.com/item?id=14717692

seanmcdirmid 9y ago

As if they would have a formally defined contract in the first place. We can't even get those for the vast majority of software we write by hand!

emodendroket 9y ago
And, really, what would you call writing such a thing if not a form of programming? But now we've come full circle and I'm just parroting the article.

skywhopper 9y ago

Assuming neural nets could solve every problem, who writes the formal contracts and validates the proofs? I would call the person writing the contract the "software engineer" and the prover the "QA engineer", and we're back to the status quo.

swiley 9y ago
You can represent any function with a neural net, it's just a matter of figuring out how to get it to learn the function. But at the end of the day you need something human (or equivalent) to validate it, and as any programmer knows it's a lot easier to understand and validate something you've written than something someone (or something) else has written.

chriswarbo 9y ago

I do think machine learning will become more mainstream, like the saying "Google uses Bayesian filtering the way Microsoft uses the if statement". Even so, if statements tend to be written by humans, compartmentalised into functions/modules/methods/etc. and plugged together to form whole systems. Microsoft software (presumably) isn't one huge `if/elif/elif/...` in a single `while` loop, even though that would suffice in theory. Likewise, I imagine Google's software isn't one giant formula, conditioned on inputs and sampled for outputs. Although many of their user-facing applications do contain a black box of this form (e.g. for translation, text-to-speech, etc.), they're only used in very narrow, well-defined tasks, and are surrounded by a huge amount of "normal" code.

falcolas 9y ago

Your comment is being dismissed (and downvoted) pretty thoroughly; but I think there's a grain of truth to it. As has been said by others, we don't get complete specs as it is, and our industry has moved towards "release often and fix the bugs or mistaken assumptions." The only real difference between the output of a NN and a human is the inference of the context to drive those assumptions. Seeding a NN would be a simple listing of invariants: Headers are at the top of the screen, footers at the bottom, there exists a name field in the page and the datastore; the name field on the page corresponds to the name field in the datastore. Once those invariants are defined, the intermediate product is released to the customers and they directly drive further development of the NN by simply saying "this is not the expected behavior" in some easy drop-down. I think the biggest hurdle will be that a human's assumptions are going to be more palatable than a NN's assumptions. But once a number of those assumptions are codified (or a statistical preference is determined), this weakness may be effectively mitigated. This "crowd-sourced" definition of correctness has already been proven - in chatbots. People have been able to coerce chat bots into providing their desired output without touching a line of code.

yoav_hollander 9y ago

Cleanly connecting NNs to contracts / rules is indeed a hard problem, which many people would like to see solved. Please see my post about that [1], and the corresponding HN comment thread [2]. [1] http://blog.foretellix.com/2017/07/06/where-machine-learning-meets-rule-based-verification/ http://blog.foretellix.com/2017/07/06/where-machine-learning... [2] https://news.ycombinator.com/item?id=14717692 https://news.ycombinator.com/item?id=14717692