[HawtAds]

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

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]

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]

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.

[ainch]

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

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

[card_zero]

This sounds kind of like unreadable code, though. So it's more than just taste.

[jmalicki]

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]

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

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

[pitched]

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]

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]

No need to downvote. Just provide a counter example...