7 ms·
The computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in
by ocfnash 2y ago
The computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in each case.
- nnarek 2y agoformal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it is very interesting how they initially formalized problem without including answer in it
- golol 2y agoI would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like {Formal description of the set in question} = ? And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above. I doubt they would claim to solve the problem if they provided half of the answer.
- puttycat 2y ago> I doubt they would claim to solve the problem if they provided half of the answer. Stranger things have happened
- sebzim4500 2y agoTo be fair, that isn't half the answer it's like 99% of the answer. They clarified above that it provided the full answer though.
- JyB 2y agoThe deepmind team has a history of being misleading. The great StarCraft 2 strategist bot is still in mind.
- totoglazer 2y agoWhat’s the story with that bot? Always thought it was cool. Was that all smoke and mirrors?
- topato 2y agoI think maybe parent comment is referring to it essentially just employing a zerg rush but with the speed and reaction time of an AI? Not 100% sure... Unrelated, iirc the starcraft functionality was an early example of generalizing a pretrained NN, alphaGO, and showing that it could adapt to learn and defeat games across strategic domains, especially after it learned so much strategy from the most difficult, widely played, and most strategically-varied physical game available.
- chx 2y ago> I doubt they would claim to solve the problem if they provided half of the answer. This falls under extraordinary claims require extraordinary proof and we have seen nothing of the sort.
- riku_iki 2y agoits not clear if theorem is actual input formal definition, or formal definition was in different form.
- cygaril 2y agoCome up with many possible answers, formalize them all, and then try to prove or disprove each of them.
- Davidzheng 2y agoThis is probably partially what they did idk why it's downvoted lol
- Smaug123 2y ago(You're talking to one of the people who was part of the project, which is why I took @ocfnash's answer as authoritative: they did not cheat.)
- Xelynega 2y agoIf they're talking to the people who are part of the project I'd hope the answer would contain detail and not expect to be taken as authoritative.
- refulgentis 2y ago[flagged]
- pishpash 2y ago[flagged]
- refulgentis 2y agoThat wasn't very nice. Are you curious about anything? Happy to help. I'd proactively do it, but I don't want to guess at whats in your mind. My initial guess is you think I think that engaging with the public is an infinite loop. I don't!
- deleted 2y ago[deleted]
- pishpash 2y agoExactly, a problem and its answer are just different ways of describing the same object. Every step of a proof is a transformation/translation of the same object. It would be disingenuous to say that some heavy lifting isn't done in formalizing a problem but it seems that step is also performed by a machine: "We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty." I'm confused, is the formalization by Gemini or "manually"? Which is it?
- deleted 2y ago[deleted]
- Davidzheng 2y agoCan you elaborate on how it makes guesses like this? Does it do experiments before? Is it raw LLM? Is it feedback loop based on partial progress?
- Sharlin 2y ago"AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go."
- JKCalhoun 2y agoYeah I am not clear the degree to which this system and LLMs are related. Are they related? Or is AlphaProof a complete tangent to CHatGPT and its ilk?
- gowld 2y agoIt's not an English LLM (Large Language Model). It's a math Language Model. Not even sure it's a Large Language Model. (Maybe shares a foundational model with an English LLM; I don't know) It learns mathematical statements, and generates new mathematical statements, then uses search techniques to continue. Similar to Alpha Go's neural network, what makes it new and interesting is how the NN/LLM part makes smart guesses that drastically prune the search tree, before the brute-force search part. (This is also what humans do to solve math probrems. But humans are really, really slow at brute-force search, so we really almost entirely on the NN pattern-matching analogy-making part.)
- sebzim4500 2y agoMy reading of it is that it uses the same architecture as one of the Gemini models but does not share any weights with it. (i.e it's not just a finetune)
- nextos 2y ago
- freehorse 2y agoIt would make a lot of sense for the lean-code-formalisation of the problems done by the researchers fed to the AI to be provided. Not assuming bad intent in not providing them, but it would help understand better the results.