Having enough datapoints to see a trajectory, is your current model that they will improve a bit more but plateau at helping with your work in a predictable way, or, does it seem more likely to might end up dramatically accelerating it in some fashion?
A thing I feel a bit confused about reading this is, like, I have an impression that, say, “interpretability researchers” have been using AI in a way that at least seemed superficially productive to them, and while I think you’re doing different stuff than them my vague impression from a year ago was it wasn’t, like, crazy different when it came to the coding.
Once the auto formalization/proving gets much better than this, we will quickly become bottlenecked on knowing/deciding what is the most useful next thing to point it at....which would be quite the exciting and different bottleneck to have and it’s hard to predict what level of productivity that “plateau” looks like. (Assuming that there are also improvements to intelligibility of the proofs themselves, otherwise that too becomes a bottleneck of a similar sort because that’s where a lot of the useful insight lives.)
Yeah my question was a mix of “what’s your next bottleneck” and “what are you/John’s guesses about whether LLMs are fundamentally capable of handling the ‘knowing deciding what to point at’ part, or other stuff that’s more taste-laden.”
Having enough datapoints to see a trajectory, is your current model that they will improve a bit more but plateau at helping with your work in a predictable way, or, does it seem more likely to might end up dramatically accelerating it in some fashion?
A thing I feel a bit confused about reading this is, like, I have an impression that, say, “interpretability researchers” have been using AI in a way that at least seemed superficially productive to them, and while I think you’re doing different stuff than them my vague impression from a year ago was it wasn’t, like, crazy different when it came to the coding.
Once the auto formalization/proving gets much better than this, we will quickly become bottlenecked on knowing/deciding what is the most useful next thing to point it at....which would be quite the exciting and different bottleneck to have and it’s hard to predict what level of productivity that “plateau” looks like. (Assuming that there are also improvements to intelligibility of the proofs themselves, otherwise that too becomes a bottleneck of a similar sort because that’s where a lot of the useful insight lives.)
Yeah my question was a mix of “what’s your next bottleneck” and “what are you/John’s guesses about whether LLMs are fundamentally capable of handling the ‘knowing deciding what to point at’ part, or other stuff that’s more taste-laden.”