67
$\begingroup$

With no doubt everyone here has heard of deep learning, even if they don't know what it is or what it is good for. I myself am a former mathematician turned data scientist who is quite interested in deep learning and its applications to mathematics and symbolic reasoning. There has been a lot of progress recently, and while it is exciting to machine learning experts, the results so far are probably not useful for research mathematicians. My question is simple:

Are there areas of research math, that if one had access to a fully trained state-of-the-art machine learning model (like the ones I will describe below), it would make a positive impact in that field?

While math is mostly about proofs, there is also a need sometimes for computation, intuition, and exploration. These are the things that deep learning is particularly good at. Let me provide some examples:

Good intuition or guessing

Charton and Lample showed that Transformers, a now very standard type of neural network, are good as solving symbolic problems of the form $$ \mathit{expr}_1 \mapsto \mathit{expr}_2 $$ where $\mathit{expr}_1$ and $\mathit{expr}_2$ are both symbolic expressions, for example in their paper $\mathit{expr}_1$ was an expression to integrate and $\mathit{expr}_2$ was its integral. The model wasn't perfect. It got the right answer about 93-98% of the time and did best on the types of problems it was trained on. Also, integration is a 200 year old problem, so it is hard to outcompete a state-of-the-art CAS.

However, there are some things which make this interesting. Symbolic integration is important, difficult, and (somewhat) easy to check that the solution is correct by calculating the derivative (and checking symbolically that the derivative is equivalent to the starting integrand). Also it is an area where “intuition” and “experience” can definitely help, since a trained human integral solver can quickly guess at the right solution. Last it is (relatively) easy to compute an unlimited supply of training examples through differentiation. (This paper also uses other tricks as well to diversify the training set.)

Are there similar problems in cutting edge mathematics, possibly in algebra or combinatorics or logic where one would like to reverse a symbolic operation that is easy to compute in one direction but not the other?

Neural guided search

Some problems are just some sort of tree or graph search, such as solving a Rubik's cube. A neural network can, given a scrambled cube, suggest the next action toward solving it. A good neural network would be able to provide a heuristic for a tree or graph search and would prevent exponential blow-up compared to a naive brute-force search. Indeed, a paper in Nature demonstrated training a neural network to solve the Rubik's cube from scratch this way with no mathematical knowledge. Their neural network-guided tree search, once trained, can perfectly solve a scrambled cube. This is also similar to the idea behind AlphaGo and its variants, as well as the idea behind neural formal theorem proving—which is really exciting, but also not up to proving anything useful for research math.

Puzzle cubes and board games are not cutting edge math, but one could imagine more interesting domains where just like a Rubik's cube one has to manipulate one expression into another form through a series of simple actions, and the ability to do that reliably would be of great interest. (Note, the neural guided tree search I've described is still a search algorithm and much slower than a typical cube solving algorithm, but the emerging field of program synthesis could possibly one day soon learn from scratch a computer program which solves the Rubik's cube, as well as learn computer programs to solve more interesting math problems.)

Neural information retrieval

Suppose you have a database of mathematical objects (say, integer sequences, finite groups, elliptic curves, or homotopy groups as examples) and you want a user to be able to look up an object in this database. If that object is in the database, you would like the user to find it. If it is not, you would like the user to find similar objects. The catch is that "similar" is hard to define. Deep learning provides a good solution. Each object can be associated with an embedding, which is just a vector in, say, $\mathbb{R}^{128}$. The measure of similarity of two objects is just the inner product of their embeddings. Moreover, there are a number of techniques using self-supervised machine learning to construct these embeddings so that semantically similar objects have similar embeddings. This has already shown a lot of promise in formal theorem proving as premise selection where one wants to pick the most relevant theorems from a library of theorems to use in the proof of another theorem.

For example, I think such a neural database search could reasonable work for the OEIS, where one can use a neural network to perform various prediction tasks on an integer sequence. The inner layers of the trained network will compute a vector embedding for each sequence which can be used to search through the database for related sequences.

Geometric intuition

Neural networks are pretty good at image recognition and other image tasks (like segmentating an image into parts). Are there geometry tasks that it would be useful for a deep learning agent to perform, possibly in dimensions 4 or 5, where human geometric intuition starts to fail us since we can't see in those dimensions. (It would be hard to make, say a convolutional neural network work for a 4 dimensional image directly, but I could imagine representing a 3D surface embedded in 4D as say a point cloud of coordinates. This could possibly work well with Transformer neural networks.)

Build your own task

Neural networks are very flexible when it comes to the choice of input and output, as well as the architecture, so don’t let the specific examples above constrain your thinking too much. All you need are the following things:

  1. A type of mathematical object. One that you care about. It should be representable in some finite way (as a formula, an initial segment of a sequence, an image, a graph, a computer program, a movie, a list of properties).
  2. A task to perform on your operation. It can be well specified or fuzzy. It can be solvable, or (like integration) only partially solvable. It can be classifying your objects into finitely many buckets. It could be computing some other related object or property of the object. It could be finding the next element in a sequence. It could be coming up with a prediction or conjecture of some sort. It could be turning that object into a some 2D cartoon image even, just to think outside the box.
  3. Lots of training data. Either you need to be able to synthetically generate a lot of training examples as in the integration example above, or like OEIS have a large dataset of 10s of thousands or examples (more examples is always better). Clean data is preferred but neural networks handle messy data very well. Another “data free” solution is reinforcement learning like in the Rubik’s Cube example or AlphaGoZero, where the agent learns to explore the problem on its own (and generates data through that exploration).
  4. Patterns in the data, even if you can’t see what they are. Your task should be one where there are patterns which help the machine learning agent solve the problem. (For example, I’m not convinced that factoring large integers would be a good task.)
  5. Motivation. Why would this be useful to the field? What purpose would having this trained model have? Would it make it easier to conjecture facts, explore new areas of math, wrap ones head around a bunch of confusing formulas? Or do you have a way to turn a learned heuristic into a proof, such as with a search algorithm (as in the Rubik’s cube example above) or by checking the solution (as in the integration example above)?
$\endgroup$
20
  • 11
    $\begingroup$ I'm one of the authors of the lean-gptf paper. :) I'm very encouraged by the progress in machine learning on formal mathematics libraries, but I think it has a long way to go to help work-a-day mathematicians. On the other hand, I think there are probably more focused applications of deep learning to specific areas of mathematics that could have an impact right now, or relatively soon. $\endgroup$ – Jason Rute Apr 14 at 13:15
  • 3
    $\begingroup$ Does numerical solution of PDEs count? arxiv.org/abs/1904.07200 $\endgroup$ – Steve Huntsman Apr 14 at 16:33
  • 1
    $\begingroup$ ...or other algorithmic techniques like arxiv.org/abs/2005.01917? $\endgroup$ – Steve Huntsman Apr 14 at 17:05
  • 11
    $\begingroup$ "While math is mostly about proofs" Objection! :-) $\endgroup$ – Jochen Glueck Apr 14 at 22:41
  • 2
    $\begingroup$ Proofs are an important part of mathematics, but mathematics is not mostly about proofs, far from it. See, for example, terrytao.wordpress.com/career-advice/… $\endgroup$ – Hollis Williams Apr 16 at 15:25
31
$\begingroup$

In the context of algebraic geometry, neural networks have become useful tools in the study of Calabi-Yau manifolds. The computation of their topological invariants, metrics and volumes is of particular interest for applications in physics (string theory). Recent contributions include


For a more general overview, see Machine-Learning Mathematical Structures

We review, for a general audience, a variety of recent experiments on extracting structure from machine-learning mathematical data that have been compiled over the years. Focusing on supervised machine-learning on labeled data from different fields ranging from geometry to representation theory, from combinatorics to number theory, we present a comparative study of the accuracies on different problems. The paradigm should be useful for conjecture formulation, finding more efficient methods of computation, as well as probing into certain hierarchy of structures in mathematics.

$\endgroup$
6
  • $\begingroup$ Have these been used for any particularly interesting applications in physics? $\endgroup$ – Will Sawin Apr 14 at 15:54
  • $\begingroup$ This is a great example! I was expecting only to get ideas for future research (and that is still what I’m looking for) and not already published results, so this is very motivating. Could you possibly elaborate on the task being performed here? I don’t know much about this area, but it seems that in the second example the input to the NN is a matrix of integers representing a class of manifolds and the output is an integer hodge number from 1 to 24 of that class. Is that correct? What about the first example? $\endgroup$ – Jason Rute Apr 14 at 16:18
  • 1
    $\begingroup$ I found this description (page 11 and following) quite helpful. $\endgroup$ – Carlo Beenakker Apr 14 at 19:33
  • 1
    $\begingroup$ @CarloBeenakker This is really general. From that paper: "We emphasize again that the computing a topological invariant of any manifold (appropriately embedded as an algebraic variety) can be cast into the form of [a simple machine learning training problem]. We turned to CY because of their being readily available [data], similar experiments should be carried out for general problems in geometry." (Although I don't know enough about this area to say if it is surprising or useful.) $\endgroup$ – Jason Rute Apr 14 at 22:20
  • 1
    $\begingroup$ I added that overview paper to the answer box (since this is not (or not yet) community wiki I refrained from making a separate answer) $\endgroup$ – Carlo Beenakker Apr 15 at 6:05
23
$\begingroup$

I have some thoughts on a level of generality that is a bit higher than the question asks for:


One obstacle that faces applications of supervised machine learning to predict properties of mathematical objects is that in many fields of mathematics, such as number theory, we tend to expect that properties of the nice mathematical objects we study will either be

  • given by explicit formulas, or
  • quasirandom and hard to predict.

If this expectation is correct, then machine learning researchers are in a bit of a bind - they will either discover nothing or something trivial. Of course, mathematicians are fallible and our expectations are certainly not always correct.

This suggests one approach would be to use neural networks to search for properties that are unexpectedly easy to predict. This would be a somewhat thankless task as you would usually find nothing of interest, but when you do find something it would be a counterintuitive new phenomenon, which could hopefully by human analysis turned into a new formula for something.

It is crucial in this setting to have a good understanding of existing quasirandom models of the object in question, to know what trivial bounds your prediction is trying to beat. (This has been a pitfall for some attempts to apply machine learning, or just classical statistics, to pure mathematics.)


I am particularly excited about bringing techniques from puzzles and games to pure math, as in the neural guided search section of the question. This is because neural networks on games are some of the only networks to not just achieve human performance on tasks, and not just achieve superhuman performance, but to achieve superhuman performance by introducing new ideas which human practitioners were able to learn from and incorporate into their own strategies.

Since the goal of mathematics is the production of ideas, this is very heartening.

So we're looking for games where one must apply a sequence of moves, following some rules, to try to reach some result. (I don't know many examples of adversarial games in pure mathematics, so I'm describing 1-player games.)

Formal theorem proving is an example of this, already discussed in Steve Huntsman's answer.

I believe Kirby calculus is a game or puzzle of this sort, with the goal of showing two 3-manifolds or 4-manifolds are diffeomorphic by a finite series of combinatorial moves, that is used in current research (to test whether a newly constructed smooth structure on a 4-manifold is exotic or diffeomorphic to the standard structure). One challenge might be finding a good way to represent the diagrams that a network can work with efficiently.

$\endgroup$
17
  • 2
    $\begingroup$ I agree that Kirby calculus is a good candidate for machine learning, but it should be emphasized that it's only good for showing that two things are the same (often in unexpected ways). So you can show that e.g. a potential counterexample to the smooth 4d Poincare conjecture is actually standard, but you'll never be able to use it to show that it is a counterexample. $\endgroup$ – Andy Putman Apr 14 at 16:53
  • 1
    $\begingroup$ The reason I want to look for problems with a sequence of steps is because I really like the AlphaZero algorithm that combines machine learning with tree search, and think it's very powerful. This algorithm, at least in its current form, relies on a sequence of choices in time, where the algorithm considers multiple choices and evaluates their effects. $\endgroup$ – Will Sawin Apr 14 at 17:19
  • 3
    $\begingroup$ A possible example of an adversarial game in pure mathematics is an Ehrenfeucht–Fraïssé game. $\endgroup$ – Timothy Chow Apr 14 at 17:20
  • 2
    $\begingroup$ @WillSawin Does this capture your idea of a 1-player game? en.wikipedia.org/wiki/Reachability_problem $\endgroup$ – Dustin G. Mixon Apr 14 at 17:33
  • 1
    $\begingroup$ I see. It would be very surprising to me if a deep learning algorithm could rediscover the formula for the constant appearing in the Artin primitive root conjecture or Bateman-Horn conjecture without being told to look for infinite products over primes. Of course, since these formulas are already available it might be hard to convince anyone that a computer found them again even if one of them did. $\endgroup$ – KConrad Apr 14 at 18:06
21
$\begingroup$

In the category of guessing, there is the Ramanujan Machine. This project got off on the wrong foot with the research mathematics community because their initial announcement made overblown claims (such as claiming novelty for some conjectures/theorems that weren't new), but it is my belief that the general concept is sound. Along similar lines, perhaps it's time to revisit Graffiti with modern neural nets. In his paper On Conjectures of Graffiti (Ann. Discrete Math. 38 (1988), 113–118), Siemion Fajtlowicz described a computer program for generating conjectures about finite graphs. Most of its conjectures were either false, trivial, or known, but it did come up with some novel conjectures that were interesting enough for graph theorists to spend time proving them and publishing the proofs.

In the category of guided search, people have tried to use neural networks to improve the performance of SAT solvers; see for example the work on NeuroSAT. This seems like a promising area for further research.

$\endgroup$
4
  • $\begingroup$ Well, if most of the conjectures it come up with is false then I don’t really see the point. I can hire a monkey to type on my laptop all day and maybe after a few weeks he would come up with the statement of Riemann hypothesis. $\endgroup$ – Heavensfall Apr 15 at 7:23
  • 3
    $\begingroup$ I remember having heard about this project some time ago, and while I forgot much about it since that time, I am pretty sure it has nothing to do with deep learning. $\endgroup$ – Thomas Baruchel Apr 15 at 7:25
  • 3
    $\begingroup$ @Heavensfall If it took only a few weeks to come up with the Riemann hypothesis then I would gladly sift through the junk to find the gold. $\endgroup$ – Timothy Chow Apr 15 at 13:15
  • 3
    $\begingroup$ @ThomasBaruchel Yes, perhaps I should have been clearer that neither the Ramanujan Machine nor Graffiti uses deep learning. I was just picking two specific areas where computers have historically come up with interesting conjectures, and suggesting that possibly better algorithms would do even better. $\endgroup$ – Timothy Chow Apr 15 at 13:21
15
$\begingroup$

Some recent work on neural formal theorem proving (already mentioned in the question, but the examples give a sense of the state of the art):

$\endgroup$
13
  • 2
    $\begingroup$ Also see TacticToe (HOL4), Tactitian (Coq), CoqGym/ASTactic (Coq), HOList/DeepHOL (HOL Light), Holoprasm (Metamath), GPT-f (Metamath), Lean GPT-f (Lean) for more state of the art in this area. $\endgroup$ – Jason Rute Apr 14 at 13:21
  • 2
    $\begingroup$ And all of Josef Urban's work. $\endgroup$ – Jason Rute Apr 14 at 13:22
  • 3
    $\begingroup$ While I think such work provides a lot of motivation and encouragement, I don't think it is currently useful to research math and I don't think it will be for a while. However, I think there are probably more specific applications of machine learning to specific areas of mathematics that could be of value right now if we find them. $\endgroup$ – Jason Rute Apr 14 at 13:23
  • 1
    $\begingroup$ @JasonRute I think formalization of math that is close to research-level, like much of what Kevin Buzzard and his collaborators have been doing, is a valid and potentially important area of research math. As far as I know they don't use any neural methods, but at the rate machine learning approaches improve, isn't it reasonable to guess these things could be useful relatively soon? $\endgroup$ – Will Sawin Apr 14 at 15:46
  • 2
    $\begingroup$ @WillSawin, I haven't been clear. I greatly value Buzzard's work and his predecessors. I played a small role in Hale's formalization of the Kepler Conjecture, and a much larger role in lean-gptf, a recent neural theorem proving tactic for Lean (Kevin's prover of choice). What I want to emphasize here is that we don't have to solve automatic theorem proving (a REALLY hard problem) to use AI to solve outstanding math problems right now. I also don't think lean-gptf and such will currently solve new theorems or create new insights, but neural tools focused on specific areas of math will. $\endgroup$ – Jason Rute Apr 14 at 17:02
14
$\begingroup$

Neural networks might help to speed up computations in the monster group $\mathbb{M}$, which is the largest finite sporadic simple group. Such a network could be in some sense a (rather large) cousin of the neural network dealing with Rubik's cube mentioned by the OP.

Elements of $\mathbb{M}$ are usually represented as words of sparse matrices in $\mbox{GL}_n(\mathbb{F}_k)$, $196882 \leq n \leq 196884, k = 2,3$. There is an effective algorithm for checking equality of two such words, see [1]. Reduction of a word to a shorter word may take several minutes on a computer, see e.g. [2] for an overview. I'm currently working on the acceleration of the reduction of such words. I plan to exploit some geometric information contained in the images of certain vectors in $\mathbb{F}_k^n$. As far as I know, nobody has used this information before. (For experts: I focus on the images of vectors called 2A-axes). Here a neural network might be better at learning how to use this information than I am.

The mathematical benefits of such a project are:

  1. Regarding computations, the monster group is the most difficult finite simple group to deal with. If we can compute in the monster group then we can compute in all finite groups, provided we have enough information about that group and enough computer memory.

  2. We can probably finish the classification of the maximal subgroups of the monster group.

References

[1] R. Wilson. Computing in the monster. In Group, Combinatorics & Geometry, Durham 2001, 327–337. World Scientific Publishing, 2003.

[2] R. A. Wilson. The Monster and black-box groups.

$\endgroup$
11
$\begingroup$

This predates deep learning, but we should not forget that there has already been some progress in graph theory by recognizing patterns (OP: "patterns in the data") and forming conjectures.

  • Hansen, Pierre, and Gilles Caporossi. "AutoGraphiX: An automated system for finding conjectures in graph theory." Electronic Notes in Discrete Mathematics 5 (2000): 158-161. DOI.

"Up to now it [AutoGraphiX] has refuted 9 conjectures of Graffiti and suggested over 50 novel conjectures, 15 of which have been proved and none disproved."

Just posted (29Apr2021): A.Z. Wagner, "Constructions in combinatorics via neural networks." arXiv abs:

"We demonstrate how by using a reinforcement learning algorithm, the deep cross-entropy method, one can find explicit constructions and counterexamples to several open conjectures in extremal combinatorics and graph theory."

As requested, now a separate post.

$\endgroup$
4
  • 4
    $\begingroup$ And not just this type of thing, here's a sample from a student in my department: paperswithcode.com/author/matthias-fresacher Learning Erdős-Rényi Random Graphs via Edge Detecting Queries $\endgroup$ – David Roberts Apr 15 at 1:29
  • 1
    $\begingroup$ It is disconcerting that their first praise for this automated system is the way it refutes conjectures from a different automated system. $\endgroup$ – Matt F. Apr 19 at 9:16
  • 3
    $\begingroup$ @MattF. And now Wagner's paper refutes a conjecture by AutoGraphiX (which was previously, independently, less efficiently refuted by a human mathematician, the authors point out). It's the circle of life! I would actually defend this - if we have automatic conjecture generators and other systems that can automatically refute them, then by combining them we should obtain automatic generation of highly plausible conjectures. $\endgroup$ – Will Sawin May 1 at 21:35
  • 1
    $\begingroup$ The third example that you have just added does actually involve neural networks, and thus seems to be a better fit for the question than your other two. It seems worth posting a new answer, or editing your answer to focus more on it. $\endgroup$ – Will Sawin May 1 at 21:38
8
$\begingroup$

Adam Wagner has a new paper on arXiv (29 Apr 2021), "Constructions in combinatorics via neural networks," whose Abstract is:

"We demonstrate how by using a reinforcement learning algorithm, the deep cross-entropy method, one can find explicit constructions and counterexamples to several open conjectures in extremal combinatorics and graph theory. Amongst the conjectures we refute are a question of Brualdi and Cao about maximizing permanents of pattern avoiding matrices, and several problems related to the adjacency and distance eigenvalues of graphs."

Will Sawin commented here that "Wagner's paper refutes a conjecture by AutoGraphiX" (and deserved to be in an answer of its own).

Timothy Gowers discussed this on Twitter, summarizing that "the rough idea of the program is to design a suitable reward function, usually very simple, for how good an attempted counterexample is, and let the magic of reinforcement learning do the rest".

$\endgroup$
6
$\begingroup$

There has been some recent efforts in utilizing neural networks to approximate solutions of different types of PDEs. The key advantage of this approach is the possibility of tackling extremely high-dimensional problems, where traditional numerical approach involving discretization proves infeasible as the number of grid points scales exponentially with dimension.

Deep learning approaches sidestep the curse of dimensionality by converting the PDE problem into e.g. minimizing an energy functional https://arxiv.org/abs/1710.00211 or a stochastic optimal control problem https://arxiv.org/abs/2102.11379, then solve the related ERM problem via Monte Carlo sampling, whose convergence is independent of dimension.

$\endgroup$
1
  • $\begingroup$ Anil Ananthaswamy did an interesting article about this topic on Quanta Magazine: quantamagazine.org/… $\endgroup$ – Shamisen Apr 27 at 13:47
5
$\begingroup$

Full disclosure: This is a copy-and-paste of my answer to a question over on CrossValidated (stats Stack Exchange).

See the 2019 preprint Machine Learning meets Number Theory: The Data Science of Birch-Swinnerton-Dyer by Alessandretti, Baronchelli & He. Here is the Abstract:

Empirical analysis is often the first step towards the birth of a conjecture. This is the case of the Birch-Swinnerton-Dyer (BSD) Conjecture describing the rational points on an elliptic curve, one of the most celebrated unsolved problems in mathematics. Here we extend the original empirical approach, to the analysis of the Cremona database of quantities relevant to BSD, inspecting more than 2.5 million elliptic curves by means of the latest techniques in data science, machine-learning and topological data analysis.

Key quantities such as rank, Weierstrass coefficients, period, conductor, Tamagawa number, regulator and order of the Tate-Shafarevich group give rise to a high-dimensional point-cloud whose statistical properties we investigate. We reveal patterns and distributions in the rank versus Weierstrass coefficients, as well as the Beta distribution of the BSD ratio of the quantities. Via gradient boosted trees, machine learning is applied in finding inter-correlation amongst the various quantities. We anticipate that our approach will spark further research on the statistical properties of large datasets in Number Theory and more in general in pure Mathematics.

$\endgroup$
3
  • 8
    $\begingroup$ This is, in my opinion, a great example of machine learning / statistics work which wastes effort by not incorporating pre-existing mathematical knowledge and heuristics for the topic area. More generally, when working with any dataset, it's important to understand where the data comes from and whether it consists of a biased sample from a larger population. In this case, the elliptic curves in the LMFDB are, by construction, elliptic curves of small conductor (or smallish prime conductor, or highly smooth conductor). This heavily influences the statistics. $\endgroup$ – Will Sawin Apr 17 at 14:42
  • $\begingroup$ Whole bunch scholar.google.com/…. $\endgroup$ – 1.. Apr 17 at 23:11
  • 2
    $\begingroup$ @WillSawin It sounds like a great example of machine learning being thrown at things by people without pausing to understand the proper practice of statistics (Speaking as someone who has friends and colleagues in my department who do theoretical statistics including machine learning) $\endgroup$ – Yemon Choi Apr 19 at 0:32

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.