AI is coming for my job!

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

AI is coming for my job!

Tim Daly
Generating Correctness Proof with Neural Networks
https://arxiv.org/pdf/1907.07794.pdf

Apparently they managed to prove 15.77% of the proofs in
the CompCert verified compiler effort.

"Now, here, you see, it takes all the running you can do to
keep in the same place. If you want to get somewhere else,
you must run at least twice as fast as that."
   -- Alvin Toffler "Future Shock" :-)

Tim

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: AI is coming for my job!

Frank Pfenning
I would venture the proofs are not the real effort in CompCert.
The real effort is to formulate the various systems such that the
proofs become as simple as possible.  So 15.77% is minuscule
compared to the total intellectual effort of this project.  Your job
is not yet in danger (even in your retirement :-)

But, seriously, sometimes I am worried that too much automation
is a bad thing, because it can mask the flaws in what one is doing.
There are many examples in the study of logics, but let me use
programming instead.  Start with your favorite terrible programming language
(Python happens to be a convenient target, or C++).  Now, sure, you can
reduce the number of bugs with automatic program analysis, the smarter
the better.  But you would nevertheless still be better off in a statically typed
functional language with a decent module system.  You prop up something
that would be better left to wither and die.

  - Frank

On Sun, Jul 21, 2019 at 8:29 AM Tim Daly <[hidden email]> wrote:
Generating Correctness Proof with Neural Networks
https://arxiv.org/pdf/1907.07794.pdf

Apparently they managed to prove 15.77% of the proofs in
the CompCert verified compiler effort.

"Now, here, you see, it takes all the running you can do to
keep in the same place. If you want to get somewhere else,
you must run at least twice as fast as that."
   -- Alvin Toffler "Future Shock" :-)

Tim


--
Frank Pfenning, Professor
Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213-3891

+1 412 268-6343
GHC 6017


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer