3 ms·

Suggestion to rely on AI for proof verification is just laughable. Neuron weights instead of formal definitions. So reliable.

drchewbacca 7y ago
It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail. Here is an example. https://arxiv.org/pdf/1608.02644.pdf https://arxiv.org/pdf/1608.02644.pdf
6gvONxR4sf7o 7y ago
That's not the suggestion. Proof verification is easy (for a proof written in a formal system). Proof search is hard. Many (most/all?) proof assistants heavily use heuristics to guide the proof search. Machine learning on a database of proofs could lead to superior heuristics and make proving stuff in the formal systems easier. Proving stuff in these systems is still harder than natural language proofs, so making them easier could increase adoption, which would make mathematicians' results more robust/rigorous.
not2b 7y ago
You seem to think "AI" means machine learning. In this case it does not. Theorem prover systems don't use neural nets.
- higherkinded 7y ago
  Okay but they are formal systems and don't have anything to do with AI either, do they?
YeGoblynQueenne 7y ago
Proof assitants have nothing to do with neural nets or optimisation. They are entirely determinitsic and return an absolute "true" or "false" result, not an approximation. https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant This is Good Old-Fashioned AI, through and through.
digama0 7y ago
Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching). No one in ITP is seriously using modern neural net based AI in real theorem provers yet, although there are several research teams working on it.

drchewbacca 7y ago

It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail. Here is an example. https://arxiv.org/pdf/1608.02644.pdf https://arxiv.org/pdf/1608.02644.pdf

6gvONxR4sf7o 7y ago

That's not the suggestion. Proof verification is easy (for a proof written in a formal system). Proof search is hard. Many (most/all?) proof assistants heavily use heuristics to guide the proof search. Machine learning on a database of proofs could lead to superior heuristics and make proving stuff in the formal systems easier. Proving stuff in these systems is still harder than natural language proofs, so making them easier could increase adoption, which would make mathematicians' results more robust/rigorous.

not2b 7y ago

You seem to think "AI" means machine learning. In this case it does not. Theorem prover systems don't use neural nets.

higherkinded 7y ago
Okay but they are formal systems and don't have anything to do with AI either, do they?

YeGoblynQueenne 7y ago

Proof assitants have nothing to do with neural nets or optimisation. They are entirely determinitsic and return an absolute "true" or "false" result, not an approximation. https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant This is Good Old-Fashioned AI, through and through.

digama0 7y ago

Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching). No one in ITP is seriously using modern neural net based AI in real theorem provers yet, although there are several research teams working on it.