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...
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...
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:
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 ...
- 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)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