Readit News logoReadit News
ainch commented on Leanstral: Open-source agent for trustworthy coding and formal proof engineering   mistral.ai/news/leanstral... · Posted by u/Poudlardo
elAhmo · 19 hours ago
I don’t know a single person using Mistral models.
ainch · 16 hours ago
That's likely because they're chasing enterprise - see deals with HSBC, ASML, AXA, BNP Paribas etc... Given swelling anti-US sentiment and their status as a French 'national champion', Mistral are probably in a strong position for now regardless of model performance, research quality or consumer uptake.
ainch commented on Leanstral: Open-source agent for trustworthy coding and formal proof engineering   mistral.ai/news/leanstral... · Posted by u/Poudlardo
flowerbreeze · 20 hours ago
They haven't made the chart very clear, but it seems it has configurable passes and at 2 passes it's better than Haiku and Sonnet and at 16 passes starts closing in on Opus although it's not quite there, while consistently being less expensive than Sonnet.
ainch · 17 hours ago
pass@k means that you run the model k times and give it a pass if any of the answers is correct. I guess Lean is one of the few use cases where pass@k actually makes sense, since you can automatically validate correctness.
ainch commented on AirPods Max 2   apple.com/airpods-max/... · Posted by u/ssijak
awad · 18 hours ago
Forgetting all technical benefits: people will always have opinions on headphones and it's rather fascinating that Apple owns the entire market for fashionable ones, despite there being nothing stopping outside players. They specifically acquired Beats for this reason to shore up that base, and so far no one has been able to make a dent in the celebrity or influencer space.
ainch · 17 hours ago
The only other pair I've seen treated that way is Nothing's Headphones - although the (maybe niche) musicians I've seen wearing them lean into y2k aesthetics, where Apple's products are more broadly appealing.
ainch commented on Comparing Python Type Checkers: Typing Spec Conformance   pyrefly.org/blog/typing-c... · Posted by u/ocamoss
Scene_Cast2 · a day ago
Are there any good static (i.e. not runtime) type checkers for arrays and tensors? E.g. "16x64x256 fp16" in numpy, pytorch, jax, cupy, or whatever framework. Would be pretty useful for ML work.
ainch · 17 hours ago
Jaxtyping is the best option currently - despite the name it also works for Torch and other libs. That said, I think it still leaves a lot to be desired. It's runtime-only, so unless you wire it into a typechecker it's only a hint. And, for me, the hints aren't parsed by Intellisense, so you don't see shape hints when calling a function - only when directly reading the function definition.

Personally, I also think the syntax is a little verbose: for a generic shape hint you need something like `Shaped[Array, "m n"]`. But 95% of the time I only really care about the shape "m n". It doesn't sound like much, but I recently tried hinting a codebase with jaxtyping and gave up because it was adding so much visual clutter, without clear benefits.

ainch commented on Comparing Python Type Checkers: Typing Spec Conformance   pyrefly.org/blog/typing-c... · Posted by u/ocamoss
ocamoss · a day ago
We're working on statically checking Jaxtyping annotations in Pyrefly, but it's incomplete and not ready to use yet :)
ainch · 17 hours ago
This would be an insta-switch feature for me! Jaxtyping is a great idea, but the runtime-only aspect kills it for me - I just resort to shape assertions + comments, but it's a pretty poor solution.

A follow-up question: Google's old `tensor_annotations` library (RIP) could statically analyse operations - eg. `reduce_sum(Tensor[Time, Batch], axis=0) -> Tensor[Batch]`. I guess that wouldn't come with static analysis for jaxtyping?

ainch commented on Harold and George Destroy the World   tomclancy.info/harold-and... · Posted by u/tclancy
donatj · 2 days ago
I have genuinely put a lot of thought into this lately. I have the sensation like older media was more expressive and thoughtful, there's at least more... interesting flavors there generally...

I am happy to ponder and willingly accept this is probably just my perception.

I have a couple of theories. The creators of the media are becoming more and more my age. Do they have nothing interesting to say to me as our experience is shared? Is this something experienced by previous generations as their generation took over media, or is our zeitgeist as "digital natives" so newly shared that this is a new experience?

I know people who would blame "ensh*tification" and move on, but I really think that there is more to what is happening.

What I do know is it's exceedingly rare for me to watch a movie or show made after about 2015 and to find myself thinking about it days later. There are of course exceptions.

ainch · 2 days ago
I wonder how much this is just a sampling bias. Older media has been repeatedly filtered over time, so you don't see all the bland, derivative ripoffs that were abundant at the time. Likewise, interesting and forward-thinking work produced today may not be widely appreciated for many years - consider that Van Gogh's work was largely ignored during his lifetime.
ainch commented on Yann LeCun raises $1B to build AI that understands the physical world   wired.com/story/yann-lecu... · Posted by u/helloplanets
visarga · 7 days ago
> Whenever I see claims about AGI being reachable through large language models, it reminds me of the miasma theory of disease.

Whenever I see people think the model architecture matters much, I think they have a magical view of AI. Progress comes from high quality data, the models are good as they are now. Of course you can still improve the models, but you get much more upside from data, or even better - from interactive environments. The path to AGI is not based on pure thinking, it's based on scaling interaction.

To remain in the same miasma theory of disease analogy, if you think architecture is the key, then look at how humans dealt with pandemics... Black Death in the 14th century killed half of Europe, and none could think of the germ theory of disease. Think about it - it was as desperate a situation as it gets, and none had the simple spark to keep hygiene.

The fact is we are also not smart from the brain alone, we are smart from our experience. Interaction and environment are the scaffolds of intelligence, not the model. For example 1B users do more for an AI company than a better model, they act like human in the loop curators of LLM work.

ainch · 7 days ago
It's unintuitive to me that architecture doesn't matter - deep learning models, for all their impressive capabilities, are still deficient compared to human learners as far as generalisation, online learning, representational simplicity and data efficiency are concerned.

Just because RNNs and Transformers both work with enormous datasets doesn't mean that architecture/algorithm is irrelevant, it just suggests that they share underlying primitives. But those primitives may not be the right ones for 'AGI'.

ainch commented on Yann LeCun raises $1B to build AI that understands the physical world   wired.com/story/yann-lecu... · Posted by u/helloplanets
Tenoke · 7 days ago
I think LeCun has been so consistently wrong and boneheaded for basically all of the AI boom, that this is much, much more likely to be bad than good for Europe. Probably one of the worst people to give that much money to that can even raise it in the field.
ainch · 7 days ago
LeCun was stubbornly 'wrong and boneheaded' in the 80s, but turned out to be right. His contention now is that LLMs don't truly understand the physical world - I don't think we know enough yet to say whether he is wrong.
ainch commented on I put my whole life into a single database   howisfelix.today/... · Posted by u/lukakopajtic
gardenhedge · 7 days ago
Isn't this a drop in the ocean? Why would any 'normal' person forgo flying? How much CO2 emissions have 'world leaders' produced going to summits, or Taylor Swift and her fans flaying to concerts or war flights?
ainch · 7 days ago
The general concern around Taylor Swift's emissions has always struck me as shortsighted. Her Eras tour is estimated to have generated around $5bn in economic uplift in the US, at an estimated 10,000 tonnes CO2e for her personal travel. Even if the total footprint is higher, that is thousands of times lower than the emissions intensity of an industry like fast fashion. From an environmental point of view, attending a Taylor Swift show is a much less carbon-intensive way to spend your money than ordering from Temu.
ainch commented on From Noise to Image – interactive guide to diffusion   lighthousesoftware.co.uk/... · Posted by u/simedw
adammarples · 17 days ago
If the prompt is the compass, and represents a point in space, why walk there? Why not just go to that point in image space directly, what would be there? When does the random seed matter if you're aiming at the same point anyway, don't you end up there? Does the prompt vector not exist in the image manifold, or is there some local sampling done to pick images which are more represented in the training data?
ainch · 17 days ago
One way of thinking about diffusion is that you're learning a velocity field from unlikely to likely images in the latent space, and that field changes depending on your conditioning prompt. You start from a known starting point (a noise distribution), and then take small steps following the velocity field, eventually ending up at a stable endpoint (which corresponds to the final image). Because your starting point is a random sample from a noise distribution, if you pick a slightly different starting point (seed), you'll end up at a slightly different endpoint.

You can't jump to the endpoint because you don't know where it is - all you can compute is 'from where I am, which direction should my next step be.' This is also why the results for few-step diffusion are so poor - if you take big jumps over the velocity field you're only going in approximately the right direction, so you won't end up at a properly stable point which corresponds to a "likely" image.

u/ainch

KarmaCake day70May 4, 2025View Original