3 ms·
LLMs can't contribute good code to some of the good OSS math libraries, How is it even solving these problems?
by aadyachinubhai 24d ago
LLMs can't contribute good code to some of the good OSS math libraries, How is it even solving these problems?
- matrix2596 24d agosearch, verifiability and compute
- emil-lp 24d agoThat's a good question. It is able to contribute code, but maybe not good code. It's the same in math: it's able to solve problems, but not necessarily in a good way with a human readable code. Math papers are a lot like software: - theorems are like API - lemmata like internal/private function API - definitions are like types - the proofs are the implementation The proofs of ChatGPT are not necessarily readable or maintainable.
- linkgoron 24d agoYou don't need a GOOD proof, just A proof.
- feverzsj 24d agoNo one knows if it's actually LLM doing the heavy weight. It could be just human written brute force algorithm running on their massive computer cluster.
- vbarrielle 24d agoMath problems are often stated in a way that makes it possible to automatically verify if a solution is correct. Which means a loop that speculates an approach (LLM and/or prompts), implements it (LLM), then checks (automated) can work. You still need to have a very good LLM, and probably very good prompts with interesting research directions otherwise you can probably loop forever.
- recursivecaveat 24d agoNotably all the major announcements so far are counterexamples or formalizations of existing results to my knowledge. Not necessarily something you can just brute force, but areas with high return on elbow grease.