formal proof

From Stampy's Wiki
Formal proof
formal proof
Alignment Forum Tag
Wikipedia Page

Description

A Formal Proof is a finite sequence of steps from axiom(s) or previous derived proof(s) which strictly follow the allowed rules of inference of the mathematical system in which it exists. They are used to establish statements as true within a mathematical framework in a way which can be independently verified with extremely high certainty, with the most reliable flavor of proof being machine-checked proofs generated by proof assistants since they have even less room for human error.

A Formal Proof is a finite sequence of steps from axiom(s) or previous derived proof(s) which strictly follow the allowed rules of inference of the mathematical system in which it exists. They are used to establish statements as true within a mathematical framework in a way which can be independently verified with extremely high certainty, with the most reliable flavor of proof being machine-checked proofs generated by proof assistants since they have even less room for human error.

Canonically answered

Can people contribute to alignment by using proof assistants to generate formal proofs?

Show your endorsement of this answer by giving it a stamp of approval!
80k links to an article on high impact careers in formal verification in the few paragraphs they've written about formal verification.
80k links to an article on high impact careers in formal verification in the few paragraphs they've written about formal verification.

Some other notes

  • https://github.com/deepmind/cartesian-frames I emailed Scott about doing this in coq before this repo was published and he said "I wouldn't personally find such a software useful but sounds like a valuable exercise for the implementer" or something like this.
  • When I mentioned the possibility of rolling some of infrabayesianism in coq to diffractor he wasn't like "omg we really need someone to do that" he was just like "oh that sounds cool" -- I never got around to it, if I would I'd talk to vanessa and diffractor about weakening/particularizing stuff beforehand.
  • if you extrapolate a pattern from those two examples, you start to think that agent foundations is the principle area of interest with proof assistants! and again- does the proof assistant exercise advance the research or provide a nutritious exercise to the programmer?
  • A sketch of a more prosaic scenario in which proof assistants play a role is "someone proposes isInnerAligned : GradientDescent -> Prop and someone else implements a galaxybrained new type theory/tool in which gradient descent is a primitive (whatever that means)", when I mentioned this scenario to Buck he said "yeah if that happened I'd direct all the engineers at redwood to making that tool easier to use", when I mentioned that scenario to Evan about a year ago he said didn't seem to think it was remotely plausible. probably a nonstarter.