mmaaz

great q! there's a variety of levers here. for one, it uses newton polytope pruning to prune the monomial basis -- this often helps a lot in practice, especially for sparse polynomials. also, both the lean and python interfaces allow to pass degree bounds in the case of a ratio of SOS, as well as a template for the denominator (e.g., ax^2 + ay^2), which also cuts down on the monomials, as well as possibly introducing affine constraints tying coefficients together. of course, in the positivstellensatz case, you can also specify the degree bound.

I wrote about all these tricks here https://mmaaz.ca/writings/sostactic.html.

and yeah, there is a clli interface for the python backend, the lean interface calls the cli.

Really cool work!

Very cool!

To provide some additional context: the algorithm being used by QEPCAD is cylindrical algebraic decomposition, which has a time complexity 2^2^n (yes, doubly exponential). So, while in theory many problems could be solved by tossing them into CAD, this is often not tractable. This isn’t a knock against CAD: imo it is one of the most fundamental and under-appreciated algorithms and I devoted a big chunk of my PhD thesis to it.

By the way, to my knowledge QEPCAD is essentially the only complete open-source implementation of it. Mathematica also implements it. I wrote one of the few open-source implementations of it, although it does not do quantifier elimination; it only returns the truth of a given statement. https://github.com/mmaaz-git/cad.

this is really brilliant!!

This website showcases our agent, based on Claude, that autonomously infers properties of code and tests them using Hypothesis. Our agent found hundreds of bugs across popular Python libraries, some of which we have since reported and patched! On this website, you can browse all of the bugs it found. You can read the linked paper and code for more information.

Exactly the same here, late night would be my most productive. I don’t know how sustainable this is as I mature lol.

Tbh the code I was writing wasn’t that complex from an engineering perspective. During my PhD I was writing “research code” which is more like writing scripts, not a full blown application or library. The most challenging part was translating the math/algorithms to code. And I would just get into a flow state sometimes and could not stop haha. I had a (bad?) habit during my PhD that whenever I was stuck on a problem I just kept bashing my head against it until I solved it (code or math).

Wow, I feel for you, that sounds really scary. Honestly no, I’ve scarcely changed how I work, except for being more strict about keeping a rigid schedule, forcing myself to take breaks, etc. It’s only my left eye that can’t read, the right eye is totally fine. But I do feel the eye strain come on sooner from relying on one eye.

Hmm not sure what you mean. In the case of MOGAD, it actually attacks the lining of the nerve. The MOG means myelin oligodendrocyte glycoprotein, which is a protein in the myelin sheath.

Good advice. I didn’t have a stroke but a couple months ago I developed blindness in my left eye. It came down to my optic nerve being inflamed. I was later diagnosed with a rare autoimmune condition called MOGAD which “attacks” the optic nerve. Thankfully my vision is approx 95% recovered by now. But I still can’t read, eg code on my laptop, which is scary (my right eye is basically making up for it). And I’m scared of another attack happening. So I’ve been really looking after my health and trying not to do the 12+ hr coding benders I used to do. I appreciate these tips!

Some time ago, I was on a team of researchers collaborating with a hospital to build some ML models for them. I joined the project somewhat late. There was a big fuss over the fact that the hospital servers were not connected to the internet, so the researchers couldn't use GitHub, so they had been stalled for months. I told them that before GitHub there was `git`, and it is already on the servers... I "set up" a git system for them.

I love this as someone who used to work on max-weight matchings and now works on LLMs :)

Fascinating insight into the industry. Thanks for sharing.

Curious what you mean by this. Do you mean like an AlphaEvolve type thing?

The state of the art solvers are the proprietary ones like Gurobi, FICO, Cplex, Mosek, etc. A major contributor to the proprietary "sauce" is in the heuristics they use. For example, all solvers will have a "presolve" phase which attempts to eliminate redundant constraints/variables. There may be some ML they are using behind the scenes to derive these heuristics, I'm not sure, although I know it is a major research area.

Otherwise, the basic underlying algorithms are all the same, as in the textbook: branch-and-bound and so on.

I tried it with a certain conceptual problem in computer algebra (which I’ve had dismal results on GPT o1-preview and o1-mini… sort of a private benchmark) and it spent 2 minutes arguing with itself about what a Python function was called.

I think this is a criticism about the general Python ecosystem, but the article has nothing to do with what other package authors do or security vulnerabilities etc. It converts SAT to “dependency resolution” by creating a bunch of dummy packages and dependencies that map back to the SAT instance. And it’s definitely just for fun, I highly doubt it’s useful except as an exercise in NP-complete reductions :)

On that note, uv, which I found to be orders of magnitudes faster (pip fails to solve even some small SAT/IP instances) uses something called PubGrub

https://docs.astral.sh/uv/reference/resolver-internals/#reso...

Thanks!