Comment by YeGoblynQueenne
10 months ago
SAT solving, verification and model checking, automated theorem proving, planning and scheculing, knowledge representation and reasoning. Those are fields of AI research where LLMs have nothing to offer.
10 months ago
SAT solving, verification and model checking, automated theorem proving, planning and scheculing, knowledge representation and reasoning. Those are fields of AI research where LLMs have nothing to offer.
I can ask Claude 3.7 to write me a program that does SAT solving, theorem proving, or scheduling, and it generally gets it right on the first try.
You could ask me, and I'll copy'n'paste for you Z3 solver, for example, stripping copyrights & rearranging code. Without any understanding how this thing work.
It will be impressive, if Claude was trained on scientific literature about SAT solvers and tutorials about programming language in question, without access to any real SAT solver code. But it is not the case.
Why do you need LLM-generated code when you can take original, which was consumed by LLM?
Or, I could ask another question: Could Claude give you SAT solver which will be 1% more effective than state-of-art in the area? We don't need another mediocre SAT solver.
I have asked Claude to solve scientific problems which I absolutely know are not in its training data, and it has done so successfully. I am not sure why people think it is only regurgitating training data. Don't be lazy and learn how it works--LLMs do generate generalized models, and employ them to solve previously unseen problems.
Would you actually use this program for real-world applications of theorem proving, e.g. validating an integrated circuit design before spending millions on its manufacturing?
I do, yes.
Demonstrate.
It would take you all of 5 seconds to try in Claude yourself. I do this work on a daily basis; I know its value.
4 replies →