6 ms·
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
by beernet 2mo 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.
- dcsommer 2mo agoSure 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.
- senorrib 2mo agoYou clearly haven't used Claude to generate code or documentation.
- Someone 2mo ago> 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 2mo agoSo they can charge more per token and decrease the pressure on their infra.
- Someone 2mo agoEven if you specifically train the model on producing shorter answers, I would think producing good short answers would require more resources just as it does for humans (https://quoteinvestigator.com/2012/04/28/shorter-letter/ https://quoteinvestigator.com/2012/04/28/shorter-letter/: “If I Had More Time, I Would Have Written a Shorter Letter”) If so, charging per output token is the wrong incentive.
- yreg 2mo agoWhat billing system would you suggest?
- windexh8er 2mo ago"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.
- js8 2mo agoYou are kind of ignoring the Dennett's idea of different stances: https://en.wikipedia.org/wiki/Intentional_stance https://en.wikipedia.org/wiki/Intentional_stance You're looking at humans from intentional stance, but at LLMs from design stance, which would be a form of categorical error.
- subsistence234 2mo agoThe supposed "magicality" of human consciousness is hard to reconcile with evolution -- where on that long path from amoeba to homo sapiens did God (PBUH) implant our connections to the soul realm? Even evolution-deniers run into difficult-to-justify self-contradictions when trying to explain how the supposed supernatural part of our consciousness is both affecting the natural world and affected by the natural world, but not part of it.
- pdonis 2mo ago> 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?
- KPGv2 2mo agoI've driven back roads in Ireland. Super messy and chaotic. I was still able to use a map to get to my destination.
- _jayhack_ 2mo agoformal verifiability e.g. vi Lean
- AlexErrant 2mo agoEven Lean has bugs. > AI "Proves" Collatz Conjecture with Lean 4 Bug https://news.ycombinator.com/item?id=49101465 https://news.ycombinator.com/item?id=49101465
- drdrey 2mo agoof course it does, but it's still the best thing we have
- 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.
- 2mo ago
- js8 2mo agoI agree, counterexample to P!=NP would be great. I tried but it's a mess.
- layer8 2mo agoI’m pretty sure “counterexample” is the wrong word here.
- Good4boothee 2mo agoIsn'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?
- SetTheorist 2mo agoAIUI if you have an (polynomial-time) algorithm to reduce some NP-complete task to P then you have indeed shown that P=NP.
- Tyr42 2mo agoYou 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.
- layer8 2mo agoIf 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-completeness https://en.wikipedia.org/wiki/P_versus_NP_problem#NP-complet...
- subsistence234 2mo agoNP doesn't mean "we don't know a polynomial time algorithm for it", it means "a proposed answer can be verified as correct in polynomial time"
- kmeisthax 2mo agoKeep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN
- empath75 2mo agoThat 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.
- don_esteban 2mo agoThe 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 2mo agoThe beernet conjecture: all conjectures have both messy, ugly proofs, as well as a elegant clean proof lurking behind the scenes.
- don_esteban 2mo agoEh, some conjectures have counterexamples. This one might be one of those. ;-)
- xboxnolifes 2mo ago[dead]