Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Llemma: An Open Language Model for Mathematics

arxiv.org

Post reply on HN
Print view View original

21–30 of 52 posts

Re: Llemma: An Open Language Model for Mathematics

#21

Post by mkl »

leedrake5 wrote: post #20
zazerbayev wrote: post #18

Earlier quoted context omitted.

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…

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

Is that supposed to be missing a "}" after the last "A"?

Re: Llemma: An Open Language Model for Mathematics

#22

Post by leedrake5 »

mkl wrote: post #21
leedrake5 wrote: post #20

Earlier quoted context omitted.

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…

> > Problem: > If $\det \mathbf{A} = 2$ and $\det \mathbf{B} = 12,$ then find $\det (\mathbf{A \mathbf{B}).$ Is that supposed to be missing a "}" after the last "A"?

Possible. I pasted the output, but tried to get some paragraph spacing in the output, possible I accidentally deleted a character.

Re: Llemma: An Open Language Model for Mathematics

#23

Post by Vetch »

aSanchezStern wrote: post #14

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…

I don't think the right way to think about its utility is as a replacement. I see it in terms of a NNUE for Stockfish type augmentation, where a small neural network supercharges search. Small neural network because no LLM, not even GPT4, is good enough that the time lost evaluating with them is gained in disproportionally less search done.

Other uses are: better autocomplete from comments for Coq and Lean VScode envs than generalist tools.

Translation from NL sketch to formal proof. This is different from autocomplete in that it should generate long attempts as an automated spitballer. Leave it running a a long time to see if it finds anything when you're stuck. This works for formal and informal proofs but the latter gets no feedback (this is imagining future tunes able to make better use of interactive prover feedback).

Translating formal proofs to natural language.

Combine it with RAG and have it pull in and summarize references from your personal paper collection and the internet. Particularly useful in place of search when you don't have the vocabulary for a concept. As a basis for non-code based autocomplete of mathematical work.

I see unbounded potential for this combination. And a natural setting where between cost of search and the symbolic prover doing the heavy lifting, it's one of those areas that naturally lends itself to specialist Open over API models.

Re: Llemma: An Open Language Model for Mathematics

#24

Post by infamouscow »

behnamoh wrote: post #7

Can we stop using catchy marketing names for things that are *supposed to be* scientific results? Choosing "llemma" (similar to Meta's "Llama") is just clout seeking.

You're totally right.

Every time someone wants to communicate something new the person(s) should take a crap and use OCR software to generate glyphs for a new alphabet used solely to communicate the new thing. That's the only way to possibly communicate ideas in a reasonable manner. Using existing things that have some notoriety can only be used to utterly confuse and distract people from new ideas. /s

Re: Llemma: An Open Language Model for Mathematics

#26

Post by aSanchezStern »

Vetch wrote: post #23
aSanchezStern wrote: post #14

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…

I don't think the right way to think about its utility is as a replacement. I see it in terms of a NNUE for Stockfish type augmentation, where a small neural network supercharges search. Small neural network because no LLM, not even GPT4, is good enough that the time lost evaluating with them is gained in disproportionally less search done. Other uses are: better autocomplete from comments for Coq and Lean VScode env…

Oh, I think you might misunderstand what I'm comparing it to. The other tools, like Proverbot9001, are exactly the NNUE scenario you describe, where a small neural network guides a search procedure to find proofs; they are more effective at finding formal proofs than Llemma. For other tasks, like non-formal proof generation, Llemma has novel results as far as I know; it's just in terms of producing formal proofs that it currently seems to lack as compared to the state of the art.

Re: Llemma: An Open Language Model for Mathematics

#28

Post by Syntonicles »

I wonder if I could use this to explore mathematics. I have been attempting to use existing LLMs, but results vary widely. I could imagine getting intuitions and insights about an equation, where the responses don't have to be watertight algebraic manipulations, but rather just deeply informed descriptions from several perspectives.
Post reply on HN