I mean, Drop does mount host filesystem in the guest, the idea is that you keep working within your current distro and have access to some of its files.
This is great as a first look, but the author is not a developer, so we don't yet know whether a dev can be as productive with local models on M5 Mac Studio compared to a 20x subscription plan.
I'm also curious about any new low hanging optimization opportunities in the kernels for this new hardware.
It's already clear to me that M5 Mac Studio is more cost-effective than anything you can run on open router, assuming decent utilization.
The M5 Mac Studio will be the most cost effective way to run uncensored cyber capable open agents.
An exciting tipping point will be if programmers can get an Astra-Ultra like experience all week with this hardware. That would be a real sense where this hardware exceeds the value of even 20x cloud subscriptions.
Astra-Ultra? Even the largest open model to date (Kimi K3) is nowhere close to Astra level, and it will be quite slow even on the highest-spec M5 Ultra, with achievable speeds of about 0.5 tok/s at most due to having to stream weights from SSD (~13 GB/s on the highest storage capacity M5 Max machines so far). This is OK for doing simple Q&A in the background but it's far from a genuine coding experience. You'd have to test batching of multiple thinking streams in order to try and raise overall tok/s via layer-wise reuse of the streamed weights (and this is where the "Ultra" part sort of becomes relevant; Kimi series models have good support for agent swarms) but this would decrease single-session performance even further. It would only be usable for background jobs, though the hardware would then have a chance of paying for itself if it was fully used on a 24/7 basis.
That's all well and good but Qwen 27B is a small, dense model; that's favorable to both batching and MTP. Batching of large, sparse/MoE models like Kimi K3 (requiring slow SSD streaming even on a single maxed out Mac Studio) on local hardware is an entirely different game that's mostly theoretical so far: many people would even call it outright pointless. (MTP clearly fares even worse, though - unlike batching, it ends up wasting scarce weights-fetching throughput on wrongly predicted tokens.)
> This is great as a first look, but the author is not a developer, so we don't yet know whether a dev can be as productive with local models on M5 Mac Studio compared to a 20x subscription plan.
Local models are definitely not as productive as SOTA, sadly it's not close yet. I do think someday they will be "good enough" to use, but they aren't today. Even the SOTA models barely code well, with Opus 4.5 being the first, good coding model.
That being said, I think it's absolutely imperative that we keep pushing local model performance. We need to continue to advance technology there and ensure that the model labs don't do regulatory capture in the name of "safety" (or anything else).
With the latest codex (weekly quota burn) fiasco I tried open weight alternatives for the first time. And tyeah... open weight models cant compete with likes of astra yet. But, my hope is that by the time I get my Mac studio at end of november an open weight models would have closed the gap (which i think is realistic at the speed of progress). Now its true a better gpt version will also be available then but it also seems the gap is shrinking with time so theres that.
> And tyeah... open weight models cant compete with likes of astra yet
I think this is true, but also misses that a lot of us are just doing basic flask apps with a react front end. We don't need astra; Something sonnet 4.6 level locally is perfectly sufficient 95% of the time, and maybe 99% of the time.
This. People have convinced themselves that the absolute frontier is what is needed, anything below it is an unacceptable compromise, and we seem to be speaking different languages when it comes to discussing model capability.
It's like watching a discussion about cars available to take on a 100km road trip. A new car gets released that is on par with a Toyota Corolla but it is dismissed as completely useless for a 100km trip because it doesn't have the seat massagers and air ride suspension that the new Escalades have.
The reality is that something like Sonnet 4.6 is still amazingly capable for so many programming tasks, especially if you already have some reasonable level of experience to steer it in the right direction.
And if you think Sonnet 4.6 is still worthwhile, then it seems undeniable that something like Qwen 3.8-27B is also worthwhile.
Local models can be widely used as productive assets. Yes the infrastructure of SOTA API models is engineered specifically for you to be that utility, but the blanket statement that local isn't up to par is intensely short sighted. Billions of tokens per month on local pays for the hardware when compared to sota costs per month.
I believe they can currently be used productively for non-coding tasks (classification, light summary)... but they definitely are not even close to SOTA when it comes to software development.
Defining productivity is a use-case scenario, and a wildly generalized assumption for most people in this argument. Local infrastructure doesn't need to be sota for absolutely every single need for a dev lab, but it absolutely can be delivered with non-api frontier class models.
Just to be clear, I'm specifically talking about coding. I think local models can help with productivity today, just not coding.
I'm also a huge fan of local models and think it's absolutely imperative that they continue to advance so we can move off of the Anthropic/OpenAI hosted models. It's important to accurately asses where we are in that journey though.
I think the issue is generalization, if you were more specific about which local models aren’t good enough for which tasks compared to which frontier models in your experience, it’d be a lot more informative
Like the other commenter, I'm confused about the 'just not coding' conclusion. I'm using Qwen 27B on a 5090 at > 100tk/s with 150k context (which isn't enough admittedly), and DeepSeek v4 Flash with 1million context on a gb10/spark. Both of which are performing surface level, and deep needle precision infrastructure architecture. They code 24-7, stupendously.
It would be interesting to hear more about how you’re actually using them. Do you have sophisticated feedback loops around the models so they can verify their work and converge on good solutions? And how do you decide what to give the 5090 vs the Spark vs a frontier model?
Correctness matters much more than speed to me, but if I can get both, that’s obviously very interesting.
I so want this to be true, but for the kind of coding I do (not Flask apps), it's definitely not the case. Like I said, SOTA models just barely, barely work for me. My projects are usually 100k-1M lines of Rust or Go.
The SOTA models now work really well in my codebases, but that's only been since Opus 4.5/4.6-ish. Prior to that, and with current local models, they simply couldn't work holistically and would just thrash around. Now I feel as if SOTA are approaching my coding levels if not surpassing it. I still need to guide on architecture, but I can see that going away within the next year or so as well.
I can launch Astra to deploy changes to my homelab via creating Forgejo issues from my phone. That kind of system is pretty hard to set up without kubernetes.
Even if you confine yourself to a dev workstation, having 5 agents concurrently building testing deploying code makes your computer loud and/or hot.
K8s jobs don’t run in a secure runtime. K8s jobs don’t give you dynamic zero trust permissions scopes. Restoring a harness in 500ms is really fast, much faster than naively creating a new job downloading session and ‘codex resume’ etc.
You might be right, it likely needs a full proper PC setup with the test suite stuff. I was looking at this vendor, https://www.gmktec.com/collections/all there's this whole AI mini-pc market but they aren't quite a full dev machine replacement
I’m running ~5 agents at a time very comfortably on a $280 mini PC with 8GB. They’re all in Docker containers, a couple have sidecar VMs they can own and run. Not having any issue with load.
So the agent-substrate checks a _ton_ of boxes. Almost all of the things it offers should be table stakes for everywhere we run not only agents but most software.
(For context I built something very similar to this the past 2 weeks for my homelab, trying to solve many of these problems. This comment is an edited version of an unreleased blog post I wrote last week.)
- Run code in secure microVMs or gVisor. Docker is not good enough. Qemu is not good enough. A secure environment for running untrusted code is the bare minimum. I don't see Firecracker in the repo yet, but that's ok the idea is there.
- Fast resumption. In my homelab, time-to-first-message is around 11-12 seconds. That's half setting up the pod, and half resuming the CLI (e.g. `codex resume ..`). Why resuming? In my homelab agents are commonly blocked waiting for CI or waiting for me to approve an action, in this case I stop their container to keep resource usage low. Then for resumption, you definitely don't want to waste the agents time by giving a new ephemeral disk and forcing them to re-clone and re-build. For microVMs this is not actually straightforward, for example Firecracker only allows block devices, so re-attaching an agents disk workspace requires a custom storage interface
- Zero Trust. Codex CLI permissions for example are extremely broken. "Can I run this 500 line long command? or allow any command starting with first 100 chars always?" More reasonable grants are needed.
I don't understand yet how they will surface Zero Trust notifications. In my homelab it's a Forgejo comment linking to an auth service, and a ntfy.sh iOS notification which opens up the auth service.
I don't get why they to restore the RAM of the agent env. Maybe to fully optimize resumption. Idk, I don't have that much RAM in my homelab, my agents use a ton, testing stuff in Chromium making screenshots for me. I can't keep RAM for 100 workspaces from the past 24 hours in RAM.
MITM gateway is very cool.
I'm curious how they will integrate with microVMs. I just wrote yesterday[1] about how there are NO GOOD OPTIONS for this atm. Kata is decent but the attack surface it introduces makes me uncomfortable.
But anyway, even if this project is abandoned out of the gate by Google, we should be happy, it sets the bar where it should be. I'm excited to learn how they solved these problems differently than I did.
Restoring memory is useful if, when you resume an agent VM, you want the apps to be in the exact state when they were suspended.
But for most things, I find resuming with memory is more trouble than it's worth. If you always resume from memory, you lose the ability to control the state of a VM. It's much easier to define which services should run than to define which active RAM state should be purged
Similar to why "did you try turning it on and off again?" is good for system reliability.
> I don't get why they to restore the RAM of the agent env. Maybe to fully optimize resumption. Idk, I don't have that much RAM in my homelab, my agents use a ton, testing stuff in Chromium making screenshots for me. I can't keep RAM for 100 workspaces from the past 24 hours in RAM.
This is going to be decomposed. I believe the plan is to offer resumption with disk state only as well (and the RAM snapshots will need to be discarded from time to time, if you update the underlying code of the agent, or switch CPU types).
By the way, the RAM snapshots are not kept in RAM, they are serialized to disk, or uploaded to object storage.
It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable.
For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable.
Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation.
Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.
We are talking about the same thing, but I would actually put this the other way around.
Computation and computability is "the final frontier". Math is a "subset" of that. Doesn't matter if we choose ZFC or in the future discover some "better" subset of core axioms, we will always hit limits where BB will trivially skip over whatever we could prove (let alone Gödel's theorems).
> given fixed input of the statement with no other information sources
Also, this is just trivially avoidable, so not sure if we really should be concerned about this limitation. An LLM in a loop where it can write on a tape can be Turing complete, ergo it can compute anything computable and is "bigger" than math at that point.
> Computation and computability is "the final frontier". Math is a "subset" of that.
In what sense? BB(n) is a prime example of an object that can be mathematically defined, yet is not computable. Or see BBB(n) for an "even more" uncomputable function. [0]
> An LLM in a loop where it can write on a tape can be Turing complete
What does this mean? A given LLM, like a given C program, can't really be Turing complete or not in a meaningful sense. The C programming language, or the concept of LLMs in general can be said to be Turning complete or not. Do you mean to state that LLMs in general are not Turing complete, but being "in a loop" somehow makes a difference?
> it can compute anything computable and is "bigger" than math at that point
Again, in what sense is it "bigger" than math? Lots of things are Turing complete, I wouldn't classify lambda calculus as "bigger" than math.
> Computation and computability is "the final frontier". Math is a "subset" of that.
Maybe I'm misunderstanding you point, but I don't know how widely this would be held as true. Are you defining "math" as _only_ what can be proven under some particular formal system?
Well, I only know how to define computability in terms of Turing machines.
For math I don't have a fix definition, but it's surely a bit more specific than that (e.g. I wouldn't consider the computation that prints a 0 at the same place for infinity math) - but of course I do see the circularity in my argument: a Turing machine is a mathematical object in and of itself. Though being able to talk about something doesn't necessarily change which is "bigger".
As for the other direction, this gets a bit more into the philosophy behind math itself. Constructive math's territory is "easy" - but I am on the opinion that if humans (or any intelligent physical entity) are at most Turing-complete [1], then any non-constructive math "steps" or thoughts must also be at most computable. Well, unfortunately I can't prove whether math done by transcendent entities are also computable, though.
In any case, I am no mathematician, so whatever I think regarding this topic may not have much relevance to anyone, only done CS course with quite a bit of math, but that's obviously not the same.
[1] I believe religion is an escape hatch here from an argument perspective
> if humans (or any intelligent physical entity) are at most Turing-complete
This is a bit of a strange assumption to make. I do agree that a human, if it had infinite memory, would be an universal machine, i.e. capable of computing any given Turing machine [0]. But would that be the limits of its capabilities? It's far from certain.
You'll get into the philosophy of free will (funnily enough, a sort of inverted Turing test), i.e. for a given human with infinite memory, is there a Turing machine that exactly replicates the behavior of that human? Is our behavior governed entirely by rules? Would that imply that a human themselves is a kind of Chinese room [1]?
> any non-constructive math "steps" or thoughts must also be at most computable.
What does it mean for a "thought" to be computable? Compare to Gödel's incompleteness theorem. Clearly the act of stating the thought, or writing down the theorem, is computable. But proving it to be true or false may very well be impossible.
> What does it mean for a "thought" to be computable?
Well, given our scientific knowledge it's a molecule-level (only important to disregard quantum physics to make the case easier) physical/chemical process, that we should in principle be able to simulate on any other medium, including a Turing machine.
Nonetheless, I can accept the definition of math where it's about "truths" and truths can obviously exist without being computable.
> any physical system can be evaluated to any degree of accuracy by a computer
That's an interesting hypothesis, but I don't know why you'd assume it to be true at face value. It's a bit unclear how you would even define "evaluated", given that we don't yet have a mathematical model of all of physics as we know it. [0] And then consider unknown unknowns.
> Do you agree that humans are physical systems?
Do you consider humans _with infinite memory_ as physical systems? Do you consider computers _with infinite memory_ as physical systems?
I agree that physics being simulated is not that easy to handwave away. That's why I mention that brains probably don't "depend" on some quantum-level behavior and a more macro view of physics could be enough. What I mean here is that while there are obviously quantum effects in play at the atomic/molecular levels, if we take the cells as a black box and replace them with statistical processes, we would probably still get a human intelligence as a result - but of course I can't prove it. As a hunch, the 100 billion neurons and their 100 trillion connections, and of course their environment (glial cells are important)'s proper Simulation is enough.
As for the infinite memory, Turing machines have this nice property that they can only visit a finite amount of memory after finite steps, no matter what. A Turing machine running for a finite time (we got this) will surely use a finite space, so being "a bit short" on infinite space is not a problem, I believe.
Let me illustrate with an example. Are you familiar with with the Collatz conjecture? It's an example of a system with only one variable, and two simple rules. Are you certain that there exists a computer program that in finite time can compute where any given integer ends up?
Now consider throwing a ball in the air. Can you even write down the rules that each of the ball's subatomic particles obeys? How can you be certain there exists a computer program that in finite time can predict where any of the particles, for any ball, ends up?
> the chemistry of the brain is very well modeled
There are models, but the fact of those models is that they do not apply to "any degree of accuracy", as you claim.
Consider the ball thrown in the air again. Is the ball affected by what happened 100 years ago, inside of a black hole 100 light years away? Why would it not be affected by that? Or if you grant that it is affected by that, do we then need a model to predict those effects before we can "evaluate" them?
EDIT regarding the below linked blog post: Did you read the rest of my comment? Did you even read the blog post you linked to?
> We certainly don’t have anything close to a complete understanding of how the basic laws actually play out in the real world — we don’t understand high-temperature superconductivity, or for that matter human consciousness
Can you try to consider my central point before replying: Are the rules governing physical reality simpler or more complex than the Collatz conjecture? Does there exist a (theoretical) computer that can "evaluate the Collatz conjecture to any degree of accuracy"?
EDIT 2: I'm not the one moving goalposts. On what grounds are you classifying the question whether a given number ends at 1 or not for the Collaz conjecture as an "inifite" computation? It's a simple boolean question, yes or no. All you have to do is build a computer that can answer yes or no for each integer. Isn't that simpler than answering the position of each atom in the ball after the throw? Each is just a function, what makes one more infinite than the other?
PLEASE just stop complaining about "moving the goalposts" when the issue is your own lack of clarity of both expression and reasoning. WHAT is the distinction between "simulate" and "predict"? You said neither by the way, you said "evaluate".
> ANY physical system can be evaluated to ANY DEGREE of accuracy by a computer
It's completely SENSELESS to claim that they are distinct, because in order to EVALUATE or SIMULATE the physical system you will need a FUNCTION which COMPUTES the STATE of the system at a given point in time. The only POSSIBLE distinction between SIMULATING and PREDICTING would be the time taken for the computation, but that is COMPLETELY IRRELEVANT as long as it is finite.
Again, your own source says:
> We CERTAINLY don’t have ANYTHING CLOSE to a complete UNDERSTANDING of how the basic laws actually play out in the real world
> You said neither by the way, you said "evaluate".
You are entirely correct. I was sloppy in my first comment. I should have said simulate. My sincere apologies if that's been the crux of our dispute.
> The only POSSIBLE distinction between SIMULATING and PREDICTING would be the time taken for the computation
No. The distinction is in determining which "you" is you. When simulating the wavefunction, every you is simulated.
> We CERTAINLY don’t have ANYTHING CLOSE to a complete UNDERSTANDING of how the basic laws actually play out in the real world
It's very understandable if you include his following sentence:
> But these are manifestations of the underlying laws, not signs that our understanding of the laws are incomplete
He's saying we don't understand emergent behavior produced by the laws - not that the laws themselves are incomplete. E.g. we don't know how/why a bag of neurons turns into a person.
Re: Collatz - you've moved the goalposts. Answering Collatz requires solving a halting problem. I didn't claim that I could find the end of an infinite computation. I claimed to be able to simulate a finite one.
And - you should reply to my comments rather than edit your old ones.
Does that mean that humans could produce mathematical proofs that are entirely logical and verifiable by other humans, but that cannot be formalised in any automatically verifiable language such as lean?
Even if the busy beaver sequence were computable and the halting problem were decidable, Gödel's incompleteness theorems would still prevent all theorems from being solved, regardless of if one used LLMs or not.
I think there's a really important sense in which Godel's argument is not the full story.
IIUC, Godel's incompleteness is less about theorems and more about axiomatic systems. Given an axiomatic system, there are statements within it which cannot be proven or disproven. It's relatively unrelated to the platonic ideal of the theorem itself. The statements it considers are axiomatic-system-specific.
Another way to view it is, who cares if we can't prove or disprove "This statement is false". Ok, the axiomatic system is incomplete; fine. What's important is can the system prove a real theorem that I care about.
The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". This format can encode many math problems. And we know already that BB(432) is independent of ZF, aka, there is a 432-state TMs which ZF can't prove or disprove the halting behaviour of.
So BB looks at real theorems, ranks them, and we can ask what axiomatic systems can solve them or not. Godel looks at 1 axiomatic system and produces a toy theorem which the system can't solve. That's an extremely important difference!
The core issue is that any fixed LLM can only encode so many axiomatic systems in its states, and the fixed systems implies an upper bound in terms of the BB number which it can solve. Godel is only looking at one system at a time, while BB is a way to use a common problem format to rank every axiomatic system on an infinite number line.
But a 432-state TM is a problem that we would like to "prove" is it not? It's not even a particularly complex one to begin with, my smartwatch has orders of magnitude more state then that and yet here we see that all of our math "fails" at it.
I'm no mathematician, but this is also the crux of Gödel's theorem, he just showed it in a more "hacky" and clever way - but BB(432)'s relation to ZF is also a consequence of Gödel's more general idea, is it not?
Even more concretely, the halting problem for turing machines with halting problem oracle would be undecidable for them. And if you could solve that you won't believe what problem would be undecidable. It's turtles all the way up.
The problem with what you're saying is that any old random true proposition about the integers is not necessarily interesting enough to be called a theorem. GIT (or the uncomputability of the Busy Beaver problem) does not establish a limitation on proving theorems, but rather on determining whether a proposition is true or not. Most propositions are ugly and irrelevant. So GIT/Busy Beaver is irrelevant.
-----
Oh, and: All proofs are conditional on axioms. If those axioms are computably enumerable, then all of their consequences are computably enumerable too.
Most propositions may be ugly and irrelevant, but how do you know how many are not so and we just can't prove it? Also, what about stuff like Continuum Hypothesis, would you add it or not?
> It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable
LLMs use RNG for sampling, so they are not pure computers.
Can you make any similar guarantees about Drop?
reply