Adventures in Symbolic Algebra with Model Context Protocol
stephendiehl.com
stephendiehl.com
It's a bit unfortunate that the field is so dominated by extremes of hype and skepticism, both of which aren't particularly helpful to getting problems really solved.
There's only so much money but come on, we're dumping trillions into highly saturated research directions where several already well funded organizations have years worth of a head start. You can't tell me that there's enough money to throw at another dozen OpenAI competitors and another dozen CoPilot competitors but we don't have enough for a handful of alternative paradigms that already show promise but will struggle to grow without funding. These are not only much cheaper investments but much less risky then betting on a scrappy startup being the top dog at their own game.
Anyone have a link to an article exploring Lean plus MCP? EDIT: Here's a recent Arxiv paper: https://arxiv.org/abs/2404.12534v2, the keyword is "neural theorem proving"
I've just remembered: AlphaEvolve showed that LLMs can design their own "learning curricula", to help train themselves to do better at reasoning tasks. I recall these involve the AI suggesting problems that have the right amount of difficulty to be useful to train on.
I'll ramble a tiny bit more: Anybody who learns maths comes to understand that it helps to understand the "guts" of how things work. It helps to see proofs, write proofs, do homework, challenge yourself with puzzles, etc. I wouldn't be surprised if the same thing were true for LLMs. As such, I think having the LLM call out to symbolic solvers could ultimately undermine their intelligence - but using Lean to ensure rigour probably helps.
Long story short, it is great when humans interact with LLMs for imprecise queries, because, we can ascribe meaning to LLM output. But for precise queries, the human, or the LLM needs to speak a narrow interface to another machine.
Precision requires formalism, as what we mean by precise involves symbolism and operational definition. Where the genius of the human brain lies (and which is not yet captured in LLMs) is the insight and understanding of what it means to precisely model a world via symbolism - ie, the place where symbolism originates. As an example, humans operationally and precisely model the shared experience of "space" using the symbolism and theory of euclidean geometry.
A great paper from Nasim Borazjanizadeh and Steven Piantadosi at UC Berkeley for those interested: Reliable Reasoning Beyond Natural Language https://arxiv.org/abs/2407.11373
For anyone digging in who wants to hack on this: arun [at] aloe.inc
> So, we’ve come full circle to symbolic AI!
Case in point, Wolfram Alpha is not much more than an attempt to market Mathematica to lazy and failing college students. If that cost, and localization, can be offloaded to LLMs as the universal front end to technical software, it'd free up SWE resources to focus on core functionality.
If Magma, my favorite math/cryptography tool, had an LLM frontend, I could save time wasted onboarding new cryptographers.
It will regularly use it and reliably when asked to.
Great quote.
On tensor notation: Tensor indices aren't bad (a good notation should guide a calculation and they do) but I can't help but feel they're far too error prone.
What are the alternatives? Penrose diagrams?
this is what the tools response for the mcp server looks like:
{ tools: [ 0: { name: "factor" description: "Factor an integer" inputSchema: { ... } 4 items } ] }
@mcp.tool()
def factor(a: int) -> int:
"""Factor an integer"""
return factor_number(a)
The documentation and source code seem to be:
- (official SDK): https://github.com/modelcontextprotocol/python-sdk/blob/e80c... -> using the function's docstring: https://github.com/modelcontextprotocol/python-sdk/blob/e80c...
- (v2?): https://gofastmcp.com/servers/tools#the-%40tool-decorator and https://github.com/jlowin/fastmcp/blob/998de22a6e76fc8ae323e... -> using the function's docstring: https://github.com/jlowin/fastmcp/blob/998de22a6e76fc8ae323e...
its interesting to see many people come to the same neuro-symbolic conclusion around the same time.
I've found it useful for thought experiments around trading.
I have never used a symbolic algebra system, but came across a problem where I am trying to model a deterministic simulation system. I can write out the computation graph (~20 million equations for final state), but Sympy chokes on seemingly dozens of symbols. No hope of processing the final state or being able to express a simulation state in terms of my desired input variables.
Not sure if my expectations are mismatched with reality, I am hugely bungling the tool, or Sympy has laughable performance vs the more capable commercial options.
It's highly unlikely it's possible, even in theory. Symbolic solvers must explore many known "routes" to expand and simply given equations, without any theoretical guarantees. Even if you found a symbolic solution to your 20M system, it'd have so many terms in it that you'd have to settle for a numerical approximation, just to make sense of them all.
Numerical solvers are of course, a different matter, altogether.
Ah well. Will have to resign myself to raw numbers.
Unfortunately, most problems in physics(field equations), or engineering (Navier Stokes) can't be formulated as satisfiability problems.
The LLM handles the natural language interaction and orchestration, while the computer algebra system does what it does best ... exact symbolic manipulation.
this smells like claude :D