| ▲ | beernet 8 hours ago |
| On the one-hand side, it's really impressive how LLMs drive mathematics forward, and this pace is only accelerating very quickly. At the same time, most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter). LLMs do not care about "elegance" the way human beings do, which is a big advantage. LLMs for mathematics is such a great fit on many levels. Can't wait for a significant breakthrough, prove P=NP and all hell breaks loose. |
|
| ▲ | HawtAds 5 hours ago | parent | next [-] |
| > 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 5 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 5 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 4 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. | | |
| ▲ | ainch 20 minutes ago | parent [-] | | 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. |
| |
| ▲ | card_zero 5 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 5 hours ago | parent [-] | | >> post-training LLMs to replace white collar workers. And I look forward to a single example where this happened.... | | |
| ▲ | pitched 5 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 3 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 3 hours ago | parent | prev [-] | | No need to downvote. Just provide a counter example... |
|
|
|
|
| ▲ | don_esteban 4 hours ago | parent | prev | next [-] |
| The mathematics is to a great extent about understanding of abstract structures.
As humans, we prefer simple structures/proofs (I suspect that is to a great extent because those are easier to understand), and as such find elegance in simplicity. In fact, the capability of the human brain to understand complex structures and proofs is rather limited. LLMs (hmm, I would prefer to use 'AI solver', as LLM is nowadays just a part of it) finding a complex proof can mean several things:
1) AI by its nature/construction does not have preference for simple stuff (it 'thinks' differently than human: a human will, in its search for a proof, start by exploring the 'simpler' parts of the proof space, and hence more likely find a 'simple' proof, while a AI might be more target oriented and descend deeply in depth-first-search manner to recursively solve sub-tasks, without much regard about the overall simplicity of the proof). This can be eventually solved, by subsequent 'polishing' passes, similarly as things work in human science. 2) there might simply not exist a simple/elegant proof of a given problem. The world is a complex beast. Its just our brains trying to find simple/elegant meaning/structure, even in places where there is none. |
|
| ▲ | scarmig an hour ago | parent | prev | next [-] |
| The beernet conjecture: all conjectures have both messy, ugly proofs, as well as a elegant clean proof lurking behind the scenes. |
|
| ▲ | pdonis 5 hours ago | parent | prev | next [-] |
| > most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter) How do you know they're correct if they're super messy and chaotic? |
| |
| ▲ | _jayhack_ 5 hours ago | parent | next [-] | | formal verifiability e.g. vi Lean | | | |
| ▲ | KPGv2 5 hours ago | parent | prev [-] | | I've driven back roads in Ireland. Super messy and chaotic. I was still able to use a map to get to my destination. |
|
|
| ▲ | js8 5 hours ago | parent | prev | next [-] |
| I agree, counterexample to P!=NP would be great. I tried but it's a mess. |
| |
| ▲ | layer8 5 hours ago | parent [-] | | I’m pretty sure “counterexample” is the wrong word here. | | |
| ▲ | Good4boothee 5 hours ago | parent | next [-] | | Isn't it a bit Catch 22 anyway? If someone finds a algorithm to reduce some NP task X to class P, then that just means X wasn't a true NP task and P!=NP is still undecided? | | |
| ▲ | layer8 5 hours ago | parent | next [-] | | If it’s an NP-complete [0] problem like SAT, as many NP problems are, then we are done, because all NP problems can be reduced to it (in polynomial time). [0] https://en.wikipedia.org/wiki/P_versus_NP_problem#NP-complet... | |
| ▲ | Tyr42 5 hours ago | parent | prev | next [-] | | You can prove something is in NP by providing a (polynomial) reduction from a known NP hard task, and vice versa. All the known NP problems (Knapsack, SAT, etc) are mutually reducable in this way, so solving one lets you solve the others. So if X was shown to be NP, then given a polynomial time solution to X, you can stack the polynomial time reduction from X to SAT to solve SAT in polynomial time too. | |
| ▲ | SetTheorist 5 hours ago | parent | prev [-] | | AIUI if you have an (polynomial-time) algorithm to reduce some NP-complete task to P then you have indeed shown that P=NP. |
| |
| ▲ | js8 5 hours ago | parent | prev [-] | | Why? A counterexample to P!=NP would be a polynomial algorithm for SAT. If it exists, it might be a constructible object. | | |
| ▲ | layer8 5 hours ago | parent [-] | | That’s not a counterexample to P != NP, it’s a proof that P = NP. You can’t prove that two sets are the same by counterexample. What you could do is disprove P = NP by counterexample, by showing that some problem is in NP but not in P. At best, a polynomial algorithm for SAT would be a counterexample to the claim that no NP-complete problem is in P. | | |
| ▲ | js8 3 hours ago | parent [-] | | Sorry, it seems like nitpicking to me. You haven't shown my usage of the word counterexample is wrong, at all. I think a proven counterexample to Q is always a proof of not Q. > You can’t prove that two sets are the same by counterexample. You can in this case. > What you could do is disprove P = NP by counterexample, by showing that some problem is in NP but not in P. You could argue that counterexample is defined in one direction only, by convention, as to which hypothesis is more believed. In that case, my usage would be more valid, because the general consensus is P!=NP. You could also argue that a counterexample should be some finite, constructible object. But that's actually also in favor of my usage - a difficult class is an infinite set, while an algorithm has a finite description. Also note that AI can still find the counterexample (the actual algorithm), without proving it is a counterexample. Again, my usage of the word counterexample favors that definition of what counterexample is. But honestly I think it would be more productive to spend this effort on thinking about actual counterexample to P!=NP. |
|
|
|
|
|
| ▲ | kmeisthax 4 hours ago | parent | prev | next [-] |
| Keep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN |
| |
| ▲ | empath75 3 hours ago | parent [-] | | That very much does not describe what happened. Someone found the bug and used it to disprove the Collatz conjecture as a demonstration of the bug. Nobody ever claimed it as an LLM proof. |
|
|
| ▲ | xboxnolifes an hour ago | parent | prev | next [-] |
| [dead] |
|
| ▲ | dcsommer 6 hours ago | parent | prev [-] |
| Sure they care about elegance, or at least brevity. Minimizing tokens out, or generally "token efficiency," is part of the objective function for these systems. It doesn't mean they are perfect at it though. |
| |
| ▲ | windexh8er 5 hours ago | parent | next [-] | | "They" don't "care" about anything. It is a stateless computational run across thousands of semiconductors. There is no objective this software has other than the computational function completing. To care would mean the model would have a level of discernment that goes along with sentience. | | | |
| ▲ | Someone 6 hours ago | parent | prev | next [-] | | > Minimizing tokens out, or generally "token efficiency," is part of the objective function for these systems. First time I heard that, and I doubt it. Don’t customers pay for output tokens? If so, why would a company specifically spend time training their LLM to generate fewer? | | |
| ▲ | yreg 6 hours ago | parent [-] | | So they can charge more per token and decrease the pressure on their infra. |
| |
| ▲ | senorrib 6 hours ago | parent | prev [-] | | You clearly haven't used Claude to generate code or documentation. | | |
| ▲ | nelox 6 hours ago | parent [-] | | "First rule in government spending: why build one when you can have two at twice the price" - S.R. Hadden | | |
| ▲ | KPGv2 5 hours ago | parent [-] | | Personally, I've found city roads to be more reliable than the private roads where I live. |
|
|
|
