Automated theorem proving by learning from examples
post by Alex Flint (alexflint) · 2011-02-16T13:38:03.753Z · LW · GW · Legacy · 9 commentsContents
9 comments
Does anyone know of work that attempts to build a theorem prover by learning-from-examples? I'm imagining extracting a large corpus of theorems from back issues of mathematical journals, then applying unsupervised structure discovery techniques from machine learning to discover recurring patterns.
Perhaps a model of the "set of theorems that humans tend to produce" would be helpful in proving new theorems.
The unsupervised-structure-discovery bit does seem within the realm of current machine learning.
Any references to related work?
9 comments
Comments sorted by top scores.
comment by timtyler · 2011-02-16T13:57:20.811Z · LW(p) · GW(p)
Most theorems are not presented in a very machine-friendly format, I believe.
Replies from: alexflint↑ comment by Alex Flint (alexflint) · 2011-02-16T20:52:51.844Z · LW(p) · GW(p)
Yes but parsing theorems (at least at the syntactic level) should be no harder than parsing English, and we do lots of reasonably smart text mining, and even some reasonable natural language translation.
Replies from: timtylercomment by moonbatmemehack · 2011-02-17T04:24:52.596Z · LW(p) · GW(p)
Theorems are not generally presented in math journals in the way they were discovered, so I am not sure machine learning from journal articles would greatly help in discovery. The issue is really that going from question to answer is a different process from verifying an answer is correct, or guiding a reader through such a verification which is what a proof is.
A perhaps less lofty, but still incredibly useful, goal would be automating a process for simplifying proofs
Or alternatively convincing mathematicians to narrate their own mental process of discovery.
comment by cousin_it · 2011-02-16T14:27:00.301Z · LW(p) · GW(p)
Again I'll have to agree with timtyler. Formalizing mathematical proofs is difficult, see my old post. Maybe you'll find it easiest to use an existing corpus, like Metamath.
Replies from: alexflint↑ comment by Alex Flint (alexflint) · 2011-02-17T09:15:00.269Z · LW(p) · GW(p)
Ooh, thanks for the link to metamath.
comment by JoshuaZ · 2011-02-16T16:13:19.631Z · LW(p) · GW(p)
There's been some work on getting machines to try to make reasonable conjectures and definitions (see for example the work of Simon Colton) but I'm not aware of any work of actually trying to teach machines. I suspect this would be very difficult since most machine learning systems work best when the problems are in some vague sense fuzzy rather than formal.
Replies from: Vladimir_Nesov↑ comment by Vladimir_Nesov · 2011-02-16T17:39:10.159Z · LW(p) · GW(p)
The problem of deciding which definitions are interesting is far from being formal.
Replies from: alexflint↑ comment by Alex Flint (alexflint) · 2011-02-16T20:58:53.163Z · LW(p) · GW(p)
Yes, and the problem of deciding which lemmas to prove and in general what structure to try for a proof is also far from begin formal. Verifying a proposed proof is the formal bit.