Discovering mathematical concepts through a multi-agent system

TL;DR

A new multi-agent model for computational mathematical discovery based on Euler's conjecture for polyhedra, which shows that the optimisation of the right combination of local processes can lead to surprisingly well-aligned notions of mathematical interestingness.

Abstract

Mathematical concepts emerge through an interplay of processes, including experimentation, efforts at proof, and counterexamples. In this paper, we present a new multi-agent model for computational mathematical discovery based on this observation. Our system, conceived with research in mind, poses its own conjectures and then attempts to prove them, making decisions informed by this feedback and an evolving data distribution. Inspired by the history of Euler's conjecture for polyhedra and an open challenge in the literature, we benchmark with the task of autonomously recovering the concept of homology from polyhedral data and knowledge of linear algebra. Our system completes this learning problem. Most importantly, the experiments are ablations, statistically testing the value of the complete dynamic and controlling for experimental setup. They support our main claim: that the optimisation of the right combination of local processes can lead to surprisingly well-aligned notions of mathematical interestingness.

Figures (6)

• Figure 1: The picture-frame (introduced by L'Huilier) is topologically the same as the torus, but not the icosahedron, which has no hole. In modern language, the symbols denote homeomorphisms, a precise notion of topological equivalence.
• Figure 2: Summary of the Conjecturing agent. At each timestep, it picks its priors and chooses the number of features, then runs the first round of regression. This produces atomic formulae over patches of data, each governed by $\lambda_i$. In the second round of regression, these are combined by the scaffolder into a global statement. The variables and operators used are tailored to the application; a successful instance of learning is shown in the box on the right, with the heights and widths corresponding to the dimensions of vector spaces. Once in the environment, the statement gets translated into Lean. Quantifiers are implicitly added during the translation; the regression only has the variables and propositional symbols in its vocabulary. The Conjecturing agent cannot access the Lean statement. For further details, see §Appendix \ref{['app:LeanTranslation']}.
• Figure 3: Summary of the full system. The Conjecturing agent produces statements until one crosses the provability threshold whilst passing simple checks, at which point the episode terminates and it receives its greatest reward. At intermediate steps, it receives a smaller reward for longer statements, measured in terms of tree size. The Skeptical agent modifies the data distribution. The colour blue is used for the agents and the flow of information, whilst green is used for elements that are in the environment. Orange represents components that should be tailored to an application. Although the game is competitive, it is not zero-sum.
• Figure 4: These tables show the pairwise performance ratios, $i/j$, for models in row i and column j on the dataset $\mathcal{D}_0$, with respect to all metrics. Again, we use cluster bootstrap (10,000 resamples). We compute a one-sided effective $\sigma$ by mapping the bootstrapped probability that model $i$ outperforms model $j$ to the corresponding normal distribution. This gives an interpretable measure of the confidence in the direction of the effect, standard practice when the underlying statistic is not Gaussian cowanAsymptoticFormulaeLikelihoodbased2011. Entries in bold mean that the ratio is empirically significant (i.e. $\geq2\sigma$), but in many cases the effect is stronger. $\geq5\sigma$ ($\leq5\sigma$ resp.) means that the effect is at least $5\sigma$ under our resampling resolution.
• Figure 5: Table (a) gives the performance ratios of $\mathcal{M}_0$ vs $\mathcal{M}_1$ on dataset $\mathcal{D}_2$. The tables in (b) - (e) again show the pairwise performance ratios, $i/j$ for row i and column j, but we are now varying the data and premises rather than the model, and each entry uses the full system (i.e. $\mathop{\mathrm{\bm{\mathtt{CA}}}}\nolimits+\mathop{\mathrm{\bm{\mathtt{SA}}}}\nolimits+$Provability). These ablations capture the changing nature of the learning problem as more diverse triangulations are added. We again use cluster bootstrap for sampling (with 10,000 resamples) and compute a one-sided effective $\sigma$, with $\sigma \geq2$ being empirically significant. Finally, $\geq5\sigma$ ($\leq5\sigma$ resp.) still indicates that the effect is at least $5\sigma$ under our resampling resolution.

Theorems & Definitions (5)

• Proposition 1.1
• Proposition 1.2
• Definition 1.3
• Definition 1.4
• Theorem 1.5