3 ms·
How good are current LLMs at translating problems given as text into something SMT solvers can operate on? Be it MiniZinc, Z3, Smtlib, Python bindings, etc. Any
by jononor 1y ago
How good are current LLMs at translating problems given as text into something SMT solvers can operate on? Be it MiniZinc, Z3, Smtlib, Python bindings, etc. Anyone tried it out?
- Jaxan 1y agoI tried it many months ago and it was garbage. But this was trying smtlib directly. Maybe via the python bindings it works better?
- hwayne 1y agoApparently they're getting very good: https://emschwartz.me/new-life-hack-using-llms-to-generate-constraint-solver-programs-for-personal-logistics-tasks/ https://emschwartz.me/new-life-hack-using-llms-to-generate-c... I try not to use them too much because I want to build the skill of using SMTs directly for now.
- Twirrim 1y agoI've found them to be bad, for the most part. There aren't enough blog posts and examples of code out there for them to leach from. Besides which, I would argue the process of writing proof in the language is integral to building the understanding you need to deal with the results. You'll spot bugs as you're creating the model.