Hi guy, I am author of Spur , I want to share the Spur solver which is backed by z3 for neuro-symbolic reasoning, combining probabilistic language models with mathematical constraint solving

The ideal here : LLM will give out constranst and translate the constranst to the z3 SMT language, then give out feedback loop between LLM model and neuro-symbolic reasoning to give out better reasioning

looking for feedback and comments from HNs

Thanks and best regards Kevin