4 ms·

Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem. Besides, they also trained a Gemini m

by golol 2y ago

Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem. Besides, they also trained a Gemini model which formalizes natural language problems, and this is how they generated training data for AlphaProof. I would therefore expect that they could have also formalized the IMO problems with that model and just did it manually because the point is not to demonstrate formalizing but instead proof capabilities.

riku_iki 2y ago
> Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem maybe not, because you need to connect many complicated topics/terms/definitions together, and you don't have a way to reliably verify if formalized statement is correct. They built automatic formalization network in this case, but didn't trust it and formalized it manually.
pishpash 2y ago
Yet the facts at hand are the opposite of what you say. Reliable formalizer was the more difficult problem than solving formalized IMO problems, because they have not produced one.
- fngjdflmdflg 2y ago
  That does not necessarily follow from the facts at hand. For example they may have prioritized work on the proof solver itself as they may feel that that is the more important result. Alternatively if their goal is to build a proof solver then building the formalizer would be useless if they could not build the actual proof solver.
  - pishpash 2y ago
    A proof solver existed. They were improving the proof solver explicitly by making the formalizer a part of the training. Formalizer reliability is the key novelty. It turns out it was only reliable enough for training. So unless they made the problem statement at the outset that "we'll only make the formalizer strong enough to train but not use", I disagree with that assessment.
    - fngjdflmdflg 2y ago
      That's a good point. The formalizer was used to created the training data for the proof solver, so they likely worked on it more than if they just used it as a preprocessing step during inference. It is still possible that they worked on the formalizer until they got good results from it enough to create good training data, and then began training as soon as possible and did not spend too much time trying to improve the formalizer. Depending on how long the training was expected to take, perhaps that is a reasonable assumption. Although I think I agree more with your view now.
petters 2y ago
If they could have solved it, they would have. But I agree that language models will be able to do it.

by golol 2y ago

riku_iki 2y ago

> Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem maybe not, because you need to connect many complicated topics/terms/definitions together, and you don't have a way to reliably verify if formalized statement is correct. They built automatic formalization network in this case, but didn't trust it and formalized it manually.

pishpash 2y ago

Yet the facts at hand are the opposite of what you say. Reliable formalizer was the more difficult problem than solving formalized IMO problems, because they have not produced one.

fngjdflmdflg 2y ago
That does not necessarily follow from the facts at hand. For example they may have prioritized work on the proof solver itself as they may feel that that is the more important result. Alternatively if their goal is to build a proof solver then building the formalizer would be useless if they could not build the actual proof solver.
- pishpash 2y ago
  A proof solver existed. They were improving the proof solver explicitly by making the formalizer a part of the training. Formalizer reliability is the key novelty. It turns out it was only reliable enough for training. So unless they made the problem statement at the outset that "we'll only make the formalizer strong enough to train but not use", I disagree with that assessment.
  - fngjdflmdflg 2y ago
    That's a good point. The formalizer was used to created the training data for the proof solver, so they likely worked on it more than if they just used it as a preprocessing step during inference. It is still possible that they worked on the formalizer until they got good results from it enough to create good training data, and then began training as soon as possible and did not spend too much time trying to improve the formalizer. Depending on how long the training was expected to take, perhaps that is a reasonable assumption. Although I think I agree more with your view now.

petters 2y ago

If they could have solved it, they would have. But I agree that language models will be able to do it.