Gabriel Poesia, David Broman, Nick Haber, Noah D. Goodman

This paper introduces an AI agent (MINIMO) that independently learns to perform formal mathematical reasoning using only axioms without relying on human-created proofs or data, as opposed to many others that need those for training.

MINIMO generates its own conjectures through constrained decoding and type-directed synthesis, ensuring that they are valid and well-formed, even when starting from an untrained model.

MINIMO uses a Transformer language model both for generating these conjectures and for theorem proving, utilizing the model as both a policy and value function to guide Monte Carlo Tree Search (MCTS) during proof searches.

The key innovation in my view is the self-improvement loop that mimics how human learn mathematics: asking ever harder questions and trying to prove the hardest ones currently attackable. MINIMO also uses hindsight relabelling, which captures both successful and failed proof attempts, adding a lot of successful proofs to the agent’s learning dynamics.

The authors present experiments across three domains: propositional logic, arithmetic, and group theory. MINIMO successfully bootstraps from the axioms in each of them, progressively tackling more complex problems. The agent is also capable of solving human-written theorems (e.g. from the Natural Numbers Game) that were not part of its training but are considered at least “interesting exercises” by real mathematicians.

A limitation of the current model is its lack of ability to accumulate learned theorems as reusable lemmas, which will hinder its scalability to deeper theories. In my view this is probably the biggest unsolved challenged to make this approach more interesting to tackle any real mathematical problems.

Ben Finkelshtein, Ismail Ilkan Ceylan, Michael M. Bronstein, Ron Levie

The Szemerédi regularity lemma is one of the fundamental results of extremal graph theory which has basically sparked a whole new area of research within mathematics.

In a very short hand way, it states that all dense, big enough graphs look the same and are only characterised by a partition of their vertices into independent sets and the edge-densities between those.  The Weak Regularity Lemma by Frieze and Kannan further extends this to an algorithmically feasible version to find those partitions.

This paper presents a new method for efficient learning on large, non-sparse graphs by approximating them with Intersecting Community Graphs (ICGs) – combinations of intersecting cliques. The authors prove the existence of the ICGs (a mathematical result probably interesting in its own), describe how to construct them efficiently, and then provide an algorithm to learn on the ICGs instead of on the graph directly.

Traditional Message Passing Neural Networks face computational challenges when dealing with large, dense graphs as their complexity is linear in the number of edges. This restricts scalability, especially in applications involving massive networks like social media platforms.

Training the newly proposed ICGs is mostly relevant for reasonably dense graphs (at least O(number of vertices^3/2) edges) and training them has complexity only linear in the number of vertices – a significant improvement.

The paper also presents some experimental results which shows from tasks like node classification and spatio-temporal data processing on real-world datasets that shows on-par performance of the ICGs while using fewer computational resources.