451–460 of 564 posts
Earlier quoted context omitted.
But for it to be 100% trustworthy, you'd have to express correctness criteria for those simple tasks as formal statements.
And most applied maths doesn't seem to worry about proofs much. They have techniques that either work pretty well or blow up.
Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. IMHO, the largest contributors to AlphaProof were the people behind Lean and Mathlib, who took the daunting task of formalizing the entirety of mathematics to themselves. This lack of formalizing in math papers was what killed any attempt at automation, because AI researcher had to wrestle wi…
Earlier quoted context omitted.
I don't know about that. A lot of the work that should have been very satisfying turned out to be boring as hell, if not toxic, while at the same time, some apparently mundane stuff turned out to be really exciting. I found the work environment to be more important than the subject when it comes to work satisfaction. If you are working on a world changing subject with a team of assholes, you are going to have a bad t…
Awesome work environment for one person can be not ideal for another. Pretty much all the top AI labs are both intensely competitive and collaborative. They consist of many former IMO and IOI medalists. They don't believe in remote work, either. Even if you work at Google DeepMind, you really need to be in London for this project.
Earlier quoted context omitted.
> However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually so…
They said the incorrectly formalized ones are usually easier, so I assume they just hire humans to solve them in the old way until the AI is smart enough to solve these easier problems.
An incorrectly formalized problem is a different problem and a solution to any formalized problem still useful for AI training because such solutions can be mechanically checked for correctness and this does not require the hire of humans. What requires humans is the initial formalization process since that is more a language translation task which requires nuance and judgment and is difficult to mechanically verify.
> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month fo…
It feels pretty disingenuous to claim silver-medal status when your machine played by significantly different rules. The article is light on details, but it says they wired it up to a theorem prover, presumably with feedback sent back to the AI model for re-evaluation. How many cycles of guess-and-check did it take over the course of three days to get the right answer? If the IMO contestants were allowed to use theor…
Earlier quoted context omitted.
> Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. The blog post indicates the opposite. The geometry problem in the IMO problem set was solved by AlphaGeometry 2, which is an LLM based on Google's Gemini. LLMs are considered relatively general systems. But the…
AlphaZero is more general than a Go and Chess AI, right? Isn't it a general self-play algorithm?
Earlier quoted context omitted.
Also AlphaProof had to search for 60 hours for one of the IMO problems it solved.
It’s going to be significantly faster very soon, we have seen how AlphaGo evolved into KataGo which is many magnitudes more compute efficient
I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.
Earlier quoted context omitted.
> A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually solve them? Formal proofs can be mechanically checked if it's correct or not. We just don't know what's the answer. Think it as an extremely rigorous type system that typically requires really long type annotations, like annotation itself is a comple…
Ah, thanks. That makes a lot of sense now.