5 ms·

Limitations Our approach to quantitative reasoning is not grounded in formal mathematics. Minerva parses questions and generates answers using a mix of natural

Limitations Our approach to quantitative reasoning is not grounded in formal mathematics. Minerva parses questions and generates answers using a mix of natural language and LaTeX mathematical expressions, with no explicit underlying mathematical structure. This approach has an important limitation, in that the model’s answers cannot be automatically verified. Even when the final answer is known and can be verified, the model can arrive at a correct final answer using incorrect reasoning steps, which cannot be automatically detected. This limitation is not present in formal methods for theorem proving (e.g., see Coq, Isabelle, HOL, Lean, Metamath, and Mizar). On the other hand, an advantage of the informal approach is that it can be applied to a highly diverse set of problems which may not lend themselves to formalization.

sharemywin 4y ago
Don't get me wrong it's pretty amazon what it can do but, I get the impression there's no confidence in the answers so I'm not really sure what to do with it. As with a lot of these systems how cherry picked were the answers
- nharada 4y ago
  If you can create a system that presents a limited number of novel solutions a human could double check each one.
- alphabetting 4y ago
  some interesting stuff from one of the authors. could only solve a third of MIT undergrad problems but did well on other tests. https://twitter.com/alewkowycz/status/1542559200051593219 https://twitter.com/alewkowycz/status/1542559200051593219
  - riku_iki 4y ago
    Looks like Polish tests were included into training dataset.
    - guyga 4y ago
      From the paper, the Polish tests are from May 2022, and the training dataset was from January 2022, so this is unlikely.
      - riku_iki 4y ago
        Unless new tests consist of many questions similar to questions from the previous years. I think this is huge issue with many current benchmarks. They need to create some handcrafted secret questions and never disclose them like it has been done with SquAD benchmark.
        rafaelero 4y ago
        Students have the same advantage. What's your point?
        riku_iki 4y ago
        First point is that LLM not necessary "solve", but potentially "memorize", while students can still be able to solve questions they didn't see. Second point is proposal how benchmarks can be improved.
        rafaelero 4y ago
        You can't "memorize" from previous tests, otherwise that's exactly what students would do.
        riku_iki 4y ago
        LLM is much more capable in memorizing than human. Human (by my hypothesis) still better in logical reasoning.
        visarga 4y ago
        You are mistaken, memorisation is trivial, what is hard is to recognise which of the memories to reuse later, and how to adapt it.
  - lumost 4y ago
    It’s worth recalling that a structurally similar problem presented somewhere else on the internet could enter the training set. A non-trivial portion of problems likely just have variable names replaced.
gwern 4y ago
('Sure, it can now read and write natural language with LaTeX math and do Python programming, solving many challenging problems from elite college STEM curricula autonomously, offline from large natural datasets, without any hand-engineering to teach it the specific algorithms, but you can't easily verify it, now can you? So overhyped.')
- yuhuai 4y ago
  That's one of the future direction we're pursuing! We hope to utilize the power of autoformalization (http://arxiv.org/abs/2205.12615 http://arxiv.org/abs/2205.12615) and provably verify the solution with formal systems. As I wrote in my tweet, in the long run, I am expecting a great synergy between a strong natural language math model and an autoformalizer to tackle challenging mathematical theorems!
  - visarga 4y ago
    Math and code can be verified, I think they can surpass human level eventually by an AlphaZero style approach. By the way, any intention to deploy this model as a math tutor?
- algo_trader 4y ago
  never rhe less, why arent we making even FASTER progress on formal domains? Where is the alphazero moment for LLMs + search? Either the reward space is truelly sparse. Or maybe the dataset of existing formulas is actually quite small?
  - visarga 4y ago
    Yes, reward space is sparse, they need to train on human demonstrations (same with the recent Minecraft model) to bootstrap more meaningful exploration.
  - gwern 4y ago
    The AlphaZero for LLMs+search is GPT-f, which most recently did https://openai.com/blog/formal-math/ https://openai.com/blog/formal-math/

sharemywin 4y ago

Don't get me wrong it's pretty amazon what it can do but, I get the impression there's no confidence in the answers so I'm not really sure what to do with it. As with a lot of these systems how cherry picked were the answers

nharada 4y ago
If you can create a system that presents a limited number of novel solutions a human could double check each one.
alphabetting 4y ago
some interesting stuff from one of the authors. could only solve a third of MIT undergrad problems but did well on other tests. https://twitter.com/alewkowycz/status/1542559200051593219 https://twitter.com/alewkowycz/status/1542559200051593219
- riku_iki 4y ago
  Looks like Polish tests were included into training dataset.
  - guyga 4y ago
    From the paper, the Polish tests are from May 2022, and the training dataset was from January 2022, so this is unlikely.
    - riku_iki 4y ago
      Unless new tests consist of many questions similar to questions from the previous years. I think this is huge issue with many current benchmarks. They need to create some handcrafted secret questions and never disclose them like it has been done with SquAD benchmark.
      - rafaelero 4y ago
        Students have the same advantage. What's your point?
        riku_iki 4y ago
        First point is that LLM not necessary "solve", but potentially "memorize", while students can still be able to solve questions they didn't see. Second point is proposal how benchmarks can be improved.
        rafaelero 4y ago
        You can't "memorize" from previous tests, otherwise that's exactly what students would do.
        riku_iki 4y ago
        LLM is much more capable in memorizing than human. Human (by my hypothesis) still better in logical reasoning.
        visarga 4y ago
        You are mistaken, memorisation is trivial, what is hard is to recognise which of the memories to reuse later, and how to adapt it.
- lumost 4y ago
  It’s worth recalling that a structurally similar problem presented somewhere else on the internet could enter the training set. A non-trivial portion of problems likely just have variable names replaced.

gwern 4y ago

('Sure, it can now read and write natural language with LaTeX math and do Python programming, solving many challenging problems from elite college STEM curricula autonomously, offline from large natural datasets, without any hand-engineering to teach it the specific algorithms, but you can't easily verify it, now can you? So overhyped.')

yuhuai 4y ago
That's one of the future direction we're pursuing! We hope to utilize the power of autoformalization (http://arxiv.org/abs/2205.12615 http://arxiv.org/abs/2205.12615) and provably verify the solution with formal systems. As I wrote in my tweet, in the long run, I am expecting a great synergy between a strong natural language math model and an autoformalizer to tackle challenging mathematical theorems!
- visarga 4y ago
  Math and code can be verified, I think they can surpass human level eventually by an AlphaZero style approach. By the way, any intention to deploy this model as a math tutor?
algo_trader 4y ago
never rhe less, why arent we making even FASTER progress on formal domains? Where is the alphazero moment for LLMs + search? Either the reward space is truelly sparse. Or maybe the dataset of existing formulas is actually quite small?
- visarga 4y ago
  Yes, reward space is sparse, they need to train on human demonstrations (same with the recent Minecraft model) to bootstrap more meaningful exploration.
- gwern 4y ago
  The AlphaZero for LLMs+search is GPT-f, which most recently did https://openai.com/blog/formal-math/ https://openai.com/blog/formal-math/