Sign up or log in for free. It helps support the project and unlocks personalized paper recommendations and new AI tools. .
The current state of the art in artificial intelligence is impressive, especially in terms of mastery of language, but not so much in terms of mathematical reasoning. What could be missing? Can we learn something useful about that gap from how the brains of mathematicians go about their craft? This essay builds on the idea that current deep learning mostly succeeds at system 1 abilitiesâwhich correspond to our intuition and habitual behaviorsâbut still lacks something important regarding system 2 abilitiesâwhich include reasoning and robust uncertainty estimation. It takes an information-theoretical posture to ask questions about what constitutes an interesting mathematical statement, which could guide future work in crafting an AI mathematician. The focus is not on proving a given theorem but on discovering new and interesting <italic>conjectures</italic>. The central hypothesis is that a desirable body of theorems better summarizes the set of all provable statements, for example, by having a small description length while at the same time being close (in terms of number of derivation steps) to many provable statements.
This paper explores the potential of using machine learning, particularly deep learning, to create an AI mathematician capable of discovering new and interesting mathematical conjectures, not just proving existing theorems.
Significance: The paper addresses the gap between current AI's mastery of language and its limited mathematical reasoning abilities. It proposes a novel approach to mathematical discovery, shifting the focus from proving known theorems to finding new and interesting ones.
Key Innovations:
* Information-Theoretic Objective for Mathematical Discovery: The paper introduces the idea that a good set of theorems should compress the set of all provable statements. This means that the set should be small, but able to easily prove many other provable statements within a small number of derivation steps. This serves as a training objective for the AI.
* Proofs as Trajectories for Conjecture-Making Agents: The paper frames the process of finding a proof as an agent navigating a state-space, akin to reinforcement learning. Derivation steps become actions, and the AI learns to find paths (proofs) from existing knowledge to new theorems.
* Active Learning for Theorem Selection: The paper suggests using active learning to select the most informative theorems to add to the AI's knowledge base. This involves prioritizing theorems that are surprising (low probability given current knowledge) or uncertain.
Prior Ingredients Needed:
* Deep Learning and Generative Models: The paper builds on the successes of deep learning, particularly generative models like Large Language Models (LLMs), in creating realistic content.
* Information Theory: The paper leverages concepts from information theory, such as compression and description length, to define the objective function for mathematical discovery.
* Reinforcement Learning: The paper utilizes concepts from reinforcement learning to model the theorem-proving process as an agent navigating a state-space.
* Automated Theorem Proving (ATP): The paper acknowledges the existing work in automated theorem proving, particularly the use of proof tactics and formal verification systems like Coq and Lean. It aims to go beyond ATP by enabling the AI to generate new conjectures.
| Action | Title | Date | Authors |
|---|---|---|---|
| Out-of-distribution generalization via composition: A lens through induction heads in Transformers | 2025-02-07 | Jiajun Song Zhuoyan Xu Yiqiao Zhong |