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

▲

travisgriggs 4 hours ago | parent | next [-]

Why 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.

▲

ainch 4 hours ago | parent | prev | next [-]

I'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.

	▲	don_esteban 3 hours ago \| parent \| next [-]
		You 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.
	▲	card_zero 4 hours ago \| parent \| prev [-]
		This sounds kind of like unreadable code, though. So it's more than just taste.

▲

jmalicki 5 hours ago | parent | prev [-]

I'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 4 hours ago | parent [-]

>> post-training LLMs to replace white collar workers.

And I look forward to a single example where this happened....

	▲	pitched 4 hours ago \| parent \| next [-]
		Before 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.
	▲	jmalicki 2 hours ago \| parent \| prev \| next [-]
		I'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.
	▲	tcp_handshaker 2 hours ago \| parent \| prev [-]
		No need to downvote. Just provide a counter example...