Earlier quoted context omitted.
Well... assuming a human made no mistakes setting up that logic.
Of course. That falls under "understanding why the proof is a proof".
Now we only need to find that human that never makes mistakes and we're golden...
AI solves International Math Olympiad problems at silver medal level
481–490 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#482Earlier quoted context omitted.
And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.
Good. I want my AI to use all the advantages it has to reinvent the landscape of mathematics
Sure but note that's not "your AI". It's a closed-source, proprietary system by DeepMind who typically publish a result to reap the hype and then bury the system forever (see AlphaGo).
Re: AI solves International Math Olympiad problems at silver medal level
#483Earlier quoted context omitted.
The deepmind team has a history of being misleading. The great StarCraft 2 strategist bot is still in mind.
What’s the story with that bot? Always thought it was cool. Was that all smoke and mirrors?
I 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.
Re: AI solves International Math Olympiad problems at silver medal level
#484So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into formal mathematical language for our systems to understand. The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The do…
[deleted]
Re: AI solves International Math Olympiad problems at silver medal level
#485Earlier quoted context omitted.
When tackling IMO problems, the hard part is coming up with a good approach to the proof. Verifying your proof (and rejecting your false attempts) is much easier. You'll know which one to submit. (Source: I am a two-time IMO silver medalist.)
I don't see why we should take your word for it, as opposed to just asking AlphaProof to comment instead.
Well, he does have twice the amount of silver medals... And can speak the English language... Although, an AI attempting to speak with the human race entirely through an esoteric math-proofing language would be an interesting take on the whole, "humans make ET contact, interact through universal language.... pause for half of the movie, military hothead wanting to blow it out of the sky, until pretty lady mathematician runs into the oval office waving a sheet of paper... OF MATH!" trope....
But now, it's a race between you and I, to see who can write the screenplay first!
Re: AI solves International Math Olympiad problems at silver medal level
#486[flagged]
Re: AI solves International Math Olympiad problems at silver medal level
#487Earlier quoted context omitted.
Good. I want my AI to use all the advantages it has to reinvent the landscape of mathematics
Sure but note that's not "your AI". It's a closed-source, proprietary system by DeepMind who typically publish a result to reap the hype and then bury the system forever (see AlphaGo).
https://github.com/leela-zero/leela-zero
You can just use another implementation nowadays.
Re: AI solves International Math Olympiad problems at silver medal level
#488Earlier quoted context omitted.
And say they did use 10% of all GCP? Would it be less impressive? This is a result that was considered by experts to be far beyond the state of the art; it's absolutely ok if it's not very efficient yet. Also, for what it's worth, I'm pretty sure that I wouldn't have been able to solve it myself in three days, even if I had access to all of GCP, Azure and AWS (except if I could mine crypto to then pay actual IMO-leve…
Which experts said that? I don't think that's the case at all. The writing was already on the wall.
The writing was on the wall for the last year and a half (in fact I lost a bet to an IMO medalist about AI getting IMO gold by 8/2023) but three years ago this was unimaginable.
Re: AI solves International Math Olympiad problems at silver medal level
#489Earlier quoted context omitted.
These kind of LLMs are also very interesting for software engineering. It's just a matter of replacing Lean with something that is more oriented towards proving software properties. For example, write a formal specification of a function in Dafny on Liquid Haskell and get the LLM to produce code that is formally guaranteed to be correct. Logic-based + probability-based ML. All GOFAI ideas are still very useful.
You can also verify software like compilers in Lean: https://aws.amazon.com/blogs/opensource/lean-into-verified-s...
Sure, but Lean has very little support for software problems compared to Isabelle, Coq or Dafny right now.
Those 3 also have a lot of training data as well. Hoping Lean gets more support as it is very friendly.
As a basic learning resource focused on software engineering, there's [1]. But nothing more advanced I am aware of.
[1] The Hitchhiker's Guide to Logical Verification. https://cs.brown.edu/courses/cs1951x/static_files/main.pdf
Re: AI solves International Math Olympiad problems at silver medal level
#490Earlier quoted context omitted.
Only slightly more general. It only works for games that are zero-sum, deterministic, have no hidden information, and discrete game state and moves. Other examples include connect-4.
So finding Lean proofs can be conceptualized as a zero-sum game? Another basic requirement is that valid moves / inference steps and the winning condition can be efficiently verified using some non-AI algorithm. Otherwise there would not be a reward signal for the reinforcement learning algorithm. This is different from answering most natural language questions, where the answer can't be checked trivially.
Theorem proving can be formulated as a game, see e.g., https://plato.stanford.edu/entries/logic-games/ and interactive theorem provers can verify that a proof is correct (and related sub problems, such as that a lemma application is valid).
Conceptually, if you're trying to show a conjunction, then it's the other player's turn and they ask you for a proof of a particular case. If you're trying to show a disjunction then it's your turn and you're picking a case. "Forall" is a potentially infinite conjunction, "exists" is a potentially infinite disjunction.
In classical logic this collapses somewhat, but the point is that this is still a search problem of the same kind. If you want to feel this for yourself, try out some proofs in lean or coq. :)