I really appreciate Stephen's mixture of skepticism combined with genuine interest in experimenting with these tools. Most MCP posts I've read have been so much hype I've been left with no clue what MCP actually does. This is the first article I've read on the topic that earnestly makes me want to start messing around with MCP for fun (and makes it clear how to get started).

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.

It's just good writing. Funny, insightful, detailed.

So, we’ve come full circle to symbolic AI! This article essentially suggests that LLMs could be effective translators of our requests to command-line code or input to symbolic AI software, which would then yield precise solutions. However, I feel this approach is overly mechanical, and I don’t believe AGI would be achieved by creating thousands, if not millions, of MCP servers on our machines. This is especially true because MCP lacks scalability, and anyone who has had to send more than three or four function schemas to a language model knows that excessive JSON schema complexity confuses the model and reduces its performance.

We've come back full-circle to precise and "narrow interfaces".

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.

I'm reminded of what happened in the later years of Cyc. They found their logical framework didn't address certain common problems, so they kept adding specialized hard-coded solutions in Lisp. LLMs are headed for AI autumn.

I think the problem here is we keep making promises we can't keep. It causes us to put too many eggs in one bakery, ironically frequently preventing us from filling in those gaps. We'd make much more progress without the railroading.

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.

The article also suggests that you could use a proof-verifier like Lean instead. Using that capability to generate synthetic data on which to train helps too. Very large context windows have been known to help with programming, and should help with mathematical reasoning too. None of this gives you AGI, I suppose, but the important thing is it makes LLMs more reliable at mathematics.

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.

Awesome stuff! We use a similar approach (without MCP) to great effect with Prolog currently and feels like we're only just starting to scratch the surface here.

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

Wonderfully cheeky but also helpfully informative writeup. Also appreciate the hat-tip to all the (as yet) unsolved security issues. Clearly MCP is onto something important, although undoubtedly the standard (or some replacement standard) will mature a fair bit before we're done with it. The flip side to that is, MCPs are probably as 'easier' to experiment with now than they are ever going to be.

  > So, we’ve come full circle to symbolic AI!

Yes, but from a business point of view, NLP based GUIs have been the holy grail of marketing and customer support, especially in STEM apps market.

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.

https://magma.maths.usyd.edu.au/calc/

I was very pleased to discover that Mistral's Le Chat has inbuilt support for python code execution and sympy is importable.

It will regularly use it and reliably when asked to.

I like this type of flow.

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?

Abstract index notation. It's completely different!

It might make more sense to give the model a Jupyter Notebook/code interpreter MCP as a more general case. The environment would have to have sympy, numpy, scipy, matplotlib etc. installed of course

How does the LLM know that it can use the factor tool to factor integers? Just by looking at the string "factor an integer"?

Yes, and I believe this is what the article is referring to when it says “a stochastic black box that communicates through a complex web of JSON schemas attached to docstring annotations”. Specifically, in the function definition:

    @mcp.tool()
    def factor(a: int) -> int:
        """Factor an integer"""
        return factor_number(a)

the decorator `@mcp.tool()` does something behind the scenes to set up the right thing using the docstring of the function.

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...

Yup

this is what the tools response for the mcp server looks like:

{ tools: [ 0: { name: "factor" description: "Factor an integer" inputSchema: { ... } 4 items } ] }

They give it a list of tool commands it can use in the context I believe.

I think this is the proper way to use llms for tasks that require high fidelity. currently im working on binary analysis using llms for natural language and letting ghidra/codeql do the symbolic work. scalability is a massive issue, perhaps the biggest besides fidelity.

its interesting to see many people come to the same neuro-symbolic conclusion around the same time.

bit more fleshed out than what I slopped together last month for this: https://github.com/sielicki/dogfood/blob/master/scripts/mcp-...

I've found it useful for thought experiments around trading.

Damn. I started building exactly the same thing a couple weeks ago.

https://github.com/equationscp/equationscp

> But let's not let a potential rootkit get in the way of a fun weekend experiment.

Great quote.

Tangentially, are there any symbolic algebra systems that can handle millions of equations?

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.

There is no general purpose solver available that can symbolically solve 20M equations, and unfortunately, progress in this field has been excruciatingly slow.

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.

Ahh nuts. I was foolishly optimistic because my experience with SAT solvers has been magical where they can effortlessly chew through huge numbers of constraints. Was thinking that computers are really fast and good at math, surely they can balance a bunch of algebra given some guidance.

Ah well. Will have to resign myself to raw numbers.

I can't recommend SAT solvers enough, the CS community isn't familiar with them and don't appreciate their vast improvements in recent years. If you've the luxury of formulating your 20M system in terms of satisfiability problem, it'd well worth a try.

Unfortunately, most problems in physics(field equations), or engineering (Navier Stokes) can't be formulated as satisfiability problems.

Presumably if you have 20 million equations, they came from a program that's has fewer than 20 million moving parts, like if they came from A x = b where the matrix A has 20M entries. The gist is either exploit structure to make a massive number of small equations or keep the symbols in their "natural" form instead of reducing to scalars, and work with more advanced CAS functionality (like, you might have to learn about noncommutative variations on groebner bases). But also, yes sympy is ultra slow with some things.

Live CEOing Ep 910: Design Review for MCP Server Paclet[0] posted yesterday