State of symbolic shapes branch

[ezyang]

@nunoplopes

Z3 is a dependency for a lot of things these days, including clang’s static analyzer (optional, but a lot of distros ship it enabled).

I definitely think Z3 as an optional dependency is not too hard a sell. The turning point would be if we could make our design substantially simpler if we could assume Z3 was always available; then the calculation would turn to whether or not PyTorch by default has Z3 as a dep, which, enhhhhh. It’s easier for a distro to do it probably.

@nunoplopes

Do you need to give an upper bound for the dimensions? Or do you generate predicates that are valid in the unbounded case?

Nope, everything is fixed dimensionality. So honestly the computations in the smt2 files are not that complicated, but they can be very repetitive because we are just tracing the real shape compute PyTorch does which was not necessarily written in a nice way for symbolic analysis.

@nunoplopes

shape+stride inference, and doesn’t look that complicated (there are min, max, equalities, mul, add, reduce)

A big gap I see from the operators you quote here is floor division (shows up a bit in pooling operations) and modulus (not sure where these come from actually.)

@nunoplopes

I’m happy to help with this stuff (designing, optimizing, whatever) if needed. I’ve experience with symbolic reasoning.

Definitely looking for collabs!

@nunoplopes

Regarding crashes

These are crashing for silly reasons haha. In order:

1. Meta tensors intentionally don’t work with fake tensor (which is what PT2 will do.) In principle they actually should work fine but real world user code doesn’t actually need to optimize code computing on meta tensors, and when we were working on fake tensor it was usually a bug to try to fakeify a meta tensor, soooo yeah. @eellison we probably should fix this eventually
2. You don’t need to explicitly fakeify before calling torch.compile; it does that for you. So what happened here is you said hey PT2 compile this with a tensor subclass input and this doesn’t work. Shouldn’t be an assert though; we should file a bug on this.
3. This is (1) and yeah let’s beef up the medsage
4. This one I think is because inductor and dynamic shapes is busted. So you need to make sure you don’t use inductor. Easiest is to use torch._dynamo.optimize(“aot_eager”) instead of compile

For playing around with simple examples, your best bet is to look at the tests with Symbolic in their class name in test/test_proxy_tensor.py. In particular, most of these call make_fx with tracing mode symbolic. This will give you the smallest slice of the system that is doing something interesting with dynamic shapes.