zozbot234

Artificial Analysis still has MiMo 2.6 Pro setting the Pareto frontier where it matters: it's as cheap as Terra High/Sol Low while being smarter than Terra Xhigh. Sol Medium beats MiMo in smarts but is priced a lot higher. Meanwhile Terra Max is dominated by Sol High in both price-per-task and smarts.

Post-training is not about "secret knowledge": it's literally about training the model in a RL environment on very specific tasks (including, potentially, cyber exploitation). It's just as compute-intensive as pre-training these days, if not more (given that several checkpoints of the same pre-trained model are being released, showing sizeable gains in real-world capabilities for non-trivial productivity tasks).

> For a model it doesn’t seem that far fetched to make the leap from “I have the knowledge of what hacking is” and “I know how computer systems work” to just being able to exploit stuff anyways.

You'd be surprised. Cyber offense is a very narrow domain, especially given the extensive mitigations that are being used in modern systems. Leaving it out of post-training tasks unless you're specifically interested in it is the no-brainer approach.

Post-training (i.e. RL fine-tuning) not pre-training. This is just a post-trained checkpoint of the K3 pretrained model.

What "rules"? They don't have to post-train the model on anything specific, it's their judgment call.

"Cybersecurity" as a general term often includes offensive "cyber" which is what is being talked about here.

> should the model be opened it’s still not dealignable because it just doesn’t know enough

This is the only AI-safe approach - see the OpenAI agent swarm incident where the swarm engaged in offensive cyber because guardrails were not active for their task and the model had clearly been post-trained on that narrow domain.

This is not about guardrails, it's just not post-training the model on tasks that specifically relate to cyber-offense. It's a very lightweight intervention, and it makes the model less of a target for bad actors.

It's not actively nerfed like the Western frontier models, it's just downweighting offensive "cyber" as a domain for post-training/fine tuning. Which, if anything, ought to improve model capabilities wrt. other domains.

Looped transformers are entirely equivalent to running a single pass through a much deeper network with shared/repeated parameters. There's nothing about it that's specifically "reasoning in latent space" any more than a much larger model "reasons in latent space" from the POV of a much smaller one. An objection to looped transformers "reasoning in latent space" is ultimately an objection that applies to any kind of efficient scaling; it's also worth noting that there's been successful work on extracting ex-post natural language descriptions of these internal latent states, so it's not entirely correct to describe them as inherently non-surveyable.

Kimi K3 has been demonstrated on a top-of-the-line laptop Mac running at several seconds per token (it has to fetch essentially all experts from SSD, since IIRC the dense part of the model takes around ~105GB on its own!). That's impressive enough if you only care about pure Q&A/chat or pure unattended tasks, but it's not what one would expect for agentic work. You'd need quite a bit of additional RAM to have good caching for the most common experts, and even then that would only help so much. MiMo Pro would be a roughly similar story.

> Or a cluster of consumer hw, and that comes with its own problems and drawbacks (esp in pp which matters a lot for agentic stuff).

Prefill actually ought to work well on a cluster AIUI, since it can leverage both pipeline parallelism and batching quite effectively.

The "upper end" of local models as of today would be something like MiMo 2.6 Pro or Kimi K3, either of which is significantly smarter than Qwen Flash-Next. Roughly comparable in smarts to the old GPT Terra series, not quite as capable as Sonnet. But yes, running these models locally at realtime-usable speeds and without heavy quantization would be even harder. They can be quite tolerable for plain Q&A chat and great for running multiple unattended workloads on a 24/7 basis, but that may be a bit of a niche.

Agreed. I assume aftermarket Linux support for Android devices with out-of-the-box unlockable bootloaders (including the OP6/6T) is the most likely path to viable daily-driver "Linux phones" in the future, and it's strange how the linked article doesn't seem to mention this at all.

If you want to checkpoint/resume applications arbitrarily, as AOSP does, you have to virtualize all of those resources anyway. Check out the CRIU patchset (since merged to mainline) which can even resume applications seamlessly across hosts, without any VM being involved.

> Safe Rust prevents data races not because they were separately considered as a tradeoff, but because its particular chosen design for memory safety requires it. It's a side-effect, not an orthogonal feature.

Data race freedom has been specified as a requirement for UB-freedom (i.e. safe code) since the C11/C++11 concurrency model, which predates the Rust borrow checker. You can make different choices on particular platforms, but they come with challenging tradeoffs: e.g. in Java, variables of type "long" are not data-race free on 32-bit platforms; writes to a long can silently tear.

How good is your Mandarin Chinese? You can easily find recent press release from Demingli and more general commentary about the state of the market inckuding mentions of other, lesser known firms.

There's rumors floating around that Chinese firms will soon be bringing new PCM storage solutions to the datacenter market. Not nearly as good as 3dXPoint/Optane, but should nonetheless be lower latency than Flash and much better endurance (DWPD).

If the pricing is competitive it will easily be replacing DRAM for many lower-level uses, thanks to its support for better PCIe standards (5.0 at least, while aftermarket Optane is stuck on 4.0).

> Why is coming up with a better proof (e.g. shorter, more intuitive, more general, connected to existing frameworks) thankless work?

I think the plausible version of this claim is that it's thankless work compared to solving the problem itself. The Quasi-Riemann Hypothesis and Hilbert's 10th problem over Q have both been described as "instant Fields medal worthy, no question asked". Explaining and cleaning up the proof is obviously important, but also quite a bit easier, and we don't really know what future 'Fields medal worthy' achievements might look like.

You're right that "wipeouts" and "total population turnover" basically doesn't exist in our genetic history, but there's one critical exception to that rule of thumb: massive epidemics really do wipe out entire local populations, and given that early farming was involved (with its higher pathogen burden) this cannot be ignored as a factor here.

> The idea of puzzling out what an AI did to prove something sounds quite boring and unappealing.

The way I see it, it's no different from a lot of grad student work where you have to figure out what a human-written proof is doing.

> Maybe they could have gotten into contact with the people of the research areas of the problems that they solved and worked with them to create a better exposition.

That's what Anthropic is doing, and the issue is that people will complain that they weren't the chosen "person to work with". OpenAI's approach is more like a race where everyone's at the same starting point: they get the AI's raw proof to work on and have to figure out how it works.

AIUI, the main limitation with &Cell<T> is (1) no provision for concurrency, obviously - though the various Atomic* types work similarly via interior mutability; and (2) data has to be read, written or modified as a single operation - any provision for enabling subobject access or the like is quite ad hoc, and has to be implemented for the specific type you're working with. GhostCell (and QCell, LCell etc.) generalizes this by tracking the use of shared references at compile time, such that writes will not overlap with each other or with reads, without enforcing a "get/set in a single step" workflow.

It may be interesting to focus on how exactly these planned "no-access" references would differ from raw pointers? Access through raw pointers is an unsafe operation already.

Rust needs shared xor mutable in order to prevent data races on non-atomically accessed data. You said that Valen can _express_ shared xor mutable, but perhaps you haven't clarified whether this also interacts with equivalents to Rust's Send and Sync to enable the same fearless concurrency.

> Just to clarify, Valen's borrow checker can express shared-xor-mutable, its value proposition is that it can _also_ express mutable aliasing (with `in`).

Just to clarify, Rust's borrow checker can express mutable aliasing via interior mutability (i.e. UnsafeCell<T> and the various Cell<T> types). A &Cell<T> reference is essentially a mutably aliased reference. The goal is exactly that people "only reach for mutable aliasing when it will benefit them". Of course, any ergonomic improvements around the Cell types are quite welcome, especially if they help C/C++ interop - provided that they're proven to be as sound as the existing borrowck.

> The point is that so far the AI is not doing a good job at explaining the "trick", so we (humans) have to do it.

Sure, but that's a real technical limitation with current AIs, not something that AI firms should be blamed for. And if anything, this creates a viable career path for the mathematicians who were "scooped" wrt. the original solution: they can at least puzzle out what exactly the AI managed to do. Many practitioners are actually quite excited by this possibility; Tao's stance is by no means universally shared.

> AI is not generating new techniques

Source? I assume that many of the approaches embedded in this proof dump will eventually be distilled and generalized into new techniques. That's how proof techniques tend to come about anyway (before AI): human mathematicians do something novel and unexpected to solve a particular problem, then efforts are made to understand how the "trick" works.

Agreed. Basically, if you don't make any effort to understand the proofs and you just look at the final answer, it will look like this proof dump is "strip mining" entire branches of math. But this is a pretty short-sighted way of looking at the issue: there will be plenty of novel approaches to be uncovered here.

> What’s not clear is whether the juice is worth the squeeze: will all the money spent on spamming the AI and human mathematician time spent studying the outputs progress the field “better” than without the AI?

The AI proofs are a side-product of benchmarking current and in-development models on especially hard problems. They're clearly cost effective for frontier AI firms, and free for the taking as far as human mathematicians are concerned. The real issue with them is that they look like bizarre nonsense as written, so they need mathematicians familiar with those specific areas of math to "decode" and digest them.

He also has an AI harness named after him (Prime Agent) so there's that.

Doesn't OnePlus 6/6T have good "close to mainline" kernel support already? Why wouldn't it work within LineageOS eBPF/version requirements?