Have you tried Zuban? The last time I looked at the options I preferred it for similar reasons to why you like Pyrefly, though I haven't re-evaluated recently.

I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.

Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.

Does this require having a Rocq semantics of LLVM IR? Which one do you use?

No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.

Ah, interesting. I went with Ghidra p-code which seems ok but what I didn't really appreciate going in was how much of the platform API surface you have to describe before you can prove pretty much anything at all.

Is there a reasonable way to run a representative subset myself?

Edit:

> For folks who want to try to repro these findings: I used the pinned v1.0 catalog, the stock just-solve prompt, seed 42, the any-case runner pass policy, and Docker with Python 3.12 and uv.

And https://github.com/gabeorlanski/scb-problems/

Yeah and I started with subsets although I did not find them representative, eg I picked 6 challenges for a subset and fable scored 33%, while on the full challenge it landed closer to 14-15% range

The part II post linked in my top comment has a list of the challenges I used for that.

To run them, just point your model at the paper, it can find the repo, etc and with a key or sub, get it running

Thanks, that's helpful. Do you still have the full data of pass/fail for each test and model? It would be interesting retrospectively to see if there is such a subset.

I built some tools for personal research projects that could potentially help success rates on long dev tasks, empirically it seems to but I've never actually done a quantitative evaluation. SlopCodeBench looks promising for all the reasons you point out in your post.

I think the reason so many people hit this in particular is enabling Sequoia beta channel is the only way to prevent the machine from wanting to upgrade to a newer major release.

... and the updates that come through the beta channel aren't clearly labelled as "beta" or "release candidate".

I've always found that quite strange. Clearly the information is present because they're not signed with the same keys.

The problem is that as far as I know the only way to pin a Mac to an older major version is to put yourself into the beta stream, so people (including me) are getting these not because they want developer access but just because they don't want to upgrade.

The thing that surprises me is that any of the popular harnesses break cache this way. Is it just an artifact of too much LLM code and not enough tests?

One of the main things I've noticed is that several of the techniques are well intentioned for other reasons. For example, when we debug low cache rates with users probably culprit #1 is usually some memory system. Many of those memory systems are trading a stable prefix for the ability to augment the current turns request with some new memory data. For some -- this may be the right trade-off, but the impact is slower responses times due to the extra prefill compute.

So when a memory system promises better LLM performance the other trade-offs aren't necessarily well understood (at the expense of caching).

Features like OMP trying to clean up history to shrink context I think are also well intentioned. But I found these trade-offs interesting hence wanting to share.

if you can, where do you work where this is something you help customers with?

They're the author of the post ;)

https://neuralwatt.com/about

thanks, missed that one

I recall this company now for their unintuitive/abstracted pricing model I have no interest in, but it does make clear why they would be helping customers with cache hit rates, that's going to lower bills on a per-request basis

It's easy to break the cache and there's a number of very valid usecases (mostly context management such as compaction or tool shaking).

Not to mention that it can be very strategic to break context. E.g, after chasing a bug for a while it does make sense to summarise all the approaches that did not work so that you have more context available for newer approaches.

Getting 99% cache hit rates while providing a good user experience is the hard part!

Compaction for sure, but putting git status in the system prompt? Why? (also I'm not sure about common approaches to compaction, they make context window management tricky and cost more generated tokens)

the fun ones are putting the current date in the system prompt, iirc OpenCode has fixed this, such that if your session spans day change, your cache does not bust

Maybe a Chrome bug? It's fine in Safari on an M1.

Also horrifically sluggish on Firefox on Linux.

Weird. Hopefully they converge, I don't miss the days of wildly divergent browser engine behavior.

I use LLMs for ranking and at least for my applications geomean has given me decent scores when the rubric has multiple axes. Raw scores tend to be noisy so either way it helps to take the rough scores and refine by reranking in chunks.

grep is insufficient or we wouldn't have LSP. At minimum you want some kind of structure aware search (for human ergonomics alone, but robots too).

Are you modeling the actual API costs? If you can cut round trips at the end of a long context window you can end up reducing usage even if the total token count is the same.