12
$\begingroup$

Although there already exists active research area, so-called, automated theorem proving, mostly work on logic and elementary geometry.

Rather than only logic and elementary geometry, are there existing research results which by using machine learning techniques(possibly generative learning models) to discover new mathematical conjectures (if not yet proved), in wider branches of mathematics such as differential geometry, harmonic analysis etc...?

If this type of intellectual task is too difficult to study by far, then for a boiled-down version, can a machine learning system process a compact, well-formatted notes (to largely reduce natural language processing part) about for instance real analysis/algebraic topology, and then to ask it to solve some exercises ? Note that the focus and interest here are more about "exploring" new possible conjectures via current(or possible near future) state-of-the-art machine learning techniques, instead of proof techniques and logic-based knowledge representation which actually already are concerned and many works done in classical AI and automated theorem proving.

So, are there some knowing published research out there, particularly by generative model in machine learning techniques.

If there are not even known papers yet, then fruitful and interesting proposals and discussions are also highly welcomed.

As a probably not so good example I would like to propose, can a machine learning system "re-discover" Cauchy-Schwarz inequality if we "teach" it some basic operations, axioms and certain level of definitions, lemmas etc, with either provided or generated examples(numerical/theoretical) ? e.g. if artificial neural networks are used as training tools, what might be useful features in order eventually output a Cauchy-Schwarz inequality in final layer.

$\endgroup$
8
$\begingroup$

One example that is close to, if not exactly of this type, is Veit Elser's demonstration that machine learning techniques can learn how to do fast matrix multiplication from examples of matrix products. As far as I know this method has so far just reproduced some known results as opposed to providing new ones. I say the example is not quite of the type requested because the system here benefits from the fact that this is a very structured problem in a specific domain; it is not going after a wide range of mathematics.

$\endgroup$
7
$\begingroup$

Check the answers in Interesting conjectures “discovered” by computers and proved by humans?.

An example in graph theory is the software graffiti which outputs conjectures.

$\endgroup$
7
$\begingroup$

A pre-print by Li-An Yang, Jui-Bin Liu, Chao-Hong Chen and Ying-ping Chen was submitted to arXiv last month (24 Feb) giving some preliminary results of an ad-hoc evolutionary algorithm used to prove some simple theorems within the Coq proof assistant: Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants

The paper also discuss some possible future work within this context and the code used was released as open-source at GitHub.

Update (04/26/2019):

Found today in a NewScientist article about the Deepmath project, a Google project seeking to improve automated theorem proving using deep learning and other machine learning techniques. In particular, they made a software named DeepHOL that is a deep reinforcement learning driven automated theorem prover (1).

(1): Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.