Maybe this is what the author is getting at, but if LP solvers are useful tools for editing weights, then Astra access to this methodology might make it more effective at weight editing.
The interpretation here is not so much that an LP can do Astra's work -- after all the Astra prompt was "improve Qwen's math by changing weights" or similar. Instead, it's that with some guidance (eliminate this behavior, preserve that behavior, as expressed through linear constraints) the solver is much more efficient than Astra's trial and error. So essentially the solver would be a way of cutting through all the time consuming stuff and expressing Astra's intent more immediately. And then presumably Astra could iterate on that to a better solution.
The use of an LP solver here is a really cool insight.
I’d really love to see an LLM that can do augmented thinking without being prompted to. External LP or SAT solvers or CLP unifiers or provers, not as “tool calls” structured as JSON structured output but rather in the embedding space in shorthand representations native to token expression that the inference engine dispatches uniquely.
It’s possible to make a differential work through those too in a useful sense, which allows their integration to be at a more fundamental level than post training bolt-on, but that’s not friendly to mass gpu parallel training without some serious work.
A conversation with an engine that thinks with the power of constraint solvers “baked in” instead of having to be brow beaten into approximate truth and iterated millions of times to care to even try to follow through to it. Wow that’s almost all I ever wanted. Here’s my word problem, go do the actual reasoning, hand waive until you’ve got enough expressive power to make an answer but if you can see a formal structure state it natively and let an actual solver spit out the (unification/feasible space/etc) back into token space that the llm picks back up on.