All of cohenmacaulay's Comments + Replies

  • Thanks for the pointer to davinci-003! I am certainly not interested in ChatGPT specifically, it just happens to be the case that ChatGPT is the easiest to pop open up and start using for a non-expert (like myself). It was fun enough to tinker with, so I look forward to checking out davinci.
     
  • I had not heard of GPT-f - appreciate the link to the paper! I've seen some lean demonstrations, and they were pretty cool. It did well with some very elementary topology problems (reasoning around the definition of "continuous"), and struggled with analysis in in
... (read more)
gwern*193
  • Yeah, that's the problem with ChatGPT: it's so easy to use, and so good within a niche, we're right back to 2020 where everyone is trying the first thing that comes to mind and declaring that GPT is busted if it doesn't (won't) do it. Heck, ChatGPT doesn't even let you set the temperature! (This is on top of the hidden prompt, RLHF, unknown history mechanism, and what seems to be at least 1 additional layer of filter, like the string-matching that the DALL-E 2 service uses to censor and decide when to apply 'diversity prompt'.) 'Deep learning is hitting

... (read more)

I think I largely agree with this, but I think it's also pretty hard to put to practice in training an AI proof system.

Fermat's theorem is actually a great example. Imagine my goal is to "align" a mathematician to solve FLT. Imagine a bizarre counterfactual where we have access to advanced AI models and computational power but, for some reason, we don't have algebraic number theory or algebraic geometry -- they were just never invented for some reason. If you want something less far-fetched: imagine the abc conjecture today if you're of a camp that believe... (read more)

I think what I mean by "promising at math" is that I would assign a reasonably confident belief that a scaled up model with the same basic architecture as this one, with maybe a more mathematical training set, would be able to accomplish tasks that a mathematician might find helpful to a nonzero degree. For example, I could imagine a variant that is good at 'concept-linking,' better than google scholar at least, where you ask it something like "What are some ideas similar to valuations rings that people have explored?" or "Where do Gorenstein rings come up... (read more)

3gjm
An idea that feels promising to me for proving things using LLMs, though I don't know whether it actually is, is something along the following lines. * Completely rigorous automated proof-checking system along the lines of Lean. * Language-model-y translator from informal mathematical statements plus purely-formalized context into formalized equivalents of those statements. * Language-model-y system generating highly-unreliable proposals for the next thing to try in a proof. * (If necessary given the foregoing:) Traditional good-old-fashioned-AI-type search algorithm attempting to build proofs using LLM 2 to generate candidate steps, using LLM 1 to translate them into formalism, and using Lean-or-whatever to see if the candidate step is easy to prove from what's been proved already. This is not so very different from what human mathematicians do, and it doesn't seem super-improbable that a modest amount of improvement to the models might be sufficient to make it work pretty well. [EDITED to add:] One thing I don't like about this sort of separate-models-and-duct-tape approach is the lack of integration: the language model doesn't really know what the proving-bits are thinking. I don't know how much difference this actually matters, but it feels a bit iffy.

Thanks for the link, this is great!

If anyone knows where to find an equivalent concept, definitely let me know! It's hard to prove that a concept has not been investigated before, so I'll just give my reasoning on why I think it's unlikely:

  1. I believe that the name "-cohesive" is untethered to the literature, even if the underlying concept exists, since it was specifically told to change the name to something new.
  2. The original name, "-smooth," appears in number theory, but the number theory concept is genuinely unrelated. The word "smooth" is heavily overloaded in algebra, but generally poin
... (read more)

Here is an additional perspective, if it's helpful. Suppose you live in some measure space X, perhaps  for concreteness. For any  can make sense of a space  of functions  for which the integral  is defined (this technicality can be ignored at a first pass), and we use the norm . Of course,  and  are options, and when X is a finite set, these norms give the sum of absolute values as the norm, and the square root of the sum of squares of ... (read more)