I love the name, it's intuitive today and does not have any overloaded meanings or other confusers.
Do you say "L-L-Emma" or "L-Lemma"?
[dead]
Llemma: An Open Language Model for Mathematics
31–40 of 52 posts
Re: Llemma: An Open Language Model for Mathematics
#32Downloading this now to test it out - if anyone has prompts or tests they’d like to see let me know. I plan to run it with llama.cpp
can you please ask it if algebraic numbers are closed under addition? chatgpt4 just told me no, and then i asked it again and it said yes, and then it apologized profusely for saying no.
Re: Llemma: An Open Language Model for Mathematics
#33A missed opportunity: TheLemma.
Re: Llemma: An Open Language Model for Mathematics
#34Earlier quoted context omitted.
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…
Ah you're right. That makes sense. The autocomplete, informal proofs, translation or autoformalization, reference, search, feedback interactive assistant use-cases do seem promising though.
Re: Llemma: An Open Language Model for Mathematics
#35This seems to be as open as proprietary game engines as no mention of model license was present in the paper, code, model card. I wonder whether their incorrect and misleading use of "open" will be caught during peer review.
Maybe the authors also believe that Windows is open. Its source code is also publicly available after all.
Re: Llemma: An Open Language Model for Mathematics
#36Earlier quoted context omitted.
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…
When do you think we’ll have something that can do “verify this proof of the ABC conjecture” and it would check the proof?
Re: Llemma: An Open Language Model for Mathematics
#37This seems to be as open as proprietary game engines as no mention of model license was present in the paper, code, model card. I wonder whether their incorrect and misleading use of "open" will be caught during peer review. Maybe the authors also believe that Windows is open. Its source code is also publicly available after all.
The license is in the model card at the top - it's the same as the Llama 2 license.
Re: Llemma: An Open Language Model for Mathematics
#38Can 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.
It's a derivative of Code Llama, which is a derivative of Llama, so it's a good name.
And of course Llama is derived from LLM (Large LAnguage Model)