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
Show HN: Spur solver – Z3-backed model-finder solved values for coding agent
github.com