Answers.Body: <p>In your described framework basically you're assuming the relevant abstracted concepts of any math question from a huge question-answer training set can be learned and combined together to fully acquire a compositional and intersected 'understanding', and then based on some statistical problem-solving relevance measure ranking for a specific question searched from a pre-trained LLM equipped with the knowledge of all mathematical categories, you can use the LLM or other DL model to craft a solution to the said specific question.</p>
  <p>However, you cannot simply count all relevant concepts of a given math question and search their intersected problem-solving concepts to generate a solution or proof like a NLP Q&amp;A task, since math solution or proof has to be exact and formally precise, even a little hallucination which seems ok in NLP Q&amp;A task would be detrimental for its theoretically binary performance. Now if you want to make DL models understand and reason about learned concepts symbolically like humans, then current DL models lack such general intelligence due to many problems such as dynamic conceptual object representation, segregation, composition, and relation responding through neural networks alone.</p>
  <p>Current SOTA Math Olympiad DL models such as AlphaProof use hybrid models including traditional symbolic AI models like constructive proof search or automated theorem provers (e.g., Coq, Lean). Generally they are trained with <a href="https://arxiv.org/abs/2202.01344" rel="nofollow noreferrer">curriculum learning</a> framework.</p>
  <blockquote>
  <p>We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.</p>
  </blockquote>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2024-12-04T07:27:18.097Z
Answers.LastActivityDate: 2024-12-04T07:27:18.097Z
Answers.UserDisplayName: cinch
Body: <p>When solving a complex mathematical Olympiad problem (or any one for that matter), there are 3 stages.</p>
  <p>The first is abstracting the concepts given in the question (this is an important process that can be trained). Say you are given a question about a recursively defined sequence that counts previous elements and asked to prove its eventually periodic. The abstracting might go like, count = combinatorics, eventually period = repetition, forced structure, recursion.</p>
  <p>Step 2, is determining how these abstracted concepts &quot;intersect&quot; / could be useful to solve the question. Here, you might ask, what combinatorial process could lead to forced repetitive structure in a recursive integer sequence? Pigeon hole principle stands out here for someone with experience. The AI could be trained to become efficient in this process of looking for ways the abstracted concepts combine or intersect to relate to the problem.</p>
  <p>Step 3, is crafting a solution to the problem via PHP.</p>
  <p>Essentially, a deep learning model, would be equipped with a language of general mathematical categories (like, combinatorics, number theory, geometry etc...) and then within those has the theorems like Fermats last theorem, and the properties of mathematical objects within those categories etc.. Then, if you train it to abstract the concepts in a given problem efficiently, it would be able to search its libraries millions of times per seconds for possible &quot;intersections&quot; (defined informally above) relating to a problem, and have statistical measures of how likely / inter-related they with respect to solving the particular question.</p>
  <p>I believe this has the potential to far outcompete a human, who can only think about &quot;intersections&quot; in a very slow fashion. Constructing the solution might not be an easy process for the AI, but I believe the process of abstracting and finding relationships to the problem could be of great utility for mathematical research, and offer new insights into a porblem.</p>
  
Tags: <machine-learning><math><computational-learning-theory>
Title: What are the limitations of this theoretical framework of a mathematical problem solving AI?
UserDisplayName: Frazer
ThreadText: # What are the limitations of this theoretical framework of a mathematical problem solving AI?
  
  (Asked by: username_0 on 2024-12-04)
  
  When solving a complex mathematical Olympiad problem (or any one for that matter), there are 3 stages.
  
  The first is abstracting the concepts given in the question (this is an important process that can be trained). Say you are given a question about a recursively defined sequence that counts previous elements and asked to prove its eventually periodic. The abstracting might go like, count = combinatorics, eventually period = repetition, forced structure, recursion.
  
  Step 2, is determining how these abstracted concepts "intersect" / could be useful to solve the question. Here, you might ask, what combinatorial process could lead to forced repetitive structure in a recursive integer sequence? Pigeon hole principle stands out here for someone with experience. The AI could be trained to become efficient in this process of looking for ways the abstracted concepts combine or intersect to relate to the problem.
  
  Step 3, is crafting a solution to the problem via PHP.
  
  Essentially, a deep learning model, would be equipped with a language of general mathematical categories (like, combinatorics, number theory, geometry etc...) and then within those has the theorems like Fermats last theorem, and the properties of mathematical objects within those categories etc.. Then, if you train it to abstract the concepts in a given problem efficiently, it would be able to search its libraries millions of times per seconds for possible "intersections" (defined informally above) relating to a problem, and have statistical measures of how likely / inter-related they with respect to solving the particular question.
  
  I believe this has the potential to far outcompete a human, who can only think about "intersections" in a very slow fashion. Constructing the solution might not be an easy process for the AI, but I believe the process of abstracting and finding relationships to the problem could be of great utility for mathematical research, and offer new insights into a porblem.
  
  **Tags:** machine-learning, math, computational-learning-theory
  
  ---
  
  ## 1 answers
  
  ### Answer by username_1 on 2024-12-04. Score: 1
  
  In your described framework basically you're assuming the relevant abstracted concepts of any math question from a huge question-answer training set can be learned and combined together to fully acquire a compositional and intersected 'understanding', and then based on some statistical problem-solving relevance measure ranking for a specific question searched from a pre-trained LLM equipped with the knowledge of all mathematical categories, you can use the LLM or other DL model to craft a solution to the said specific question.
  
  However, you cannot simply count all relevant concepts of a given math question and search their intersected problem-solving concepts to generate a solution or proof like a NLP Q&A task, since math solution or proof has to be exact and formally precise, even a little hallucination which seems ok in NLP Q&A task would be detrimental for its theoretically binary performance. Now if you want to make DL models understand and reason about learned concepts symbolically like humans, then current DL models lack such general intelligence due to many problems such as dynamic conceptual object representation, segregation, composition, and relation responding through neural networks alone.
  
  Current SOTA Math Olympiad DL models such as AlphaProof use hybrid models including traditional symbolic AI models like constructive proof search or automated theorem provers (e.g., Coq, Lean). Generally they are trained with [curriculum learning](https://arxiv.org/abs/2202.01344) framework.
  
  > We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.
  
  
  ---
  
  