strongly-typed

A framing from that podcast that helped me better understand the role of Bonsai is that it's really a framework for building incremental distributed state machines.

Lean is such a wonderful language. So hyped by these releases.

Lean is such a wonderful language. So hyped by these releases.

I’m not following. If I run an agent on ollama locally, it’s not in the cloud. I don’t see what cloud has anything to do with the argument.

As to your other point about anything you include in the prompt can and will be ignored. Yes, I agree. You could draw an analogy to how a teacher assigns an in-class reading assignment and follows it up with a reading comprehension quiz. If your mind wanders during the reading you may come to find that you will fail the quiz because “anything you include in the prompt can and will be ignored”. Therefore, the quiz result serves the purpose of an evaluation.

No no, that’s not what I’m saying. The fact that the data is stored in files is incidental. It could be in a database, in a knowledge graph, derived from so other data Regardless of where it is, something should know to include it in the context, but only when it’s relevant.

So for instance you could start by trying to classify the prompt in some way. If you use an LLM for this, you might need to get it to return a machine parsable data format. Then your harness can pattern match on the classification and use it to enrich the prompt with additional context. The challenge would be in determining how exactly you want to go about this, balancing tradeoffs such as accuracy, cost, time, etc..

For the classification step you might begin with something like "Determine whether the following prompt is a QUESTION or a STATEMENT. Respond using only one of the two words. Prompt: $PROMPT"

You could have multiple back-and-forths like this and at each round you gain more information about the prompt, and you can use that information to determine further classifications and/or context to include.

That's the million dollar question. Maybe have systems of agents that all validate each other's work? Maybe something needs to be done at the harness level? I don't suppose that we could realistically expect 100% accuracy, but if we take 100% to be the upper limit, we could build systems that get us closer to that ideal.

To me it sounds like a tooling problem. OP seems to be trying to use probabilistic text systems as if they enforce rules, but rule enforcement should really live outside the model. My sense is that there was a failure to verify the agent's intent.

The tooling that invokes the model should really define some kind of guardrails. I feel like there's an analogy to be had here with the difference between an untyped program and a typed program. The typed program has external guardrails that get checked by an external system (the compiler's type checker).

Doesn’t matter if the recruiter doesn’t call you back because you’re not a 1000x engineer.

Wait, what does NFTs have to do with RAG?

You know you could just define the verified specs in lean and if performance is a problem, use the lean spec to extract an interface and tests for a more performant language like rust. You could at least in theory use Lean as an orchestrator of verified interfaces.

Strong agree. OCaml's compiler is sofa king good at catching and preventing real bugs that the agents accidentally introduce here and there. It's the same as with humans, except the agents don't complain about the bullshit reasons humans don't like OCaml. They just crank through and produce high quality output.