Hi,
Why does this Lama have a red pyjama.
Oh, its a baby Lama. Its still in the cradle
and needs some training:
RedPajama-Data-v2
https://github.com/togethercomputer/RedPajama-Data
But then Andrej Karpathy recently showed
GPT-2 training on rented GPUs for less
than 100 USD in less then 2 hours.
So where do these grown up Lamas go.
Well Georgi Gerganov prefered C++/C
when he shouted Llama Llama Red Pyjama.
But you also find WebLLM, wrapping the
underlying C++/C GPU interface via the
W3C standard WebGPU / WGSL, with JavaScript:
In-Browser LLM Inference Engine
https://webllm.mlc.ai/
My experience with WebLLM 6 months
ago on an iPad Pro 2024, still a little early
stage performance and robustness.
But hey hardware of AI mobile iGPUs is
still evolving, and AI laptop, AI smartphones
and AI tablets, will soon feature Chinese
hardware such some new Kirin AI in 2027.
Bye
Mild Shock schrieb:
Hi,
Remember when first all local AI was Python
and PyTorch APIs. And then suddently people strated
using bare metal C/C++ Code. Here is the story:
How it started:
GPT-J or GPT-J-6B is an open-source large
language model (LLM) developed by EleutherAI
in 2021. As the name suggests, it is a
generative pre-trained transformer model
designed to produce human-like text that
continues from a prompt.
https://www.eleuther.ai/
How it was going [Georgi Gerganov]:
So a few days later comes out the LLaMA, I do
some calculations and I figure out rCLOkay, 65
billion parameters. You probably need about
40 gigs of RAM, with 4-bit quantization. So
this can run on a MacBook. Why not do it?rCY
Why I was able to do it so quickly - basically,
for all that I saw itrCOs pretty much GPT-J architecture
with some modifications, like some extra memorization
layers. ItrCOs minor changes. Basically, again, the
existing code for the GPT-J, I just simply
modified it there, it happened pretty quickly.
https://changelog.com/podcast/532
Georgi Gerganov, Bulgarian, now with Hugging
Face, ggml-cann also running on Chinese AI chips.
ggml Manifesto https://github.com/ggml-org/ggml
Bye
Hi,
Why is nobody mentioning Agda here. It has
beautiful dependent types, and tactics are
just programs. Poor Henk Barendregt, not
everybody likes dependent types it seems:
Are we stuck with Lean?
https://mathoverflow.net/q/513742/
Does Depependent types require proof objects,
which waste large amounts of memory. Well,
if you are not good in erasing them.
But is there a Red Pyjama for Proof Assistants,
the baby cradle where LLMs can learn proof
assistant lingua and strategies. It seems
yes, synthetic data corpuses to the rescue:
We address this gap by introducing SMAD
(Synthetic Multilanguage Autoformalization
Dataset), a 400K 4-to-3 parallel corpus
covering four formal languages (Dedukti,
Agda, Coq, Lean) and three natural languages (
English, French, Swedish), generated via
the Informath project.
https://github.com/GrammaticalFramework/informath
But the corpus could be an accident, maybe rather
a toy from the https://www.grammaticalframework.org/
folks, will this have an impact?
Bye
Mild Shock schrieb:
Hi,
Why does this Lama have a red pyjama.
Oh, its a baby Lama. Its still in the cradle
and needs some training:
RedPajama-Data-v2
https://github.com/togethercomputer/RedPajama-Data
But then Andrej Karpathy recently showed
GPT-2 training on rented GPUs for less
than 100 USD in less then 2 hours.
So where do these grown up Lamas go.
Well Georgi Gerganov prefered C++/C
when he shouted Llama Llama Red Pyjama.
But you also find WebLLM, wrapping the
underlying C++/C GPU interface via the
W3C standard WebGPU / WGSL, with JavaScript:
In-Browser LLM Inference Engine
https://webllm.mlc.ai/
My experience with WebLLM 6 months
ago on an iPad Pro 2024, still a little early
stage performance and robustness.
But hey hardware of AI mobile iGPUs is
still evolving, and AI laptop, AI smartphones
and AI tablets, will soon feature Chinese
hardware such some new Kirin AI in 2027.
Bye
Mild Shock schrieb:
Hi,
Remember when first all local AI was Python
and PyTorch APIs. And then suddently people strated
using bare metal C/C++ Code. Here is the story:
How it started:
GPT-J or GPT-J-6B is an open-source large
language model (LLM) developed by EleutherAI
in 2021. As the name suggests, it is a
generative pre-trained transformer model
designed to produce human-like text that
continues from a prompt.
https://www.eleuther.ai/
How it was going [Georgi Gerganov]:
So a few days later comes out the LLaMA, I do
some calculations and I figure out rCLOkay, 65
billion parameters. You probably need about
40 gigs of RAM, with 4-bit quantization. So
this can run on a MacBook. Why not do it?rCY
Why I was able to do it so quickly - basically,
for all that I saw itrCOs pretty much GPT-J architecture
with some modifications, like some extra memorization
layers. ItrCOs minor changes. Basically, again, the
existing code for the GPT-J, I just simply
modified it there, it happened pretty quickly.
https://changelog.com/podcast/532
Georgi Gerganov, Bulgarian, now with Hugging
Face, ggml-cann also running on Chinese AI chips.
ggml Manifesto https://github.com/ggml-org/ggml
Bye
Hi,
Years ago Sam Altman said to have no idea how
to generate revenue, but when the generally
intelligent system is in place, he might ask it.
Some schools approach the rCLgeneralityrCY from
a totally wrong perspective. Take the EyeProlog
Pseudo Scientism here:
The Art of EyeProlog https://eyereasoner.github.io/eyeprolog/the-art-of-eyeprolog
It is the same nonsense like constraint propagation,
the idea here is to evolve better software, that it
has as a main component refinement:
Start -> Algo1 -> Algo2 -> Algo3 -> Algo4 ...
But EyeProlog itself is an example of not using
this refinement. Like dropping the classical
WAM architecture, and back to YieldProlog somehow.
What if the world ticks like this
when it come to generality:
-a-a-a-a-a-a /-> Algo1
-a-a-a-a-a /--> Algo2
Start ---> Algo3
-a-a-a-a-a \--> Algo4
-a-a-a-a-a-a \-> ...
Innovation requires to start from scratch.
I think this little booklet, recommended by
Ernst Specker, Proofs from THE BOOK is a
book of mathematical proofs by Martin Aigner
and G|+nter M. Ziegler, first published in 1998.
Just wants to teach us about this bifurcation:
Chapter 1: Six proofs of the infinity of
the primes, including Euclid's and Furstenberg's. https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK
Yeah, lets aim for surprises by
generative AI, not refinement.
Bye
See also:
Sam Altman on his Business Model
https://www.youtube.com/shorts/pLnyjxgFxew
Mild Shock schrieb:
Hi,
Why is nobody mentioning Agda here. It has
beautiful dependent types, and tactics are
just programs. Poor Henk Barendregt, not
everybody likes dependent types it seems:
Are we stuck with Lean?
https://mathoverflow.net/q/513742/
Does Depependent types require proof objects,
which waste large amounts of memory. Well,
if you are not good in erasing them.
But is there a Red Pyjama for Proof Assistants,
the baby cradle where LLMs can learn proof
assistant lingua and strategies. It seems
yes, synthetic data corpuses to the rescue:
We address this gap by introducing SMAD
(Synthetic Multilanguage Autoformalization
Dataset), a 400K 4-to-3 parallel corpus
covering four formal languages (Dedukti,
Agda, Coq, Lean) and three natural languages (
English, French, Swedish), generated via
the Informath project.
https://github.com/GrammaticalFramework/informath
But the corpus could be an accident, maybe rather
a toy from the https://www.grammaticalframework.org/
folks, will this have an impact?
Bye
Mild Shock schrieb:
Hi,
Why does this Lama have a red pyjama.
Oh, its a baby Lama. Its still in the cradle
and needs some training:
RedPajama-Data-v2
https://github.com/togethercomputer/RedPajama-Data
But then Andrej Karpathy recently showed
GPT-2 training on rented GPUs for less
than 100 USD in less then 2 hours.
So where do these grown up Lamas go.
Well Georgi Gerganov prefered C++/C
when he shouted Llama Llama Red Pyjama.
But you also find WebLLM, wrapping the
underlying C++/C GPU interface via the
W3C standard WebGPU / WGSL, with JavaScript:
In-Browser LLM Inference Engine
https://webllm.mlc.ai/
My experience with WebLLM 6 months
ago on an iPad Pro 2024, still a little early
stage performance and robustness.
But hey hardware of AI mobile iGPUs is
still evolving, and AI laptop, AI smartphones
and AI tablets, will soon feature Chinese
hardware such some new Kirin AI in 2027.
Bye
Mild Shock schrieb:
Hi,
Remember when first all local AI was Python
and PyTorch APIs. And then suddently people strated
using bare metal C/C++ Code. Here is the story:
How it started:
GPT-J or GPT-J-6B is an open-source large
language model (LLM) developed by EleutherAI
in 2021. As the name suggests, it is a
generative pre-trained transformer model
designed to produce human-like text that
continues from a prompt.
https://www.eleuther.ai/
How it was going [Georgi Gerganov]:
So a few days later comes out the LLaMA, I do
some calculations and I figure out rCLOkay, 65
billion parameters. You probably need about
40 gigs of RAM, with 4-bit quantization. So
this can run on a MacBook. Why not do it?rCY
Why I was able to do it so quickly - basically,
for all that I saw itrCOs pretty much GPT-J architecture
with some modifications, like some extra memorization
layers. ItrCOs minor changes. Basically, again, the
existing code for the GPT-J, I just simply
modified it there, it happened pretty quickly.
https://changelog.com/podcast/532
Georgi Gerganov, Bulgarian, now with Hugging
Face, ggml-cann also running on Chinese AI chips.
ggml Manifesto https://github.com/ggml-org/ggml
Bye
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 74 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 45:25:47 |
| Calls: | 1,100 |
| Files: | 1,339 |
| Messages: | 275,372 |