ResiMind — Agents That Verify, Remember, and Reuse
Give your agent a checked answer—and a rule it can reuse.
ResiMind is a standalone, open-source neuro-symbolic Agent architecture for verification-guided self-correction and reusable rule memory. Rules, symbolic tools and your model can propose steps. Independent code checks them. The residual tracks what remains to be solved and guides the next attempt.
Verified memory · Residual-guided recovery · Learning without model retraining
The adaptive math Agent can switch strategies after a failed check and turn completed, verified derivations into rules for future tasks. Here, verified memory means a persistent rule library: verify before admission, recheck on reload, and verify each new application. Knowledge grows outside the model; its weights stay unchanged.
The current adaptive and rule-learning demo supports bounded rational polynomial expansion. The same Agent core also runs planning, customer support, optimization and bridge examples with domain-specific checks.
Bring your own model · Python 3.10+ core · Optional MCP (3.11+) · MIT · v0.14.0 / Experimental
New: let another Agent use ResiMind as a tool. Check a model's polynomial identity, return exact sparse expansions, explicitly learn checked rules, and recall them on a new expression. Five local tools, structured evidence, zero model calls. Connect over MCP or try the JSON CLI →
| Looking for… | Start here |
|---|---|
| An MCP math server to check an LLM's algebra | Verify / expand tools |
| Agent memory that checks a rule before reuse | Learn → recall, runnable example |
| An Agent architecture for engineering and constrained decisions | Bridge · Domain examples |
New in v0.13: learn a checked rule, save it, reload it, and use it on a new problem. A compact exact tool handles long polynomial expansions; a learned route preference can choose computation when it costs less than recall.
240/240 generated polynomial tasks, zero model calls, compared with 220/240 for the previous frozen search implementation. Compact-only also solves 240/240; memory demonstrates transfer on 48 tasks with recall-first routing, without adding a completion-rate gain here. Protocol, ablations and limits →
中文 · Quick start · Knowledge growth · Open-ended case · Evidence · Architecture
Created and originally published by @1105216375-alt. Original repository · Citation
Watch it recover. Then watch it reuse what worked.
| Capability | What actually happens |
|---|---|
| Self-correction | A failed check can trigger a smaller local task, a verified rule, a symbolic rewrite, or a checked checkpoint return. |
| Verified memory | A completed proof can become a stored rule, with conditions and provenance, independently checked on admission and reload. |
| Learning without retraining | A new task can retrieve and execute the rule, checking its application again. Model weights stay unchanged. |
Each new candidate is checked before becoming a fact; retry and action budgets remain bounded across strategy changes.
Propose → check → diagnose what remains → change strategy → check again
↓
completed proof → admit rule → reuse and recheck
Try the offline recovery demo: a deliberately wrong expansion is rejected, a local edit passes, symbolic steps finish the proof, and its checked rule solves a new-variable task in one application. The fixture is scripted; the verification, state transitions, rule admission and reuse actually execute.
Current scope: the adaptive adapter handles bounded rational polynomial expansion. Other domains share the Agent core and use their own checks. An optional Lean 4.29.0 backend checks generated equalities over Rat and feeds unfinished proof goals back into the next proposal.
Run the learning-and-reuse demo → · Release validation · Changelog
v0.13: verified memory meets compact computation
The lifelong math adapter adds shared expression DAGs,
verified sparse output, applicable-rule retrieval, and explicit train/freeze
memory. Try python -m resimind demo --domain lifelong. A 240-task development
comparison includes compact-only, memory and policy ablations; it does not
claim frontier theorem-proving performance.
An opt-in search adapter now connects dependency-ready work, alternative routes, checked rule abstraction and frozen strategy learning. A bridge adapter reuses unaffected checked cases after inputs change. Run the workflow and read the measured gains, costs and remaining failures.
New in v0.12: let hard cases spend a bounded reserve
The adaptive math Agent keeps its normal local-work budget, then can spend an explicit cumulative overflow reserve on unusually large symbolic steps. Each accepted step pays only its estimated excess; exact identity, goal progress and optional Lean gates still decide whether it commits. The default reserve is zero, so existing callers keep the previous budget behavior.
New in v0.11: keep reasoning aimed at the goal
A correct equality can leave the original problem unfinished. The math Agent now inspects goal progress before spending a Lean proof check: cosmetic rewrites receive concrete feedback, useful decomposition can grow the expression, and uncertain intermediate steps have a finite exploration allowance. Every committed step still needs exact verification and Lean when enabled.
Run cosmetic recovery and useful decomposition →
New in v0.10: use what you know; call the model when needed
The math adapter now compares bounded previews of verified rules, compaction and local expansion before requesting a model. A rule that closes the task can win even if its expression is larger; a matching rule can be skipped when simpler local work looks cheaper. Every selected step still needs independent verification, including Lean when enabled.
Try local selection, zero-callback reuse and explicit fallback →
New in v0.9: compact math, with Lean in the loop
Keep intermediate expressions small with exact term collection and bounded local distribution. When Lean is enabled, each accepted step also needs a kernel-checked proof. An unfinished proof supplies the next proposal with its actual Lean goal and diagnostics; it can change tactic or rewrite, within finite budgets.
Run the growth comparison and real Lean feedback demos →
Try it in three minutes
With Python installed:
git clone https://github.com/1105216375-alt/resimind.git
cd resimind
python -m venv .venv
source .venv/bin/activate
python -m pip install .
python -m resimind demo --domain lifelong
On Windows PowerShell, activate with .venv\Scripts\Activate.ps1. Installation may download build tools. The demo runs offline, without an API key; both python -m resimind and the installed resimind command work outside the checkout.
The first demo solves two training problems, extracts a checked rule, saves and reloads frozen memory, and transfers that rule to new coefficients. It then solves a long expansion using a sparse certificate. The frozen memory stays unchanged throughout evaluation. No API calls are made.
Choose a different challenge. These commands run offline; the Lean example additionally requires an installed Lean 4.29.0 toolchain:
| Try | What the example makes visible | Command |
|---|---|---|
| Learning across episodes | Save and reload frozen memory, transfer a checked rule, and verify a long sparse expansion | python -m resimind demo --domain lifelong |
| Search and learning | Fit strategy preferences, extract checked schemas, and recheck only affected bridge cases | python -m resimind demo --domain search-learning |
| Goal progress | Skip a cosmetic rewrite, act on remaining expansion goals, and allow a useful step with a larger expression | python -m resimind demo --domain progress |
| Local scheduling | Reuse a useful rule, simplify before an expensive substitution, and skip model callbacks when local work suffices | python -m resimind demo --domain scheduling |
| Expression growth | Compare primitive expansion with bounded distribution and term collection on four quadratic factors | python -m resimind demo --domain growth-control |
| Lean proof feedback | A real unfinished Lean goal drives a new tactic, then a checked rule is reused | python -m resimind demo --domain lean |
| Adaptive reasoning | Reject a wrong step, change strategy, finish a proof and reuse its checked rule | python -m resimind demo --domain adaptive |
| Knowledge growth | Derive a rule, verify and store it, then reuse and recheck it on a new task | python -m resimind demo --domain knowledge-growth |
| [General architecture exte |