anon291

I work on AI and I oppose a bailout for an ai bubble or whatever else.

If you're lucky enough to be in this field and you're not managing your finances, that's not the governments problem to fix

Why is this a cloud service instead of a local emulator? I don't get it

At each cycle, a cpu is a simple function from the previous state to the next state.

> There’s no such thing as a read/write head in transformers. You can use it as a metaphor but that’s a leaky metaphor, hence all these misunderstandings.

The input to a transformer is a list of embeddings. The output is a list of embeddings of the same length. At the end of the day, you can represent the entirety of the transformer's matrix multiplies and such as a DFA (IEEE 754 float multiplication and addition is a simple DFA, and you're just scaling this up that many times). Thus, you take a list of embeddings (i.e., the tape) and output another, modified, list of embeddings. You have successfully read (ingested) and written (the transformer output) N positions on a tape.

Yes. Aesthetic things are good for the soul in subtle ways. It's like making a split pea soup without a bay leaf. You wouldn't be able to figure it out, but you know something is missing and it makes most people sad even if they can't identify it.

> but they won't increase the value of the house.

But they will make your life better.

The papers describing lean and it's core operations are deliberately small. The kernel of a theorem prover is meant to be such that a human can check it for correctness. The kernel does not include things like type inference or execution. It literally checks the proof and that's all and everything needs to match exactly. It's fairly trivial to write such a thing.

Humans have to establish trust in this.

After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it

Hey now... If you have a formulation in type theory (lean is not set theory), then you can translate to homotopy type theory fairly easily

of course it has a read write head. In fact it has N read / write heads equal to the size of the context since each latent state is updated with the results of the cross attention mechanism at each step.

Alternatively, you can view the '<unknown>' token that is dynamically driven to the embedding of the output token to be the write head. Either way, the simple truth is that you can train a transformer system (i.e., an iteratively applied transformer) to simulate an arbitrary turing machine.

It's not contradictory at all. The dfa at each step of the turing machine model is also o(1).

For the umpteenth time a transformer is an arbitrary turning machine due to the fact that it has a theoretically limitless tape (the context).

A single transformer step is simply O(1) (for a particular parameter size), but it applied a potentially infinite number of times.

Thus while a single transformer cannot solve any problem, a transformer system applied in the normal way can solve any computable problem.

This is why I bought real estate in the bull market of the last decade.

That's a surmountable political problem

No because companies trade at multiples of revenue. A $10/yr in revenue company would trade at a total market cap of like $200. That $190 is new money.