3 ms·
Here's what I forsee. GPT3 (or the like) learns strategies to solve problems in a limited DSL (like isabelle). Prompt GPT3 with a problem (e.g. P = NP). Have
by dnautics 6y ago
Here's what I forsee. GPT3 (or the like) learns strategies to solve problems in a limited DSL (like isabelle). Prompt GPT3 with a problem (e.g. P = NP). Have it walk down the tree of proof possibilities (possibly using Q-learning), trim incorrect branches, and then out comes a proof. Somewhere in its modestly coherent glossolalia, GPT3 will figure out how to prove something "tough for humans" correct. Nice thing is, you might even be able to paralellize the search using independent agents.
Is there anyone working on this? Drop a line.
- serendipityrecs 6y agoI ran some experiments with GPT3+proofs. You can read about it here: http://serendipityrecs.com/blog/posts/experiments-with-gpt-3/#experiment-3-writing-proofs http://serendipityrecs.com/blog/posts/experiments-with-gpt-3... I wasn't able to get it to return anything interesting but I also didn't spend a lot of time refining the approach (this was just a series of quick and dirty experiments, ultimately I identified recommendations as a good use case for GPT-3 and started building a product around it.) I think it will be interesting to use GPT-3 in conjunction with existing automated/machine proof techniques. Since GPT-3 doesn't "know" anything, automated proof systems can help the system stay logically consistent.
- sukilot 6y agoGPT-3 is approximate remixes of old text. How is that at all relevant to theorem proving, which is a search problem?
- serendipityrecs 6y agoAny proof is also a remix of old text (and often times old ideas too)