mmaaz

Joined 3 years ago

Karma

88

Submissions

28

Member since

Mar 13

Anthropic. PhD, University of Toronto. mmaaz.ca @mmaaz_98

View on Hacker News

Recent submissions

Comment · 6 months ago

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.

Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean github.com

14 mmaaz 6 months ago 1 comments

Comment · 9 months ago

Really cool work!

Finding bugs across the Python ecosystem with Claude and property-based testing red.anthropic.com

1 mmaaz 9 months ago 0 comments

Comment · 10 months ago

Comment · 10 months ago

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.

Comment · 11 months ago

this is really brilliant!!

Mathematics is hard for mathematicians to understand too science.org

134 mmaaz 11 months ago 148 comments

Comment · 11 months ago

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.

Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem mmaaz-git.github.io

2 mmaaz 11 months ago 1 comments

Comment · 1 year ago

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

Comment · 1 year ago

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).

Comment · 1 year ago

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.