▲ 74 ▼ ‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop (www.theverge.com) submitted 2 days ago by Mustachius_Grumpius@thelemmy.club to c/technology@lemmy.world 41 comments fedilink hide all child comments
[–] AppleMango@lemmy.world 3 points 1 day ago (2 children) Hopefully this is sarcastic permalink fedilink source parent hideshow 2 child comments replies: [–] minorkeys@sh.itjust.works 2 points 1 day ago Lol yes it is permalink fedilink source parent [–] gole@lemmy.zip 11 points 1 day ago* It is sarcastic. But it is also what OpenAI tried. The reason they just drop these and say nothing is because these are unverified slop. OpenAI's method of verification is rewrite them as Lean proofs that can be verified by computers. Two things have happened so far: The Lean proof proved the slop wrong, easy, retract. The Lean proof, being generated by a LLM, is susceptible to hallucinations. For example the Navier Stokes problem Lean proof turned out to be slightly different than the original natural language proof, because the LLM tried to bend a condition to make the proof compile. But, in case nobody found any problem, OpenAI gets to claim credit for the discovery until someone can review and prove something's wrong. You can say these proofs are "Schrodinger's correct" permalink fedilink source parent
[–] gole@lemmy.zip 11 points 1 day ago* It is sarcastic. But it is also what OpenAI tried. The reason they just drop these and say nothing is because these are unverified slop. OpenAI's method of verification is rewrite them as Lean proofs that can be verified by computers. Two things have happened so far: The Lean proof proved the slop wrong, easy, retract. The Lean proof, being generated by a LLM, is susceptible to hallucinations. For example the Navier Stokes problem Lean proof turned out to be slightly different than the original natural language proof, because the LLM tried to bend a condition to make the proof compile. But, in case nobody found any problem, OpenAI gets to claim credit for the discovery until someone can review and prove something's wrong. You can say these proofs are "Schrodinger's correct" permalink fedilink source parent