skybrian's recent activity
-
Comment on Yandex outage: data shows that instead of going dark, malicious bots went on the move in ~tech
-
Yandex outage: data shows that instead of going dark, malicious bots went on the move
8 votes -
Comment on Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs in ~tech
skybrian (edited )Link ParentFrom the paper: When they write about "mistranslations," they seem to be showing that the intermediate lemmas don't match? This wouldn't invalidate either proof, necessarily. They could have...From the paper:
We do not make claims about the correctness of OpenAI’s NL proof, we only make statements
about mistranslations into Lean.When they write about "mistranslations," they seem to be showing that the intermediate lemmas don't match? This wouldn't invalidate either proof, necessarily. They could have reached the same destination by different routes. Both could have correct lemmas, but different.
Since they take different routes, the Lean proof being correct doesn't guarantee that the NL proof is correct. For example, a "mistranslation" might be a correction! Perhaps the translator noticed a mistake and fixed it by changing the proof?
Since it's very likely that the Lean proof is correct (it's been checked automatically), that means that if the NL proof is wrong, its mistakes somehow didn't matter. This reminds me of a joke:
that the mathematical literature as a whole is so reliable comes down to the fact that, over time, we have made an even number of sign errors
-
Comment on Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs in ~tech
skybrian Link ParentI'm not a mathematician, but I think they do check that the Lean proof is proving the correct problem, and the rest gets verified automatically. This is a lot easier than reviewing the entire...I'm not a mathematician, but I think they do check that the Lean proof is proving the correct problem, and the rest gets verified automatically. This is a lot easier than reviewing the entire proof. So that shows that it's true.
For the natural language proof, it's a bit odd that mathematicians can be somewhat casual about it, but my impression is that it's sort of like how you wouldn't consider a spelling error to invalidate someone's entire argument, provided that you otherwise understand the argument. It's assumed that minor mistakes can be corrected by the reader and are unlikely to make the proof invalid. Also, maybe it's okay if some statements in the proof are proven in a slightly different way? The goal is to understand the journey well enough to get to the same place, rather than to repeat the journey exactly.
-
Comment on MIT class project turns into an US Food and Drug Administration-cleared treatment for tremors in ~health
skybrian LinkFrom the article: [...] [...]From the article:
The three founders of Encora who are still with the company are Carballo, Allison Davanzo ’18, and Kyle Pina ’18. They were each seniors in 2017 when they enrolled in 2.009, MIT’s popular product-design class.
The semester began with a brainstorming session in which groups of about 17 students were asked to come up with dozens of potential product ideas. Carballo proposed a wearable device that used mechanical vibration to send signals to the brain to reduce tremors. The initial idea was to help patients with Parkinson’s disease.
“It was one of hundreds of throwaway ideas,” Carballo recalls. “The initial concept was inspired by classes I had taken in robotics around neural control of movement. I had a preliminary understanding of how an electromechanical device might interact with the body’s control systems and feedback loops that control movement to relieve pathological control of movement.”
The team eventually whittled their long list of ideas down to a few. Carballo’s idea was finally selected by a vote of 16-1 — with Carballo the only dissenting vote.
“I tried to explain to the team that this was so far-fetched that there was no way, in one semester, we would be able to make anything,” Carballo recalls. “Thankfully, I got outvoted.”
[...]
One current approach to target those signals is surgery that involves drilling holes in the skull to insert electrodes that drive new electrical patterns in the brain. Encora’s watch-like product targets the same brain regions with mechanical vibrations at the wrist.
“We’re applying mechanical stimulus, basically vibration, to stretch receptors in the wrist, which tell your body where it is in space,” Carballo explains. “The stimulation causes the receptors to activate and send a patterned signal to peripheral nerves of the wrist, that then carry the signal to the peripheral nervous system and into the central nervous system, to the same regions of the brain targeted by surgery.”
In 2024, Encora ran a randomized control trial with 47 patients living with essential tremor. Last year, the team ran a 59-person trial where patients used the devices at home. In both trials, more than 70 percent of patients experienced meaningful improvement.
The results were promising enough to gain what’s known as 510(k) clearance from the FDA for use as a medical device, in February of this year.
[...]
Today, Encora is focused on building a national sales force and working to secure coverage from insurers. As the company ramps up production, the product will finally become available for patients who qualify.
-
MIT class project turns into an US Food and Drug Administration-cleared treatment for tremors
15 votes -
Comment on Ukraine accuses SpaceX of crippling drone missions as ties with US worsen in ~society
skybrian LinkFrom the article: [...] [...] [...] [...]From the article:
Ukraine accused Elon Musk's SpaceX on Wednesday of limiting Starlink services, crippling its drones, as Russian missiles knocked out power stations in attacks President Volodymyr Zelenskiy called "ostentatious disrespect" to Donald Trump.
[...]
Ukrainian military officials said Musk's SpaceX had without warning interrupted functioning of military-grade Starlink terminals moving at high speed, effectively preventing Kyiv from using them as onboard guides for drones.
"Our defence forces did not receive a warning about this limitation, and this led to the disruption of several missions," presidential adviser Serhiy Beskrestnov wrote on Telegram.
[...]
Sources have told Reuters and other news organisations that the US has threatened to cut off intelligence for early warning of missile strikes on Ukraine, to press Kyiv to suspend attacks on Russian oil refineries.
[...]
Ukrainian officials said late on Tuesday they had received no warnings from Western partners for a second day before the massive Russian attacks on the capital. Trump had insisted on Tuesday that Washington was still sharing intelligence.
[...]
Starlink does not work inside Russia, and Ukrainian drones hitting Russia's oil industry use other means of communication, but Ukraine uses Musk's system to guide drones over its own territory, including parts of Ukraine occupied by Russia.
"According to our observations, during flights, the connection could drop for 10–20 seconds at speeds of just 110–120 km/h. The drones kept moving, but these interruptions made them harder to control," Ukraine's 7th Rapid Reaction Corps, deployed in the southeast, said in a statement to Reuters.
A source in Ukraine's defence ministry said the limitations significantly complicate logistics and some drone operations.
-
Ukraine accuses SpaceX of crippling drone missions as ties with US worsen
21 votes -
Comment on Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs in ~tech
skybrian LinkObviously this is over my head, but there are some blunt claims in this Twitter thread by Elliot Glazer, a mathematician and expert at formalization, that this doesn't affect whether the proof is...Obviously this is over my head, but there are some blunt claims in this Twitter thread by Elliot Glazer, a mathematician and expert at formalization, that this doesn't affect whether the proof is right:
This Navier-Stokes mistranslation thing is a nothingburger. Like 5 of you are making a nuanced (frankly pedantic) point about readability issues that are being phrased in a way that sounds to non-math ppl like there are serious doubts the proof is correct. There is no such doubt.
...
They're the same proof. The disagreements between them are smaller than a typical pair of human presentations of the same proof.
...
If OpenAI presented its autoformalizer a wrong proof of Navier-Stokes, it would not have successfully formalized it. The proof is right and nearly identical to the Lean conversion.
-
Comment on Those viral claims about plummeting Russian ‘bot’ activity have no basis in fact in ~society
skybrian Link ParentI don't think I'm immune, but I think I do better than people who are reposting memes without checking them at all. (At least, when I actually check!)I don't think I'm immune, but I think I do better than people who are reposting memes without checking them at all. (At least, when I actually check!)
-
Comment on Those viral claims about plummeting Russian ‘bot’ activity have no basis in fact in ~society
skybrian (edited )Link ParentYour argument is like saying nobody should use a search engine because some people found qanon or Al-Qaeda that way. Yes, there are real stories where people got suckered in by feeding their own...Your argument is like saying nobody should use a search engine because some people found qanon or Al-Qaeda that way. Yes, there are real stories where people got suckered in by feeding their own delusions, but using an AI like a search engine to ask a factual question (like I did in my example) is not the same.
-
Comment on Those viral claims about plummeting Russian ‘bot’ activity have no basis in fact in ~society
skybrian Link ParentMuch like with catching security bugs, asking an AI for a quick fact check before posting or resharing might help. Here’s an example. In this case, it found that other people had already done the...Much like with catching security bugs, asking an AI for a quick fact check before posting or resharing might help.
Here’s an example. In this case, it found that other people had already done the fact-checking.
-
Comment on Those viral claims about plummeting Russian ‘bot’ activity have no basis in fact in ~society
skybrian Link ParentYeah, it’s popping up all over the place, on Bluesky too. We’re hearing a lot of people saying it because it’s a meme going around. Most of the people resharing are political types who don’t care...Yeah, it’s popping up all over the place, on Bluesky too.
We’re hearing a lot of people saying it because it’s a meme going around. Most of the people resharing are political types who don’t care about journalistic standards of evidence when it’s something they want to believe. That’s why they’re susceptible to disinformation!
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
skybrian Link ParentThe difference between this sort of thing and the HuggingFace incident is that OpenAI had a kill switch and also confessed pretty much immediately as soon as they knew. Big Tech firms are American...The difference between this sort of thing and the HuggingFace incident is that OpenAI had a kill switch and also confessed pretty much immediately as soon as they knew. Big Tech firms are American companies that can be sued and there are many ongoing lawsuits for other things they did.
(Admittedly, you and I aren't likely to sue them, but someone can.)
When there's a war or international grey zone, which sometimes the Internet is, regulation and lawsuits no longer work. Yes, computer viruses usually have an author, somewhere, but good luck suing the Russians, North Koreans, Iranians, etc. It's one reason why many websites huddle behind Cloudflare.
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
skybrian Link ParentOnly running code that's signed by a developer should help somewhat. Is that what you meant by "whitelists?"Only running code that's signed by a developer should help somewhat. Is that what you meant by "whitelists?"
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
skybrian Link ParentAI is pretty good at finding security bugs and can also be used defensively. The question is, how often will people actually do that?AI is pretty good at finding security bugs and can also be used defensively. The question is, how often will people actually do that?
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
skybrian Link ParentI expect there will be people making AI worms on purpose, which makes them considerably more likely. Perhaps to mine or steal cryptocurrency? What those worms start doing, though, might be...I expect there will be people making AI worms on purpose, which makes them considerably more likely. Perhaps to mine or steal cryptocurrency?
What those worms start doing, though, might be unexpected, even by the creator.
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
skybrian (edited )Link ParentFor once, Anthropic isn’t warning about something they themselves are doing. (I mean, they did experiments, but they’re not releasing anything.) This is about what someone else could build with...For once, Anthropic isn’t warning about something they themselves are doing. (I mean, they did experiments, but they’re not releasing anything.) This is about what someone else could build with open-weights models. Like any other technology, the availability of open weights models has downsides.
“Don’t build it” isn’t a solution when a technologies spread widely enough. How do you get every hacker in the world to agree not to build these things? It’s like saying “let’s not build ransomware.”
To have a chance of depriving AI worms of fuel, AI inference needs to be locked down more than computers have been historically. Particularly poorly-secured Internet-of-things devices.
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
skybrian (edited )LinkFrom the article: [...] [...] [...] [...] So, very slow to start with, but might get faster as hardware supporting AI inference becomes more common outside data centers. Maybe game devices would...From the article:
Our experiments suggest that small AI models may be months away from being capable enough to self-replicate on commercial internet-of-things (IoT) devices, like smart ovens and off-brand Android TV boxes. A replicator like this would be challenging to shut down, since there’s no centralized point to shut off—though it may be slow (with a doubling time of days). Unlike non-AI malware, it could also figure out unfamiliar devices on its own. In our evaluations, a 9B model got inference running on 8 of the 9 hardware types we tested.
[...]
IoT devices are light on memory, but distributed inference as in Petals makes serving our lightweight models feasible. The representative threat model is Kimwolf, a large IoT botnet that infected over two million devices, primarily off-brand Android TVs. Such smart TV boxes, which are readily available for purchase, typically run forks of the Android Open Source Project (AOSP), which their manufacturers don’t add security features to. Typical boxes in this range ship with between 1 and 4 gigabytes of RAM. Assuming 4GB of RAM at 4-bit quantization, this allows for inference of 9B models with 4 or more machines, and inference of 26B models with 10+ machines.
In the demo at the top of this post, we ran Gemma4-26B-A4B across 15 smart TV boxes with 4GB of RAM each. We sharded the model under pipeline parallelism, where each box holds a small fraction of the model’s layers.
[...]
It appears that GLM-5.2 is able to propagate Llama3.1-8B well, which suggests that future small models of the same capability level could also complete the network enumeration, payload delivery, and inference standup steps of the replication process. Our evaluation keeps the cyber-exploit element of the replication trivial (there’s no authentication over the ADB port), which makes this an upper bound on real-world success. Note that past IoT botnets have replicated via means as simple as going through a default list of manufacturer usernames and passwords, as in the case of the Mirai botnet, so real IoT security might not be dramatically more difficult than the trivial step in our evaluation.
[...]
Unlike coding agents, these replicators would be running below the interactive speeds of user-facing chat and coding harnesses. The spread would be slow and persistent, with tokens being trickled out on edge hardware. We can use our achieved speeds on our real smart TVs as a demonstrated baseline for replication speeds. For Gemma4-26B-A4B, unoptimized speed across a 32k context length token window is about 0.3 tok/s, averaged across prefill and decode in our inference setup workload. More details in Appendix C.
[...]
The number of devices infected by the Kimwolf botnet at its peak, reported by Synthient, is somewhere over 2 million (primarily Android TV boxes). In an equivalently-sized infected fleet of TVs serving AI models, if every group of 15 TVs ran a copy of Gemma4-26B-A4B, we would have ~133k copies (“replicas”). A group of TVs like the ones in our demo can serve 2 agents simultaneously at roughly 0.3 tokens per second each, yielding 80k tokens/s across the botnet.
So, very slow to start with, but might get faster as hardware supporting AI inference becomes more common outside data centers. Maybe game devices would have more powerful hardware?
-
AI models may be capable of self-replicating without access to a datacenter
35 votes
From the article:
[...]
[...]
[...]
[...]
[...]
[...]