3 ms·
> LLMs do not care about "elegance" the way human beings do, which is a big advantage. It's just a matter of time before you can post train it for elegance too
by HawtAds 2mo ago
> LLMs do not care about "elegance" the way human beings do, which is a big advantage.
It's just a matter of time before you can post train it for elegance too. Mathematical proofs in particular can be formally verified automatically which is a big advantage.
- jmalicki 2mo agoI've actually been involved in annotation projects doing RLHF to train LLMs to do exactly that. It's not a matter of time, it's already happening - it's just seemingly lower priority than "profitable" projects like post-training LLMs to replace white collar workers.
- tcp_handshaker 2mo ago>> post-training LLMs to replace white collar workers. And I look forward to a single example where this happened....
- pitched 2mo agoBefore LLMs, empire building was a very large incentive to hire. Teams tended to become larger than they needed to be so the boss feels good about their life choices. LLMs do not fix this problem, they make it worse. Instead of the team being oversized, they’re now way oversized. It is still in everyone’s best interest to look busy anyways and LLMs do help a lot with that.
- tcp_handshaker 2mo agoNo need to downvote. Just provide a counter example...
- jmalicki 2mo agoI'm not saying it happened, I am saying they are working hard towards that goal as a business priority, and spending a lot of money on it. Software engineers are first, but other fields like finance and radiology have huge targets on them too.
- ainch 2mo agoI'm not sure that elegance will be so easy to train for, the same way that writing skill has plateaued (or arguably declined) since earlier models. "Have you solved the problem" is verifiable, but questions of taste are harder to pin down.
- card_zero 2mo agoThis sounds kind of like unreadable code, though. So it's more than just taste.
- don_esteban 2mo agoYou can select for 'short proof', or 'elementary proof', or assign the 'cost' of the proof as a some combination of its length, the number and complexity of the new terms it needs to define, and so on. This might not help you with finding the proof, but once you have a machine that can produce several different proofs, you can select among them and incrementally polish the best one. I think this is the 'easier' part.
- ainch 2mo agoI'm sure you could select for shorter proofs, but then that might be confounding in its own way. I think it's a general problem for LLMs that taste is both subjective and hard to pin down to a single metric. There's a reason mathematicians talk about elegance rather than brevity. Sometimes a long geometric proof with a simple algebraic alternative is still elegant, or elucidates the problem in a new way.
- don_esteban 2mo agoWell, there are not that many proofs from 'The Book'. We are a bit ahead of time, currently I would settle for 'as easy to understand as possible' proof. Not a long, complicated, inpenetrable, mess, that Lean says is correct, but reading it provides no insight.
- travisgriggs 2mo agoWhy is it “just a matter of time”? Why do we assume and say this? The amount of times humanity has said this and time itself was not enough of an ingredient to achieve some anticipated outcome are legion. But we filter those out and go back to making more predictions based on the current linear derivative we’re observing.