[cfbolztereick]

All the minimized inefficiencies that are found by my script are already optimizations. They just happen to be rather specific patterns, so they need to be suitably generalized. There's another Regehr etal paper about how to do that automatically: https://dl.acm.org/doi/10.1145/3649837

(llm's aren't involved, it's all based on z3)

I don't plan on implementing something like this for now, I'd rather take the inefficiencies and manually extract optimizations out of them and implement them in PyPy's jit.

[algo_trader]

You are not wrong

AlphaZero-type systems were unable to significantly improve over near-optimal solvers such as z3.

[Zacharias030]

Could you point me to some references to learn about his?