| |
| ▲ | lionkor 4 hours ago | parent | next [-] | | They're solving them in a way that isn't particularly interesting because it's near impossible to read and understand, and follow, what the LLM did. It's this way not because it's so smart, but because it's so stupid and still reached the goal by pure force and effort. | | |
| ▲ | QuesnayJr 2 hours ago | parent | next [-] | | I don't know how to communicate this, but what you are saying is almost entirely wrong. People can follow what they did. The documents OpenAi produced in their big drop are hard to read because they are poorly written in weird ways, not because they are beyond human intelligence. They didn't brute force in the normal sense. AI doesn't get tired, so it can try 1000 promising ideas, but it's like 1000 Ph.D.-level mathematicians trying different ideas, not 1000 calculators trying all combinations. The biggest results -- quasi-Riemann, no Siegel zeros, and Unique Games Conjecture -- have already been digested by experts. No Siegel zeros in particular already has like five different write-ups, and Tao has written a exposition on his blog. | |
| ▲ | JPLeRouzic 4 hours ago | parent | prev [-] | | I am sorry but your argument looks to contradict itself: They solve hard mathematical problems because they are stupid and use brute force? Then why a human skilled in mathematics guided them for many turns in their conversation? If they were really stupid, a Prolog program, a genetic algorithm or a SAT solver would be enough to reach the goal. Clearly it was not the case. | | |
| ▲ | suddenlybananas 3 hours ago | parent [-] | | Can't you kind of think of them as a genetic algorithm that has a very good hypothesis generator? Humans could, in principle, help guide that (already very impressive) hypothesis generator to make better guesses to find the proof more easily. |
|
| |
| ▲ | ccppurcell 4 hours ago | parent | prev | next [-] | | I think it does gel. You're right that the comment you're replying to is weakened by that fact. It gels because they solved about 700 problems out of 4000 attempts. And they threw a ton of resources at each. So "per problem" it's less than 1 in 5, "per token" it's probably not a great record. I mean it's astonishing that it's possible at all of course. But on average, even an expert with a top model will probably have an underwhelming response to the vast majority of prompts. | | |
| ▲ | internet_points 4 hours ago | parent [-] | | and I'm guessing it was with "tool calling" ie. they can write a bunch of Lean proofs and hit compile and basically brute-force a whole bunch of hypotheses quickly? Ie. the LLM itself isn't as "smart" as the combination of LLM, Lean, looping, search and vast gpu/cpu-time. | | |
| ▲ | ogogmad 2 hours ago | parent [-] | | In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. That last step sometimes takes them much longer than checking their proof without Lean, which is a problem humans have as well. What they're truly bad at, however, is explaining their proofs. Until they improve at that, we'll have to keep resorting to Lean to check whether they solved something correctly. I'm less sure about the following, however: I think that while current LLMs are bad at explaining their own proofs, some models are great for discussing older, human-written proofs. For this use case, from best to worst, Gemini > Claude > GPT-Astra >>>>>>>>>>>> GPT-Sol. |
|
| |
| ▲ | seba_dos1 4 hours ago | parent | prev [-] | | A relentless low IQ person with broad textbook knowledge and no need to sleep, I guess? | | |
| ▲ | Ar-Curunir 4 hours ago | parent [-] | | Look cmon, this is pure cope. The problems it has solved in TCS are far from trivial, with plenty of smart people making their careers in trying to solve them. The techniques these LLMs are using are non-trivial, and not just brute force. | | |
| ▲ | LtWorf 3 hours ago | parent [-] | | You mean techniques like using the prompt of mathematicians in the training set and brute force a solution before they publish? |
|
|
|
