Discussion about this post

User's avatar
Chase's avatar

Smart post and the research idea seems good to me. Only thought I had is that they're aiming for models that are generally pleasing to many audiences. Maybe reward training on proofs make their outputs in other domains less compelling?

Imagine the equivalent of this reasoning – "Assume for the sake of contradiction that P has n real roots. If n>k+1, we just need to consider a subset of these roots in the n=k+1 case to get our contradiction. Thus assume n=k+1." – being deployed when someone wants to draft an email or talk about an emotional problem. "Assume the user has already seen a psychologist with training in CBT" (Being facetious, but you get the higher level point).

I often think about how the labs talk about how the release models are fine-tuned for certain things and people should temper expectations. In particular, that OpenAI warned o3 the released model wasn't going to be as good at ARC-AGI as the preview model

Expand full comment
Kevin's avatar

I’ve been trying to get LLMs to write various sorts of proofs, and one thing that has helped is expanding the prompt with examples. This can get really big but for an agentic system like Claude Code you can say things like: “If you are thinking about a proof by induction, check file X to see examples.” Maybe what is happening is that it doesn’t really get this “reduction” idea, but with some examples it could.

In general, how many of these issues are we going to be able to afford to specially train a model to solve, and how many are we going to have to solve with cheaper techniques? (Measured by engineering time to develop, maybe not inference cost.) Prompt engineering is very cheap in developer time.

Expand full comment
3 more comments...

No posts