Learning Interestingness in Automated Mathematical Theory Formation

TL;DR

This paper introduces FERMAT, a reinforcement learning environment for automating mathematical theory discovery, and demonstrates an LLM-based evolutionary approach to score the interestingness of mathematical objects, advancing AI's capability in theory formation.

Contribution

The paper presents FERMAT, a novel RL environment for concept discovery and theorem proving, and develops an LLM-based evolutionary algorithm for scoring mathematical interestingness, improving over baseline methods.

Findings

LLM-based evolutionary algorithms outperform hard-coded baselines.

FERMAT enables modeling of concept discovery and theorem proving.

Effective measures of interestingness are synthesized through evolutionary strategies.

Abstract

We take two key steps in automating the open-ended discovery of new mathematical theories, a grand challenge in artificial intelligence. First, we introduce $\emph{FERMAT}$, a reinforcement learning (RL) environment that models concept discovery and theorem-proving using a set of symbolic actions, opening up a range of RL problems relevant to theory discovery. Second, we explore a specific problem through $\emph{FERMAT}$: automatically scoring the $\emph{interestingness}$ of mathematical objects. We investigate evolutionary algorithms for synthesizing nontrivial interestingness measures. In particular, we introduce an LLM-based evolutionary algorithm that features function abstraction, leading to notable improvements in discovering elementary number theory and finite fields over hard-coded baselines. We open-source the $\emph{FERMAT}$ environment at this URL(https://github.com/trishullab/Fermat).