Llemma: An Open Language Model for Mathematics

I skimmed (ctrl-f) the paper and didn't see a comparison against gpt-4. Anybody knows how they'd compare?

Note that this still doesn't seem as good at solving proofs as some of the specialized prover models at formal theorem proving that aren't LLM-based. In particular, they show a 3% increase in proves solved over COPRA on the MiniF2F Lean dataset, but in COPRA's own paper they show that they prove about 18.5% fewer theorems than Proverbot9001 on the CompCert dataset (their pitch is that they are faster, but not better at proving, than other tools). Assuming COPRA isn't just way better at Lean than Coq (there should be some amount of difference, but given that it's the same algorithm run on a uniform interface over Coq and Lean it's unlikely to be large), Llemma should be proving 10-15% fewer proofs than Proverbot9001's algorithm. There's a bit of trickiness to trying to do this kind of cross-benchmark comparison, and COPRA picks a bit of a weird dataset to compare to Proverbot9001 on to save costs, but they also use a slightly older version which has worse results. So it probably still washes out to the best LLM-based provers being about 10-15% worse at proving theorems than the best specialized models.

EDIT: To be clear, that's 10-15% of the total theorems in a test set, not a relative 10-15% improvement. Given that solve rates for tools are in the 10-30% range, that's much more than a relative 10-15% improvement.

Not directly, but COPRA which they compare to (and show about 3% more theorems proved than) is based on GPT-4 using an agent framework. And in the COPRA paper, they compare to using GPT-4 directly as a one-shot, and find it can only get 10% of theorems in miniF2F, as opposed to 23% with their agent based approach. So if the eval line up correctly, we would see GPT-4 one-shot proving 10.6% of theorems in miniF2F, as opposed to Llemma-7b proving 26.23%, a pretty significant improvement. Still not as good as other specialized tools though, especially when you look at tools in other theorem proving languages (see my other comment for more detail about a cross-language comparison).

Hey, author here.

You can check out our evaluation library (https://github.com/wellecks/lm-evaluation-harness) for the exact benchmark implementations we used, including prompting.

In particular, the prompt that starts at line 27 in this file (https://github.com/wellecks/lm-evaluation-harness/blob/maste...) is quite good for high school/olympiad problems. We took this prompt from Google's Minerva paper.

Thanks! First thank you for all the work to develop a math LLM. Those prompts are helpful. I shrank the weights down to f16 to fit on my system from f32 using the procedure at ggerganov/llama.cpp, then tried some of those prompts. From line 34:

> Problem: > If $\det \mathbf{A} = 2$ and $\det \mathbf{B} = 12,$ then find $\det (\mathbf{A \mathbf{B}).$

> Solution: > We know that for a matrix \mathbf{M}, the determinant of its inverse is given by $\frac{1}{\det \mathbf{M}}.$ We also know that the determinant of a product of matrices is equal to the product of their respective determinants. Therefore, we have: \begin{align} \det (\mathbf{A}^{-1}\mathbf{B}) &= \frac{\det(\mathbf{AB})}{\det\mathbf{A}}\\ &= \frac{\det\mathbf{A}}{\det\mathbf{B}} \end{align} > Therefore, we have: > $\det(\mathbf{AB}) = 24

The f32 answer: > We have that $\det (\mathbf{A} \mathbf{B}) = (\det \mathbf{A})(\det \mathbf{B}) = (2)(12) = \boxed{24}.$ > Final Answer: The final answer is $24$. I hope it is correct.

Final answer is the same, which is encouraging for quantization to expand hardware options.