Interesting, I'm not familiar with that paper, but I guess the performance gain comes from raising the abstraction level (hiding solver boilerplate). PTC-Lisp could achieve the same thing by defining constraint-building functions as tools, and the LLM writes high-level PTC-Lisp that calls a solver. In fact, Lisp has a natural advantage here: instead of building a separate DSL with its own compiler (as I guess Logic.py did), Lisp can extend itself with macros — code is data, data is code - however this is not impl. yet in ptc-lisp.