v0.12.1 — Audited bounded reserve

ResiMind v0.12.1 — audited bounded reserve

A focused patch to the v0.12 bounded local-work reserve:

• multiple matching verified rules now charge the estimate of the rule actually selected;
• cumulative reserve spending is exposed in adaptive statistics and audit events;
• repeated preview denials are deduplicated by state and candidate;
• failed identity/proof gates and rollback paths do not consume reserve;
• the neuro-symbolic Agent architecture and default zero-overflow behavior are unchanged.

Validation: 1,652 tests passed. The release includes a wheel, source distribution, and SHA256 checksums. Detailed model pressure tests remain local and are not presented as benchmark claims.

v0.12.0 — Bounded reserve for hard symbolic steps

ResiMind v0.12.0 — bounded reserve for hard symbolic steps

ResiMind is a neuro-symbolic Agent architecture with residual-driven reasoning, independently checked facts, and reusable verified memory.

This release adds an opt-in cumulative local-work overflow reserve for unusually large polynomial expansions:

• the normal max_local_work=4096 budget stays unchanged;
• max_local_work_overflow can cover several large symbolic steps, charging only each step's estimated excess;
• exact identity, goal-progress, and optional Lean gates still decide every commit;
• failed, unverified, and rolled-back proposals do not consume the reserve;
• the default reserve is 0, preserving existing behavior.

Example:

agent = build_adaptive_learning_agent(
    problem,
    library,
    max_local_work=4096,
    max_local_work_overflow=4096,
)

Validation: 1,649 tests passed. The release includes a public validation record and a wheel, source distribution, and SHA256 checksums. Detailed model pressure tests remain local and are not presented as benchmark claims.

v0.11.0 — Reason Toward the Goal

Reason Toward the Goal

ResiMind v0.11.0 keeps the adaptive mathematics Agent focused on unfinished expansion goals. After verifying an identity, it now assesses whether the proposed step advances the task before spending an optional Lean proof check.

• Act on remaining work. Prompts include the expansion goal, bounded excerpts of unresolved subexpressions and feedback on unhelpful proposals. Cosmetic sign rewrites leave committed state unchanged.
• Allow useful decomposition. Local distribution and power unfolding can increase expression size while moving reasoning forward. A smaller AST alone does not establish progress.
• Explore with a limit. Uncertain intermediate steps have a separate per-task allowance, charged only after the step commits. Proof retries do not charge it twice; state changes and rollback do not refund it.
• Keep outcomes distinct. The audit separates an assessed candidate, an accepted exploratory step, observed goal progress and actual task completion. Every committed step still passes exact verification and Lean when enabled.
• Continue proofs after cancellation. Lean retains every task variable even when one disappears from the expression. A theorem-local linter setting prevents unused bindings from interrupting a valid chain; emitted warnings and errors still fail verification.

python -m resimind demo --domain progress
python -m resimind demo --domain progress --json

This offline demo uses scripted callbacks. It shows a cosmetic rewrite followed by goal-directed correction, and a valid distributive decomposition followed by local expansion. Its zero local-work threshold deliberately activates the callbacks; no model API or Lean compiler is used by this demo.

Validation: 1,645 source tests, all 12 examples, 20 installed-console runs and 35 installed-wheel CLI tests passed. All 37 packaged Python files matched the tested source. Actual Lean 4.29.0 was exercised by the integration tests and the separate Lean demo. Validation · API and examples.

Scope and compatibility: goal_directed=True and max_progress_detours=1 are the defaults. Set goal_directed=False for the previous progress behavior; scheduling and growth controls are independent. The policy is a bounded rational-polynomial heuristic. It can miss useful transformations, including sign rewrites that expose a stored rule, and does not guarantee optimal reasoning or model success.

让推理朝着目标前进：看清剩余问题，保留有用拆解，把探索次数管住。

Wheel, source archive and SHA-256 checksums are attached below.

v0.10.0 — Use What You Know. Call the Model When Needed.

Use What You Know. Call the Model When Needed.

ResiMind v0.10.0 lets checked rules and bounded symbolic tools handle suitable mathematics tasks before requesting a model.

• Compare before committing. Preview several matching rules, compaction and local distribution. Prefer a candidate that finishes the goal; otherwise compare remaining rewrite work and expression growth. A matching rule can be skipped when another local route looks cheaper.
• Keep the model available. Call it when no suitable local candidate remains, estimated work exceeds the configured budget, or proof feedback needs a revised proposal. Exhausted local strategies cannot hide that fallback.
• Observe rule effects. Inspect selection reasons, bounded preview work and each rule's actual outcome and before/after complexity. These observations remain separate from knowledge verification and do not claim measured savings.

Every selected step still passes exact verification and optional Lean checks. State binding, revocation checks and finite model/action/proof budgets remain in place.

python -m resimind demo --domain scheduling
python -m resimind demo --domain scheduling --json

The offline demo compares empty and reloaded learned libraries with a model callback configured. Normal tasks finish without invoking it; a separately labeled zero-local-work case invokes one scripted response to demonstrate fallback. No model API calls are made.

Validation: 1,603 source tests, all 11 examples, 18 installed-console runs, and 33 installed-wheel CLI tests passed. All 35 packaged Python files matched the tested source. Release validation · API and limits.

Compatibility: cost_aware_scheduling=False selects the earlier policy. Growth control is independent. Existing standalone build_learning_agent behavior is unchanged. The new heuristic scheduler currently targets bounded rational polynomials; it is not a universal optimal planner or a trained policy.

会的直接做，需要时再问模型：先比较规则、化简和展开的作用，再决定是否花一次模型调用。规则正确还不够，使用时机同样重要。

Wheel, source archive and SHA-256 checksums are attached below. New quantitative evaluation records remain local.

v0.9.0 — Compact Math. Lean in the Loop.

Compact Math. Lean in the Loop.

ResiMind v0.9.0 keeps polynomial derivations compact and brings real Lean proof feedback into the Agent's next reasoning step.

• Control expression growth. Combine like terms and exact coefficients, then distribute one bounded local product at a time. Every proposed whole-expression change still needs independent verification.
• Use proof failures to choose the next step. The optional Lean 4.29.0 gate sends actual goals and diagnostics back to the proposal loop. An unfinished proof cannot commit a fact; the Agent can request a revised proposal or try a bounded proof retry.
• Reuse checked knowledge. Completed algebraic derivations can enter the existing verified rule library. With Lean enabled, later applications also need a formal equality proof.

Try the two new demos after installing the package:

python -m resimind demo --domain growth-control
python -m resimind demo --domain lean

The first uses no model. The second uses scripted proposals and a real local Lean compiler: rfl fails, its goals reach the next proposal, and grind succeeds. Install Lean 4.29.0 using the integration guide.

Validation: 1,560 source tests, all 10 examples, 16 installed-package CLI runs, and 31 installed-wheel CLI tests passed. See the release validation and design details.

Scope: experimental Agent architecture, bounded rational polynomials, fixed rfl/grind tactics. This is not a new foundation model or a general theorem prover. Rule admission/reload still use exact algebra verification; the Lean gate does not retroactively certify an existing library. No live model benchmark is claimed by these release checks.

发布亮点：复杂表达式分步展开、随展开随合并；真实 Lean 证明失败会带着目标和诊断回到 Agent，指导下一次尝试。验证通过的推导可以继续入库复用，模型权重不变。

Wheel, source archive and SHA-256 checksums are attached below.

v0.8.0 — Self-Correcting Agents with Verified Memory

Self-Correcting Agents. Verified Memory. No Model Retraining.

Catch a bad step. Try another route. Remember a verified solution.

ResiMind v0.8.0 brings verification-guided self-correction and reusable rule memory to a neuro-symbolic mathematics Agent. When a check fails, it can try a local task, a checked rule, a symbolic rewrite or a verified checkpoint. Completed, verified derivations can become rules for the next task.

Verified memory is the persistent rule library: verify before admission, recheck on reload, and verify each new application. This is knowledge growth outside the model; no model weights are retrained. The current adaptive and rule-learning demo supports bounded rational polynomial expansion.

What you can run

• Change strategy after failure. Whole-expression proposals can give way to local subexpression edits, verified rules or primitive symbolic steps. Repeated candidates and failed paths consume finite budgets.
• Keep every step accountable. Polynomial actions bind to the current expression and state; only accepted verification results become facts. Returning to a checkpoint adds a checked transition and preserves the audit.
• Build a reusable rule library. Completed derivations can become independently checked rules. Save, reload and reverify the library; check each application on the next task.
• Bring your own model. The core remains provider independent and has no runtime dependencies. The new adapter can also run with symbolic strategies alone.

Try it without an API key

Download the attached wheel, then run:

python -m pip install resimind-0.8.0-py3-none-any.whl
python -m resimind demo --domain adaptive

The demo deliberately proposes a wrong expansion, verifies a local edit, completes the proof with symbolic steps, then saves and reuses its checked rule on a new-variable task. Model responses in this demo are scripted offline fixtures; the verification and recovery paths really execute.

Adaptive API and strategy behavior · 中文项目介绍 · Full changelog

Scope and validation

This is an experimental Agent architecture release. The concrete adaptive adapter supports bounded rational polynomial expansion. The shared core also has planning, customer-support, optimization and bridge examples with domain-specific checks. Lean integration is future work.

Release checks cover the complete regression suite, runnable examples and the installed wheel. See the release validation record for exact results. Earlier published model pilots remain labeled as historical; new private evaluation results and their raw model traces are not part of this release. This release makes no frontier-ranking or universal-correctness claim.

中文：会纠错、能积累知识的 AI Agent，无需重训模型。 发现错步，换条路走；验证过的解法，留给下一题。当前自适应数学与规则学习示例针对有界有理多项式，Lean 留到后续版本。

Created and originally published by @1105216375-alt. MIT licensed; citation metadata is included.

v0.7.0: Open-ended plans, independently checked

ResiMind now includes open-ended day planning: a model freely chooses venues, their order, times, and transport, while an independent verifier checks the resulting itinerary. Different valid plans are accepted; subjective explanations remain outside the checked facts.

The home pages now lead with the standalone ResiMind Agent. LangGraph is clearly grouped under optional integrations and is not required by the core, domain adapters, or offline demos.

• Try python -m resimind demo --domain planning after installation. Its labeled offline fixture rejects 50 minutes of walking against a 45-minute limit, then checks a revised itinerary.
• Use --scenario rain for indoor-venue requirements and --scenario missing-travel for unresolved return data. Missing information cannot become a free, instantaneous journey.
• The live entry point is python -m examples.open_planning --live --model YOUR_DEEPSEEK_MODEL --json from a checkout. The core reasoning loop is unchanged.

Actual live experiments: ordinary and rainy-day requests each passed on the first model call. Separately, coffee was changed from a preference to a hard requirement. The actual older plan was then rejected, and one new DeepSeek call revised “gallery → noodles → reading room” into “gallery → reading room → cafe.” The revised plan cost ¥73, included 35 minutes of walking, and returned at 13:04 under the supplied ¥300 / 45-minute / 18:00 constraints. The reused candidate is explicitly identified in the audit and is not counted as a new API response.

660 tests passed, both against source and the installed wheel. A core-only install ran without LangGraph or a model SDK. Tests accept three distinct itineraries under the same request and cover complete route accounting, timing, costs, missing selected data, provenance, and state tampering. All seven archived live audits reproduce through offline verification replay.

Open planning guide · Live experiments and provenance · 中文首页 · Validation

The venue catalog, prices, traffic durations, and weather flag are fictional inputs. Checked feasibility is not proof of optimality, enjoyment, or real-world availability. These three live experiments are smoke tests, not a comparative model benchmark. No booking or messaging is performed. Remote CI remains a template.

Experimental release, MIT licensed, with a dependency-free core. Project creator and original publisher: @1105216375-alt. Wheel, source archive, and SHA256 checksums are attached.

v0.6.0: Customer support that checks before it promises

ResiMind now includes an everyday customer-support workflow alongside mathematics and bridge engineering. A proposed refund must agree with the supplied order evidence and configured merchant policy before it becomes a checked recommendation.

• Try python -m resimind demo --domain customer-support after installation. The default offline case rejects a ¥259 quote that incorrectly includes shipping, then verifies the ¥249 item amount.
• Try --scenario missing-delivery: missing evidence remains pending, with no completed recommendation. --scenario expired completes a human-review recommendation with no refund amount.
• Use python -m examples.customer_support --live --model YOUR_DEEPSEEK_MODEL --json from a checkout for real model proposals. No offline fallback is used.
• The existing Agent runtime and LangGraph verification gate support the new domain unchanged. Recommendations never execute a refund, send a customer message, or claim that a payment has arrived.

A real deepseek-flash smoke run completed in 5 API calls. Two intermediate proposals were rejected for missing order-snapshot references; the model corrected them before the final ¥249 recommendation passed. The complete trace is published. This is one synthetic-case smoke test, not an accuracy benchmark.

558 tests passed, against both source and the installed wheel. The core-only package ran all three support scenarios outside the checkout without third-party runtime dependencies. All four archived live runs reproduce through offline verifier replay. Remote CI remains a template.

Customer-support guide · 真实客服运行记录 · 中文首页 · Validation

The 14-day window and shipping exclusion are fictional merchant rules, not consumer-law claims. ID matching checks supplied record consistency; real customer authentication, authorization, policy selection, and payment execution belong to the host application.

Experimental release. Core remains dependency-free and MIT licensed. Project creator and original publisher: @1105216375-alt. Wheel, source archive, and SHA256 checksums are attached.

v0.5.0: Verify your AI agent with DeepSeek + LangGraph

ResiMind adds independently checked facts and explicit unfinished work to an AI Agent workflow. This release makes the architecture easier to try and connects real DeepSeek proposals to a LangGraph verification subgraph.

• Start offline with python -m resimind demo; the installed command also works outside the checkout. Optimization and bridge cases include JSON audits.
• Connect DeepSeek Chat Completions or OpenAI Responses through optional callbacks, with explicit models, bounded API attempts, timeouts, token accounting, and no offline fallback.
• Embed the LangGraph subgraph: completed verification exposes committed facts; unfinished work routes to needs_review without a completed report.
• See the actual rejection/correction trace in the bilingual README animation. The animation is an explicitly labeled offline fixture.
• Inspect all three live DeepSeek preparation runs. The final deepseek-flash run completed the exact optimization proof in 4 calls; two earlier deepseek-chat attempts remained unfinished. These are smoke runs on one synthetic problem, not an accuracy benchmark.

Validation: 454 tests passed, both against source and the installed wheel. A separate core-only installation ran both domains outside the checkout with no third-party runtime dependencies. Archived live candidates reproduce under the release verifier. OpenAI was tested with its real SDK and simulated HTTP responses; no live OpenAI call was made. Remote CI remains a documented template, not an active workflow.

Quickstart · 中文 · Live model guide · LangGraph · Full validation · Live audits

Experimental release. Domain-specific verifiers have explicit scopes; they do not validate arbitrary prose. The bridge inputs and limits are synthetic. Core remains dependency-free and MIT licensed. Project creator and original publisher: @1105216375-alt.

Install the attached wheel for the core, or use the source archive for examples and optional integrations. SHA256 checksums are attached.

ResiMind v0.4.0 — Exact proofs and continuous bridges

ResiMind v0.4.0 — Proofs and bridges

Two substantive Agent showcases now lead the project: exact constrained optimization with a global proof certificate, and a statically indeterminate continuous bridge with complete load-case envelopes.

Exact mathematics

A coupled three-variable quadratic program with equality, nonnegativity and upper-bound constraints. The Agent rejects an infeasible stationary point, checks primal and dual witnesses atomically, and proves the unique optimum (1, 3/4, 5/4) with objective -73/8 using an exact polynomial gap identity. A feasible but nonoptimal proposal cannot lock the run to a bad witness.

Continuous bridge

A synthetic 24 m + 30 m bridge girder with unequal stiffness and eight combination/pattern cases. The verifier rejects a simply-supported-span approximation because it violates pier rotation continuity. It checks beam equations, support conditions and equilibrium, then completes bending-moment and midpoint-deflection envelopes and supplied-limit comparisons. Partial live loading governs the span sagging maxima.

Includes bilingual landing pages, two reproducible figures, readable CLI traces, JSON audit output, reusable domain inputs, and provider-neutral model callbacks.

Validation: 400 tests pass locally on Python 3.12, including an independent virtual-work oracle for the bridge. The installed wheel passes the same suite; all eight examples and both new JSON modes run successfully. The optional GitHub Actions configuration remains a template; hosted CI is not enabled.

python -m examples.constrained_optimization
python -m examples.continuous_bridge

The package still has zero runtime dependencies and uses the MIT license. These deterministic offline demonstrations make no claim about neural-model performance. The bridge is a synthetic line-beam model, not a code-compliance assessment; it checks fixed midspan deflections, not global displacement extrema or moving-vehicle envelopes.

中文

新增更完整的数学与桥梁案例，并放到首页：约束二次优化包含 KKT 与全局最优性证明；两跨连续梁桥包含八工况、反力、正负弯矩极值和跨中挠度包络。两个案例都展示真实的“拒绝错误候选—读取反馈—修正—核验完成”过程。

400 项本地测试通过；附源码、安装包、双语说明与结果图。