Minerva: Solving Quantitative Reasoning Problems with Language Models | Hacker News Reader

Minerva: Solving Quantitative Reasoning Problems with Language Models

ai.googleblog.com

98 pointsguyga36 comments

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.

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

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

Looks like Polish tests were included into training dataset.

From the paper, the Polish tests are from May 2022, and the training dataset was from January 2022, so this is unlikely.

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.

Students have the same advantage. What's your point?

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.

You can't "memorize" from previous tests, otherwise that's exactly what students would do.

LLM is much more capable in memorizing than human. Human (by my hypothesis) still better in logical reasoning.

You are mistaken, memorisation is trivial, what is hard is to recognise which of the memories to reuse later, and how to adapt it.

I would love to learn why do you think so.

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.

If you can create a system that presents a limited number of novel solutions a human could double check each one.

('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.')

That's one of the future direction we're pursuing! We hope to utilize the power of autoformalization (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!

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?

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?

Yes, reward space is sparse, they need to train on human demonstrations (same with the recent Minecraft model) to bootstrap more meaningful exploration.

The AlphaZero for LLMs+search is GPT-f, which most recently did https://openai.com/blog/formal-math/

Weird. There are some impressive examples and then it fails spectacularly e.g. by simply removing all square root signs at one step.

Given that type of failure I must conclude the model didnt learn essential fundamentals of math reasoning (i guess it was clear from the start it is not built to do so).

I would like to have an interactive demo where I can type tasks for it.

> then it fails spectacularly

Like a math professor never forgot to carry a sign or programmers don't make off by one errors. It's quite endearing to see it make human like errors.

One of the errors the authors presented was

> f(x) = f(y) + f(z) => x = y + z

where f(.) denotes square root.

This is very different in nature from flipping a sign or a one-off error.

I mean that’s pretty close to a mistake that students make so frequently it has a Wikipedia page https://en.m.wikipedia.org/wiki/Freshman%27s_dream

lol. it's a funny name but I find it hard to believe it's actually a common mistake. my experience is that squaring and multiplying polynomials is done so often in high school that it's hard not to learn this is not true (i studied in an ordinary high school in russia, not any special one).

Me too, I studied it in Romania and it was very basic and well drilled. But plenty of students just blocked out math. I bet the Minerva model learned it on the internet, some bad training example could explain it.

What happens if you feed it the Riemann Hypothesis or the Collatz Conjecture?

It’s impressive that the model is clearly learning a lot of facts in training that it just memorizes—like the variance of the first m even numbers, and remarkable to me that these models can generate correct output with high probability when they have no actual understanding of mathematics. But perhaps that’s just an indication that my own ideas are wrong—to wit, maybe math just isn’t that hard (in the sense that the sequence of correct outputs to a given prompt are a highly constrained pattern built around successive substitutions in common templates, rather than searching for a needle in a practically-infinite haystack).

Pretty insane. I thought AI had a ways to go before it could solve problems like these. https://minerva-demo.github.io/#category=Algebra&index=1

So, I look at the internet for some questions, for example: https://minerva-demo.github.io/#category=Algebra&index=3

And here you go: https://books.google.com/books?id=QutS5unZDLYC&pg=PA126&lpg=...

So, they may have data leak in training data. I am wondering what would be model answer if they slightly change numbers.

They have this plot in the paper. See Figure 5. Average accuracy (averaged over problems) does not change.

The question listed in paper (they modified 20 out of thousands in MATH dataset) as example is very far in calculating complexity from what I quoted in my comment above.

Their question for your convenience:

At each basketball practice last week, Jenny made twice as many free throws as she made at the previous practice. At her fifth practice she made 48 free throws. How many free throws did she make at the first practice?

> accuracy (averaged over problems

My understanding is that it is average over 64 solution attempts (model generated 64 possible answers, and they calculated average accuracy of this answers), which is not target metric of benchmark.

Additionally, accuracy degradation is clearly visible on graphs, first graph has 4 problems out of 20 bellow the line, last graph has 14 problems bellow the line.

The model gets a question and outputs one answer, so this is the target benchmark. to do this, 64 samples are generated and we pick the most common answer, ie we use majority voting or self-consistency.

Target benchmark accuracy: accuracy of "most common answer".

Accuracy in Figure 5: average accuracy over 64 answers.

This is mathematically different metrics.

Somebody needs to figure out how to merge language models with theorem proving. In fact, that might be the first step to AGI.

That’s the topic of my thesis ! Here’s some work by open ai doing exactly that ! :) https://arxiv.org/abs/2202.01344

Reply on news.ycombinator.com