4
$\begingroup$

This is a rather soft question. Some people believe that GPT-style models can eventually solve very complex math problems if the models are large enough, but I'm skeptical about this. Suppose the GPT model is indeed large enough and can make very accurate predictions about the probabilities of the next token. Now we let it solve an extremely hard math problem, e.g. proving the Riemann Hypothesis. Proof length is not an obstacle, since the model can generate lots of tokens and therefore gains a lot of computational resources.

I think the most serious obstacle is how to generate the most likely proof, instead of the most likely next token. The bad thing is, that a proof might seem very plausible in the beginning, but may look more and more ridiculous as more tokens are generated. So, greedy decoding does not necessarily work; that's why people came up with beam search. But, beam search is also kind of greedy, and it also does not guarantee to produce the global optimal proof.

There may be extreme cases in which the optimal proof is among the top k+1 candidates but our beam size is k so it's not adopted. Therefore, the problem degenerates to a classic computational complexity problem: how on earth can we find the optimal generated sequence? This seems to be rather irrelevant to LLMs.

This problem is clearly in NP since its corresponding decision problem is: given a scheme to generate the next token probabilities, can we generate a sequence with length as most l and log-likelihood at least p? This decision problem can be verified in polynomial time by providing a satisfying sequence. I suspect this problem is NP-complete but I don't know how to prove it yet.

So, I conjecture that, unless P=NP, we can't use GPT-style LLMs to solve really hard math problems. Do you think so?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

I think that recently it has been a very interesting topic of conversation using LLMs for planning in the context of reasoning or for the case you mentioned for mathematical proving. Specially with the news of the supposed "Q*" that all the sensational news are very hyped about. Overall this is an opinion based on my experience and not a very factual thing based on the idea that these are currently open-ended research problems in the field and there could be a research paper in the future that proves me wrong.

I do not think that Natural Language or at least the methods we currently have are the best solution for solving sophisticated math reasoning or any type of active research problems. I do think that the models are very good intelligent algorithms able to solve math problems. I think that the field of mechanistic interpretability has reached very interesting results that contribute to the idea that LLMs are not just transformers that learn from the biases of the data and predict the next probable token based on previous data. They are able to run a model of the world and extract patterns they can generalize. I recommend the work of Neel Nanda on the topic. The question is then, if these models can be expanded more and more, can we upgrade the models in scaling, better data quality and diversity, to reach the so called "AGI"?

I think that better improvements in reasoning, especially in math, would depend less and less on prompting techniques and more on better fine-tuning of math problems or more broadly on better pretraining techniques. I think that ICL (In Context Learning) can only set you so far, and better models are going to come with better reasoning skills. It has been seen that models, even with very good few-shot learning, aren't capable of solving certain tasks. The concept of using planning like Tree of Thoughts and trying to optimize an answer by generating variants and selecting the best outcome is definitely a not very efficient way of handling the problem becuase of the computational implications and the intrincic limitations that these Models have in understanding.

In the case of LLMs proving a mathematical statement, it is very different than using Natural Language. First, because the language of mathematics must be completely logical, something that lacks in Natural Language. Inside each language, there are a lot of logical incongruencies that are innate in the way we speak. This is often called "sui generis", which means in Latin "in a class by itself", meaning that each language has its own set of rules that makes sense inside them. A mathematical analogy would be that each language has its own set of axioms that are different between them. Mathematics is just another language with its own rules. That's why only relying on the Language Model to analyze and try to create a proof can lead to various logical errors.

In fact, automatic theorem proving programs, like Lean, have already been explored and there is a lot of literature on the topic. There has been a lot of research in combining both Language Models with these programs using Retrieved Augmented Generation (RAG). Like Lean + GPT-4 + Embeddings.

In the context of Theoretical Complexity, I am not very familiar with the field, but am sure the problem is definitely a hard problem because we are not just considering proving an algorithm. We are considering if there is an algorithm that can solve an arbitrary number of proofs. It certainly sounds like an NP-Complete problem because of the complexity, but I also do not know how to prove that. The search problem is one thing, but using a Language Model makes it even a lot harder to determine complexity. I am very skeptical of Language Models for creating new knowledge because it lacks important features in the way humans create knowledge. For example, human interactions are very important. The way that humans can overspecialize in a certain topic for years and encapsulate knowledge for other humans to use for other purposes is a very interesting phenomenon that I think because of the problem of the scaling of language models, it is something we cannot do in a feasible way. We have a single, best performant Language model that is way better in almost all tasks than any of us, but not the best at anything. And there are also a lot of different discussions on whether or not these technologies could ever reach that type of performance in realizing these types of intelligent tasks.

In my opinion, the evolution of AI for scientific research is going to be more focused as helping tools for researchers rather than autonomous agents that can solve very complicated problems. Tools like AlphaFold, AlphaTensor, AlphaDev, GNome, and basically all the other research for scientific AI of DeepMind has more future in my understanding. We still do not have good models for imitating the scientific development that humans can do. Either way, I do not think we should not explore this type of idea because it is a very interesting problem with a lot of important implications for humanity.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ Thanks a lot for writing such a long answer. I do agree that the important thing to do now is to make LLMs a helper rather than a mathematician, but there are people working on using LLMs to do automatic reasoning, like Yuhuai Wu (a co-founder of xAI). I'm trying to say that beam search does not allow LLMs to undo what they've generated, but humans can backtrack when they've found the current way of solving problems is seemingly ineffective. My question focuses on the defect of beam search and impossibility to search over a complex space with greedy method $\endgroup$
    – Soha
    Commented Dec 10, 2023 at 7:07
  • 1
    $\begingroup$ @Soha - your problem is deper than that, Beam search ranking criteria has nothing to do with assessing correctness, usefulness or matching to reality of the results. It refines only the language. So the whole "what if the best result is in k+1" thing is a red herring. A good/correct answer could be in process of being formed in the current beam and then rejected because there is no mechanism to promote it, no part of the system recognises it, and if it were novel in some language-affecting way it could well score badly. $\endgroup$
    – Neil Slater
    Commented Dec 10, 2023 at 10:27
  • 1
    $\begingroup$ @Soha - The specific problem with automatic theorem proving using language models is that it doesn't guarantee 100% accuracy in predicting the steps of the proof (it can perform infinite illegal reasoning steps). However, this is not the case for systems like Lean, which use other ML methods to search in the possible action spaces. Your question would be more appropriate for these types of systems, not LLMs. Besides, it's probably almost impossible to answer that question. How could we optimize for solving the Riemann Hypothesis? It's even more challenging to establish its computational cost. $\endgroup$
    – Cesar Ruiz
    Commented Dec 11, 2023 at 0:28
  • $\begingroup$ @CesarRuiz I know that formal proof assistants like Lean or Coq are more suitable for searching for proofs. But I was asking about GPTs, because I just want to emphasize that LLMs are typically not good mathematicians and refute the rumors like "LLMs will replace mathematicians" etc. $\endgroup$
    – Soha
    Commented Dec 11, 2023 at 2:05
  • $\begingroup$ @NeilSlater I don't think beam search "merely" refines the language. If the token-generating model is big enough, the token that makes the "most sense" will tend to be given a high probability; the model has an attention mechanism and can look back at what it has already generated, so the most probable token should be also "mathematically correct". Ideally, if the model can tell the correct proof in the first place, then greedy decoding is enough. My argument focuses on the fact that a model can't "search" for a proof since beam search doesn't allow it to backtrack. $\endgroup$
    – Soha
    Commented Dec 11, 2023 at 2:19

You must log in to answer this question.