We are both! The cloud service is for everyone to try right now. We have a paid local license version too.
But we started as local only however quickly learned thag cloud has a few advantages. we can have seamless github integration setup for people. And quite a few people prefer when things just work with a setup on every commit!
Convenience of the cloud or you can setup yourself with developer license.
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.
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
It depends on what you say is O(1). A theoretical Turing machine has an infinite tape that can be accessed in O(1), but in real life, it would require a machine of an infinite size.
Same idea for that transformer, it needs an infinite context, and it is an infinitely big machine, but with that level of abstraction, it processes a token in O(1).
In practice, there is no such thing as O(1) on arbitrarily sized data, there is no such thing as infinity either, it is just an abstraction.
It’s not the same for transformers, especially not with the theoretical infinite context. It simply doesn’t process tokens in O(1) in your given setup.
In practice, with frontier LLMs, it’s of course more complicated, and also they don’t reveal how they do lookups, but still the theoretical limit applies regardless.
Do you mind elaborating or perhaps providing some reference as to why you think transformers should be similar to a Turing machine on this specific criteria?
The context can change each time. To implement a UTM only requires 2 states and 3 symbols or the reverse.
So if you use the context not as a tape in itself, but as an io channel to read/write an infinite tape, the context for any given step can remain fixed in size, and so the step itself can be O(1).
Any basic lookup table is turing complete if you bolt an external infinite tape and read/write head onto it. But then that’s moving the goal post since the context wouldn’t be the “limitless tape” and it’s not a transformer “in the normal way” because turing completeness would be coming from external io and not from auto regressive self attention. Different topic.
The point is that the discussion is essentially entirely meaningless, as it's pretty much hard to implement any simple construct that can make deterministic decisions based on a data stream and wrap it in a loop without ending up with a UTM.
The consequence of that is that the original question GuB-42 raised is pretty pointless too. An "inert" transformer effectively has limitations, but as typically used it trivially becomes Turing complete, and so the class of problems it can solve is the exact same class of problems almost any of our other computational devices can solve.
And if you want to point out that this externalises all of what actually matters if we are talking about e.g. intelligence, then yes, it does. But by extension you can trade complexity of the tape for complexity of the machine, and so you can internalise any part of the problem that can be solved with a finite section of tape as a single state transition (trivial proof: For a given machine M with finite state, you can make your machine N execute those steps as a single state transition by having N run M on a state transition.)
To extend that to where I assume they'd want to go in the first place: A transformer wrapped in a loop with access to "just" a "tape head" can "only" be limited from being theoretically able to get all the way to human level intelligence if human brains depend on computations that exceed the Turing computable. But that is no different from any other Turing complete device.
Of course that says nothing of whether it's a practical way of getting there.
Of course it is. You’re conflating a turing machine with a transformer. Transformers don’t have a local read/write head. The [self] attention is over the whole context, which makes each step O(N) at best (with caching) and O(N^2) w/o.
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 '' 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.
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.
> In fact it has N read / write heads equal to the size of the context
And what is the asymptotic notation when computation scales linearly with the size of context?
> Either way, the simple truth is that you can train a transformer system
Which still doesn’t mean they have a read/write head or have O(1) complexity for token computation with “infinite context”.
> 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.
Completely false. If I start a company spending $5 in capital and issue ten shares worth 50 cents each, and later on my revenue from that company reaches $10 through my labor (or the labor of the employees I paid), then the valuation of the company is at least $10 (certainly more) and money has been created because those ten shares are worth more.
Unlike central bank printing or even loan creation, this method of wealth creation is not zero-sum and not inflationary.
Because of inflation. If there are people with astronomically more wealth than the rest of the population, they will push up prices. There is no such thing as a "high floor" in a system where there is extreme wealth inequality.
I don't see why that would happen. The money is being spent whether it's distributed to the masses and spent on food, or spent on a yacht. If anything it should be deflationary because the rich mostly don't spend their money, else they wouldn't be rich.
Because the 0.1% have an also-outsized influence on politics, and in making our world a better place in general (and they repeatedly fail all of us in both cases).
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
reply