ResiMind

ResiMind — AI エージェントのための検証済みメモリー

エラーを見つけ、洞察を残し、次のタスクを検証済みの有利な状態から始めましょう。

デモを実行 · MCP に接続 · スキルをインストール · チャレンジに挑戦 · 中文

フロンティアロードマップとエビデンス · 外部定理ベンチマークの範囲

main の最新情報（v0.16.0 以降）： メモリーの来歴、期限切れ、転送の監査、ChinaTravel 統合における予約済みの改訂ステップ、実験的な外部 Lean テンプレートコンパイラーを追加しました。最新の同一モデルによる計画結果と開発時の再実行結果は、失敗も含めて公開されています。どちらも計画成功率の向上を示すものではありません。MiniF2F と LeanDojo のスコアはまだ出ていません。

ResiMind は、独立した検証、残差に導かれた自己修正、再利用可能なルールメモリーをつなぐ、オープンソースのニューロシンボリック・エージェントアーキテクチャです。モデル、ルール、またはシンボリックツールがステップを提案し、どの内容を事実として扱うかはドメインチェックが決定します。チェックに失敗すると、次の試行で修正すべき点が示されます。

検証済みの解答は、検証済みのルールになります。 明示的な学習機能は、完了した導出から候補ルールを抽出し、採用を独立して検証したうえで、今後の適用ごとに再チェックします。知識はモデルの外部で増えていき、モデルの重みは変更されません。ローカルルールやツールで対応できる場合、サポート対象の数学処理ルートはモデル呼び出しゼロで実行されます。

形式的なメモリーで、検証済みの条件を組み合わせられるようになりました。 範囲を限定した Lean プランナーは、含意を導入し、検証済みの条件付き補題を適用して、そこから得られる残余サブゴールを別の検証済み補題またはローカル仮定に渡します。型付きプラン全体は Lean によって再コンパイルされます。構造的なマッチングは証明とは見なされません。これは実験的な合成プリミティブであり、MiniF2F や一般的な定理証明における優位性を主張するものではありません。

コアは、専用の検証器を備えたブリッジエンジニアリング、制約付き最適化、カスタマーサポート、オープンエンドの計画にも対応します。適応型代数、ルール学習、5 つの MCP ツールが現在対応しているのは、範囲を限定した有理多項式です。コアの要件は Python 3.10 以降で、実行時依存関係はありません。オプションの MCP には Python 3.11 以降が必要です。

実現したいこと	参照先
既存のエージェントに厳密な代数ツールを追加する	MCP のセットアップ · MCPB をダウンロード
エージェントに範囲を限定した検証・修正ワークフローを教える	修正スキル · インストールガイド
独自のチェック機能を備えたエージェントを構築する	アーキテクチャ · アダプターの仕様
実際に測定された内容を確認する	エビデンス · リリース検証

@1105216375-alt が作成し、最初に公開しました。引用情報 · 変更履歴

エージェント用のツールを評価していますか？まず、このツールで誤答を見抜けることを確かめてください。 9 回の呼び出しによる統合プローブを実行：拒否 → 修正 → 学習 → 想起を、対応範囲外の制御ケースも含めて検証します。モデルキーは不要です。機械可読なケース · ドキュメント一覧

3 分で試す

Python がインストールされている場合：

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

Windows PowerShell では、.venv\Scripts\Activate.ps1 で有効化します。インストール時にビルドツールがダウンロードされる場合があります。デモは API キーなしでオフライン実行できます。python -m resimind とインストール済みの resimind コマンドは、どちらもチェックアウトディレクトリの外で動作します。

最初のデモでは、2 つのトレーニング問題を解き、検証済みの規則を抽出し、固定メモリを保存して再読み込みした後、その規則を新しい係数に適用します。続いて、疎な証明書を使って長い展開を解きます。評価中、固定メモリは変更されません。API 呼び出しは行われません。

デモのコマンド一覧：数学、橋梁、計画、サポート、Lean

別の課題を選んでください。これらのコマンドはオフラインで実行されます。Lean の例には、Lean 4.29.0 ツールチェーンのインストールも必要です。

試す項目	この例で確認できること	コマンド
エピソードをまたいだ学習	固定メモリを保存して再読み込みし、検証済みの規則を転用し、長い疎な展開を検証します	python -m resimind demo --domain lifelong
探索と学習	戦略の優先度を調整し、検証済みのスキーマを抽出して、影響を受ける橋梁のケースだけを再検証します	python -m resimind demo --domain search-learning
目標の進捗	表面的な書き換えを省き、残りの展開目標に取り組み、式が大きくなる有益なステップを許可します	python -m resimind demo --domain progress
ローカルスケジューリング	有用な規則を再利用し、コストの高い代入の前に簡約し、ローカル処理で十分な場合はモデルのコールバックを省きます	python -m resimind demo --domain scheduling
式の増大	4 つの二次因子に対して、基本的な展開と、上限付きの分配および項のまとめを比較します	python -m resimind demo --domain growth-control
Lean の証明フィードバック	実際の未完了の Lean のゴールをもとに新しい戦術を導き、その後、検証済みの規則を再利用します	python -m resimind demo --domain lean
適応型推論	誤ったステップを却下し、戦略を変更して証明を完了し、検証済みの規則を再利用します	python -m resimind demo --domain adaptive
知識の拡張	規則を導出、検証、保存した後、新しいタスクで再利用して再検証します	python -m resimind demo --domain knowledge-growth
汎用アーキテクチャ拡張	依存する残作業を追跡し、固定戦略を順位付けし、再利用可能な規則スキーマを厳密に検証します	python -m examples.general_architecture
オープンエンドな計画	有効な回答は多数ありますが、時間、予算、経路の制約は引き続き適用されます	python -m resimind demo --domain planning
カスタマーサポート	¥259 の返金案は、設定された ¥249 の計算に合いません	python -m resimind demo --domain customer-support
数学	候補が制約に違反していれば、目的関数の値が小さくても役に立ちません。最適性の厳密な証明書を検証します	python -m resimind demo
橋梁工学	力の釣り合いが取れていても、共有橋脚で回転の不整合が隠れていることがあります	python -m resimind demo --domain bridge

監査内容を確認するには、--json を追加します。モデルに独自の計画を立てさせる場合は、DeepSeek を接続してください。

## リカバリーする様子を見てください。そして、うまくいった方法を再利用する様子も見てください。

機能	実際に実行されること
残差に基づくリカバリー	チェックに失敗すると、より小さな局所タスク、検証済みルール、記号的書き換え、またはチェック済みチェックポイントへの復帰が行われることがあります。作業量の上限は維持されます。
検証済みメモリ	候補ルールを独立して承認し、Python ライブラリを永続化して凍結し、再読み込み時に再チェックし、新たに適用するたびに検証します。MCP メモリはプロセス内でのみ有効です。
コンパクトで厳密な計算	共有式と疎な有理数証明書により、明示的なリソース上限内で長い展開を処理します。
任意の証明フィードバック	Lean 4.29.0 が生成された Rat の等式をチェックします。未完了のゴールは、次の提案の指針になります。Lean は MCP ツールとは別です。
残差証明の合成	上限付きの型付きプランで条件を導入し、検証済みの条件付き補題を適用し、残りのサブゴールを解き、1つの Lean 証明としてコンパイルします。

適応型デモでは、意図的に誤った展開を提案して却下し、アプローチを変更して証明を完了し、チェック済みのルールを新しい変数を使うタスクで再利用します。提案はスクリプト化されていますが、検証、状態遷移、承認、再利用は実際に実行されます。

ルールがタスクの境界を越える様子を見る

コアをインストールした後、これらを1つのプロセス内で実行してください（Bash/Zsh。リクエスト形式についてはJSON Lines ガイドを参照してください）。

python -m resimind api <<'JSONL'
{"tool":"verify_identity","arguments":{"lhs":"(x+1)**2","rhs":"x**2+1","variables":["x"]}}
{"tool":"learn_polynomial","arguments":{"expression":"(a+b)**3","variables":["a","b"]}}
{"tool":"learn_polynomial","arguments":{"expression":"(u+v)**3","variables":["u","v"]}}
{"tool":"recall_polynomial","arguments":{"expression":"(2*x+3*y)**3","variables":["x","y"]}}
JSONL

注目点：誤った恒等式は却下され、最初の学習例ではルールが追加されません。2つ目の互換性のある例では、独立してチェックされた3次のスキーマが生成されます。再呼び出しでは、新しい係数に対して1回のルールアクション、モデル呼び出し0回で適用し、その後に厳密な検証を行います。これは再現可能な例であり、一般的な性能を主張するものではありません。レスポンスのフィールド、上限、永続的な Python メモリ →

あなたのエージェントは誤った手順を見つけられますか？

公開されている多項式タスク28件を与えます。正しい計算手順が12件、変更を加えた計算手順が12件、サポート対象外の対照例が4件です。最初に誤りがある手順を特定して修正し、サポートされる範囲を守るよう指示してください。提出内容は独立した SymPy スコアラーがチェックします。

チャレンジに挑戦 → · 検証・修復 Skill をインストール → · 検索可能なタスク例 →

検証できる問題を選ぶ

分野	見つけるべき失敗	実行例
数学	実行不可能な点で目的関数がより小さくなる	厳密な最適性証明書
橋梁工学	力のつり合いは取れているが、橋脚の回転が一致しない	2径間、8つの荷重ケース
自由形式の計画	もっともらしい旅程が厳しい制約に違反する	複数の答えと、チェック済みの実行可能性
カスタマーサポート	返金の提案が設定済みのポリシーに矛盾する	根拠と厳密な算術

自由形式の計画：複数の答えと明示的な制約

依頼：「アートと食事を楽しむ、のんびりした1日を計画してください。静かな場所とコーヒーが好きです。」

指定された必須制約は、09:00～18:00、1人あたり¥300、徒歩は最大45分、異なる立ち寄り先が3か所以上、アートと食事を含めること、出発駅に戻ることです。営業時間、最低滞在時間、すべての移動区間も条件に収まる必要があります。静かさとコーヒーは当初は希望条件ですが、後の実験ではコーヒーを必須条件にします。

同じリクエストでも、妥当な回答は異なります

モデルは、場所、順序、タイミング、移動手段を選べます。ベリファイアーは、1つの固定回答と比較することなく、制約を満たすプラン全体を受け入れます。以下の2つの独立して検証されたオフラインの例は、同じ元のリクエストを満たしています。

実行可能なプラン	費用	徒歩	帰着時刻
ギャラリー → 麺料理店 → 読書室	¥61	22分	13:38
カフェ → 陶芸ワークショップ → 読書室	¥95	8分	13:43

施設と移動手段のデータは架空です。これらの検証で確認できるのは、与えられた入力に基づいて実行可能であることです。楽しさや「最高の1日」は主観的なものです。スケジュールと移動手段の選択を確認する。

制約違反：フィードバックと修正を確認する

オフラインシナリオ	起きること
歩きすぎ	確定済みの事実を変更せずに50分 > 45分を却下します。移動手段を修正すると徒歩は22分に減り、プランは合格します。
雨天のため屋内施設が必要	庭園への訪問を却下します。修正した屋内の旅程は合格します。
帰路の計測情報が不足	移動の根拠情報を未解決のまま保持し、検証済みの旅程は作成されません。

これらは、意図的に不備のある候補を用いた、実行可能なオフラインのフィクスチャです。検証と状態遷移は実際に実行されます。これらの誤りは、稼働中のモデルに起因するものではありません。

**ニューロシンボリックなやり取り：**ニューラルな提案が選択肢を探り、シンボリックな検証が明示された制約を適用し、残りの提案に向けたフィードバックが、修正または根拠の提示が必要な点を伝えます。

要件を変えて、プランの変化を確認する

実際のDeepSeekの実行では、ギャラリー → 麺料理店 → 読書室が提案されました。元の制約を満たしていました。そこで、構造化された要件にコーヒーを必須として追加し、その実際のプランを再提出しました。

手順	起きたこと
古いプランを再検証	**却下：**必須のアクティビティが不足していました。事実は確定されません。
フィードバックをDeepSeekに渡す	モデルへの新たな呼び出し1回で、ギャラリー → 読書室 → カフェが選ばれました。
修正版を独立して検証	受け入れ：¥73、徒歩35分、13:04に帰着。与えられたすべてのハード制約を満たしました。

モデルは可能なプランから選び、ベリファイアーは要件を適用します。架空のカタログでは、カフェで食事とコーヒーの両方を満たせます。この記録された実験では、合成の施設データと移動データを使用しています。検証で確認できるのは、これらの入力に基づいて実行可能であることです。

2つの提案、却下、検証済みの修正版を確認する →

計画ルールの全文と3つすべてのオフラインシナリオ · 実行可能な例 · DeepSeekの実際の監査記録

スタンドアロンのAgentを使う

ResiMindが推論ループを担います。根拠を収集し、提案し、検証し、事実を確定し、残りの義務を再構築します。直接実行するには：

from resimind import Task
from resimind.domains.planning import DOMAIN, build_agent, demo_problem, verified_plan

agent = build_agent(demo_problem())  # Offline; inject complete=your_model for neural proposals.
result = agent.run(Task("day-out", "Plan a relaxed day with art and a meal.", DOMAIN))
run = result.run_result
if run.status == "solved" and run.residual.solved:
    print(verified_plan(result))
else:
    print("Still unresolved:", run.residual.pending)

モデルSDKと外部ワークフローコネクターは任意の統合機能です。このAgentや組み込みのドメインデモにLangGraphをインストールする必要はありません。

カスタマーサポート：返金を約束する前に確認する

お客様から注文品の返品を求められました。記録上、商品の支払い額は ¥249、送料は ¥10 です。この例の販売業者が設定したポリシーでは、この見積もりに送料は含まれません。

状況	エージェントの対応
候補が ¥259 を提案する	金額を却下します。不正確な提案によって、確定済みの事実が変わることはありません。
修正後の候補が ¥249 を提案する	適格性と金額を確認し、構造化された推奨を作成します。
配達日が不明	必要な証拠が揃うまで保留し、完成した返金推奨は提示しません。
依頼が設定済みの期間を超えている	人による確認を推奨し、ポリシーにない例外を作りません。

python -m resimind demo --domain customer-support
python -m resimind demo --domain customer-support --scenario missing-delivery
python -m resimind demo --domain customer-support --scenario expired

これらは、架空の販売業者のルールと合成注文を使ったオフラインのデモです。エージェントは推奨を準備しますが、返金を実行したり、返金が入金されたと主張したりすることはありません。証拠が不足している実行では、タスクが未完了のため、ゼロ以外のコードで終了します。実際の DeepSeek コールバックに接続することもできます。

カスタマーサポートアダプターとライブサンプルを読む → · 実際の DeepSeek 実行：5 回の呼び出し、2 件の却下された提案、検証済みの推奨

数学：解答はまだ証明ではありません

完成した証明から再利用可能な手順を学ぶ： 新しい knowledge-growth Agent は、2 つ目のループを追加します。検証済みの導出 → 候補ルール → 独立した採用審査 → 永続ライブラリ → 今後の提案、という流れです。多項式のデモでは決定的な書き換え文法を使用します。同じゲートを通じて、モデルコールバックから提案を行うこともできます。記録された結果は、オフラインでのルール再利用を測定したものであり、ニューラルネットワークによる数学的発見を示すものではありません。

静的な経過。これは、意図的に実行不可能な候補を含めたオフラインの実行済みフィクスチャです。

連成項、等式制約、非負条件、上限制約を持つ3変数二次関数を最小化します。

$$ \min_x;2x_1^2+x_1x_2+x_2^2+x_3^2-8x_1-3x_2-3x_3, \quad x_1+x_2+x_3=3,\quad x\geq0,\quad x_1\leq1. $$

初期の等式制約下での停留点の提案は (26/15, 1/5, 16/15) です。目的関数の値はより小さいものの、x1 <= 1 に違反するため、検証器はこれを却下します。フィードバック後、エージェントは目的関数の値が −73/8 となる (1, 3/4, 5/4) を提案します。

この答えだけではタスクを完了できません。検証器は、厳密な LDLᵀ 正定値性、実行可能性、KKT 停留条件と相補性、多項式による大域最適性証明書を確認する必要があります。すべての演算で有理数を使用します。オフラインの提案器は活性集合を探索し、検証器はその探索を実行せずに提出された証明書を確認します。

python -m examples.constrained_optimization
python -m examples.constrained_optimization --json

ACCEPT certify_convexity   → positive_definiteness_verified   (2 remaining)
REJECT certify_primal_dual → primal_inequality_violation      (2 remaining)
ACCEPT certify_primal_dual → primal_and_kkt_verified          (1 remaining)
ACCEPT certify_global     → global_gap_identity_verified     (0 remaining)

問題、証明、失敗例を読む →

橋梁工学：連続性によって答えが変わります

曲げ剛性が異なる、24 m + 30 mの2径間連続橋桁を対象に、死荷重、左径間・右径間・両径間への活荷重載荷、および提示された2つの荷重組み合わせを分析します。合計8ケースです。

最初の提案では、径間をそれぞれ独立した単純支持梁として扱っています。力のつり合いは取れていても、正しいとは限りません。共通の橋脚で回転が一致する必要があります。検証器は、修正後の連続梁解を受け入れる前に、梁の方程式と変位の適合条件を確認します。

次にエージェントは、必要な荷重ケースをすべて考慮し、支点反力と正負の曲げモーメントの極値を計算して、ケース包絡線を作成し、提示された曲げモーメントおよび径間中央たわみの制限値と比較する必要があります。載荷パターンを省略すると未解決の義務が残ります。一方、制限値の超過が確認された場合でも、分析自体は有効な完了済み分析です。

python -m examples.continuous_bridge
python -m examples.continuous_bridge --json

結果	値	支配載荷パターン
橋脚上の負曲げモーメント	−7,281.94 kN·m	両径間
径間ABの正曲げモーメント最大値	+3,403.57 kN·m	左径間
径間BCの正曲げモーメント最大値	+6,241.85 kN·m	右径間

構造モデル、方程式、制限値を読む →

どちらのショーケースも、決定論的なオフライン提案器と意図的に無効な候補を使って、実際の検査を実行します。ニューラル提案を使用するには、モデルコールバックを指定してください。これらの実行例が示すのは検証の挙動であり、LLMの精度ではありません。この橋梁は、提示された制限値を用いた合成の等価線梁モデルの例であり、設計基準に基づく評価ではありません。また、中点での検査は、全体のたわみ包絡線ではありません。

含まれるドメインアダプター

アダプター	独立した検査	完了に必要な条件
知識の拡張	多項式証明チェーン、独立した採用、再読み込み、適用を厳密に検査	ルール抽出前にタスクが完了していること。不明な検査結果では知識を採用できません
オープンエンドの計画	予算、時間枠、経路の連続性、訪問範囲、徒歩および屋内の要件	根拠のある移動手段を含む、実行可能な旅程であること。主観的な好みは未検証のままです
カスタマーサポート	対象範囲を限定した注文の証拠、設定済みポリシー、正確な返金計算	推奨内容または人による確認結果が検査済みであること。証拠が不足している場合は未解決のままです
制約付き最適化	厳密な因数分解、実行可能性、KKT条件、多項式証明書	全域最適性を証明する、検証済みの証明書
連続橋	力のつり合い、曲率と適合条件、全荷重ケース、曲げモーメントの極値	ケース包絡線の完成と、提示された制限値との比較
線形方程式	有理数による正規化、解の算出、代入	解なし・恒等式のケースも含め、元の方程式を検査
軸力を受ける棒材	明示された仮定、寸法、公称応力、提示された制限値	応力の検証と比較

solvedは、明示された義務が完了していることを意味します。実行可能な解が存在することや、工学的な制限値を満たすことを自動的に意味するものではありません。各アダプターの対象範囲は限定されています。共有コアによって、これらの検査が明示されます。

ニューロシンボリックな部分の所在

ニューラルによる提案。 ModelProposer は、プロバイダーに依存しない complete(prompt: str) -> str コールバックを受け取ります。実際のモデルは、登録済みのアクションを選択し、根拠の参照を含む主張を提案できます。ドメインビルダーは build_agent(problem, complete=your_complete) を受け付けます。コールバックには現在の状態、未解決の義務、根拠、許可されたアクション、最後の検証フィードバックが渡され、JSON 形式の候補または null が返されます。

シンボリックなチェック。 信頼されたドメインコードが結果を独立して再計算し、参照、前提条件、スコープ、厳密な有理数演算、単位をチェックします。コミット可能な事実は検証器が作成します。モデルは、信頼度スコアや verified フィールドを使って自らに検証を付与することはできません。

残余フィードバック。 残余とは、未達成の目標、未知の事項、ハード制約の集合です。これはコミット済みの事実から再構築されます。却下された場合は状態が維持され、理由が提案器に返されます。前提条件が不足している場合、タスクは未完了のままです。

知識の成長。 LearningAgent は、完了した導出から候補知識を抽出します。KnowledgeLibrary は登録済みのドメイン検証器に採用判定を委ね、再検証と取り消しに対応した保存・再読み込みをサポートし、提案のガイダンスとしてルールを取得します。現在のタスクにも、引き続き検証が適用されます。

形式的な残余の合成。 resimind.integrations.formal.solve は、含意補題と局所仮定を使った、上限付きの連鎖を探索できます。残余プランを記録した後、intro／apply／exact のツリー全体を Lean で再コンパイルします。プランナーは新たな合成プリミティブです。凍結された miniF2F／LeanDojo 評価が存在するまでは、このリポジトリは外部の定理証明ベンチマークにおける結果を主張しません。

再利用可能なアーキテクチャ拡張。 ObligationGraph は依存関係を考慮した残余作業と根拠の無効化を追跡します。StrategyPolicy](docs/general-architecture.md) は凍結された観測に基づき、登録済みの戦略の順位を付けます。また、構造的なルール抽出器は厳密な検証後に限り、適用範囲の狭いスキーマを提案します。これらのヘルパーが事実を承認したり、ドメイン検証器に取って代わったりすることはありません。

モデルはコールバックを介して接続します。このプロジェクトが開発するのは、エージェントの推論、検証、知識の採用です。代数の証明チェッカーには、式とリソースに関する明示的な上限があります。知識の成長とニューロシンボリック実装マップを参照してください。

アーキテクチャ

flowchart LR
    T[Task] --> A[Agent]
    A --> E[Evidence tools]
    A --> P[Model / rule proposer]
    E --> P
    M[Reviewed route memory] --> P
    R[Residual obligations] --> P
    P --> C[Candidate + references]
    C --> V[Independent verifier]
    E --> V
    V -->|accept + binding checks| F[Commit verified facts]
    V -->|reject / defer + feedback| P
    V -->|interrupt| H[Stop and hand off]
    F --> D[Rebuild residual]
    D --> R
    F --> O[Facts + JSON audit trail]
    D -->|task complete| X[Extract derivation certificate]
    X --> K[Independent knowledge admission]
    K -->|verified| L[Persistent knowledge library]
    L -->|retrieve; application rechecked| P

• 主張の前に根拠を用意： 登録済みのツールが各タスクの型付き入力を収集します。
• 状態変更の前に検証： 判定は候補、状態、根拠にひも付けられます。コミット時には参照と競合がアトミックにチェックされます。
• 未完了の作業を明示： 目標、未知の事項、ハード制約は、ドメインアダプターによって解消されるまで可視の状態に保たれます。
• 引き継がれる知識： 完了した導出は独立した採用判定を受け、再読み込み時に再検証され、新たに適用するたびにチェックされます。
• 再利用可能な経路： メモリー内の経路にはレビューと適用可能性の一致が必要です。再利用するステップも、現在の入力に対する検証が必要です。
• 実行の検査可能性： すべての試行について、判定、理由、状態、残余が記録されます。試行回数と停滞の上限によってループを制限します。

独自のアダプターを構築する

次の3つの小さなインターフェースを実装します。

インターフェース	担当する内容
Proposer.propose(...)	モデル、ルール、検索を使って次の候補を提案します
Verifier.verify(...)	現在の入力と候補を独立して確認し、accept、reject、defer、interrupt のいずれかを返します
Domain.rebuild(...)	確定した事実から、残っているすべての義務を再計算します

これらを Agent、Task、登録済みの EvidenceTool オブジェクト、および任意の RouteMemory と組み合わせます。コアはどちらの参照ドメインもインポートしません。独自の計算、シミュレーション、ルールチェッカー、または証明ツールを接続する方法については、アダプターガイドとドメインコントラクトを参照してください。これらの詳細ガイドは現在、中国語で記載されています。neuro-symbolic.mdには、英語の実装マップがあります。

オプションの統合

スタンドアロンの ResiMind Agent は、提案、検証、残余フィードバックを引き続き担当します。アプリケーションに必要な統合のみを追加してください。

統合	目的	追加要件
DeepSeek	任意のドメインビルダーに実際のニューラル提案を提供します。	.[deepseek]
OpenAI Responses	代替モデルコールバックを使用します。	.[openai]
LangGraph	既存のグラフから ResiMind を呼び出し、完了済みまたは未解決の結果をルーティングします。	.[langgraph]

ライブプランニングを実行するには、チェックアウトしたリポジトリから次を実行します。

python -m pip install '.[deepseek]'
# Set DEEPSEEK_API_KEY and DEEPSEEK_MODEL in your local environment first.
python -m examples.open_planning --live --json

ライブ呼び出しではプロバイダー料金が発生する場合があり、未解決のままになることもあります。モデルガイドにはリクエスト予算とタイムアウトが記載されています。ライブリクエストが失敗した場合、オフラインのフォールバックはありません。検証では、実際のライブ記録とシミュレートされたトランスポートテストを区別しています。

LangGraph は任意の外部コネクターです。 ResiMind コアとすべてのドメインアダプターは、LangGraph なしで動作します。既存の LangGraph プロジェクトと統合する場合は、検証サブグラフを使用してください。これは検証済みの事実または未解決の義務を転送するもので、追加のドメイン検証ルールは提供しません。

その他の例とチェック

python -m examples.agent_demo       # task → tool → model callback → verifier
python -m examples.inventory        # independent recomputation and rejection
python -m examples.document_review  # missing evidence stays unresolved
python -m examples.route_memory     # review, applicability, and revocation
python -m pip install -e '.[dev]'
python -m pytest -q

現在のチェックについては、v0.16.0 リリース検証を参照してください。また、過去のチェックについては、v0.14.0 の記録、v0.13.0 の記録、v0.12.1 の記録、v0.12.0 の記録、v0.11.0 の記録、v0.10.0 の記録、v0.9.0 の記録、v0.8.0 の記録、知識成長の開発記録、以前のバージョンの記録を参照してください。

一度導出して、新しいタスクで再利用する

Agent は平方と立方の恒等式を導出し、その証明チェーンを独立した採用審査に提出してから、ライブラリを保存し、検証とともに再読み込みします。新しいタスクではこれらのルールを検索できますが、適用するたびに、現在のタスクのチェックに合格する必要があります。

10タスクのオフライン比較	固定ライブラリ	成長するライブラリ
独立して妥当性が確認された完了タスク	10/10	10/10
転送提案	84	24
確定したタスク間ルールの適用	0	8

転送提案が71.4%減少し、ルールの学習に追加で13件の提案を要しました。両方の条件で同じ決定論的な提案器と予算を使用しています。これは公開済みの開発タスクにおける再利用を測定したものであり、モデルの精度向上や総計算量の削減を測定するものではありません。

ルールの証明、採用、保存、取り消し、再利用の方法 → · 比較を再現する · 検証

モデルではなくエージェントを評価する

モデル、タスク、リソース上限を固定し、完了率、無効な成果物、呼び出し回数、タスク間での再利用を測定します。これらの研究ではタスクや予算が異なるため、結果は個別に報告します。

研究	測定結果	根拠
公開代数修正チャレンジ：28 タスク	決定論的なツールのベースライン：ステータス 28/28、エラー箇所と修正 12/12、誤受理 0/16。公開フィクスチャであり、エージェントのリーダーボードではありません	チャレンジと独立スコアラー
コンパクト計算とメモリ：生成された多項式タスク 240 件	新たなコンパクトのみの条件とメモリ条件は、どちらも 240/240。以前の固定検索は 220/240。想起優先のメモリは、完了率を向上させることなく 48 タスクを直接完了	プロトコルとアブレーション
型付き Lean ゴールと定理メモリ：4 ラウンドで 24 件の反復プローブ	各条件は各ラウンドで 24/24。メモリが増加する条件では、直接再利用が 6→24 に増加。完了率の向上も、安定した時間短縮も実証されていません	形式メモリのパイロット（中文）
条件付き Lean 補題合成：制限付き開発チェーン	intro → apply → exact の完全な計画がカーネルで検査されます。弱い simp のアブレーションではチェーンが必要ですが、強い grind との比較も必須です	合成パイロット（中文）
オフライン統合開発フィクスチャ（モデルなし）	独立採点による完了は 150/150。ルールの再利用により、数学の平均ステップ数が 33.1% 減少。難しい式に対する予備枠のアブレーション：2/8 → 5/8	プロトコル、制限事項、再現方法
同一モデルの代数問題：固定 v1 + 既知ケースを用いた開発版 v2	v1：5/8、6/8、6/8、7/8。v2：5/8、7/8、6/8、7/8。成長条件は、呼び出し回数を増やした再試行と同等	4 条件のプロトコルと結果
ナレッジの成長：オフライン転移タスク 10 件	両条件とも 10/10。提案は 84→24 件に減少し、学習提案が 13 件追加。タスク間での適用が 8 件コミット済み	手法と結果
ChinaTravel：公式タスク 12 件、同一の DeepSeek	公式 ReAct は 0/12、公式 NeSy は 5/12、ReAct + ResiMind は 1/12。ResiMind は無効な計画を出さず、11 タスクを未完了のまま残しました	評価の全容
ローカル修正と制限付き検索：既知タスクの再実行	保守的なデフォルトでは 0/2。明示的な手動の意味注釈を有効にすると 1/2	開発結果
オープンエンドの計画：実際の要件変更	コーヒーを必須にすると古い計画は却下されます。DeepSeek の新たな呼び出しを 1 回行うことで、検証済みの改訂版が生成されます	提案と監査

関連システム（中文）では、このプロジェクトとオーケストレーションフレームワーク、検証主導の推論、ナレッジを蓄積するエージェントを比較しています。

以前の同一モデルのパイロット：プロトコル、コスト、否定的な結果

## 以前に公開したパイロット：同じDeepSeek、4つのエージェント戦略

これらのv1／v2の記録は以前の実装について説明したものであり、v0.8の適応型アダプターのベンチマークではありません。

元の固定済み8タスクの代数パイロット（v1）では、**deepseek-flash**を使用し、モデル設定は同一で、1タスクあたり最大8回の呼び出しとしています。最終出力の採点には、別途、厳密なオラクルを使用します。

エージェント戦略	正しく完了したタスク	提出された無効な回答	転移時のモデル呼び出し数
ReAct形式のベースライン	5/8	3	8
検証して再試行	6/8	0	22
残差推論	6/8	0	22
残差推論＋検証済みの知識成長	7/8	0	20

知識成長の条件では、タスク間のルール適用を実際に3回記録しており、いずれも他の条件でも解けたタスクに対するものです。追加で完了した1タスクではルール適用が確定されていないため、7/8という結果から再利用の因果的な効果を切り分けることはできません。3つのルールの学習には追加で3回の呼び出しが必要で、学習と転移を合わせると23回の呼び出しになります。この実行結果は、全体的なコスト削減を示すものではありません。

これは、手作業で作成した単一のパイロットです。ReAct形式の実装には任意で使えるチェックツールがありましたが、モデルはツールを一度も呼び出しませんでした。この研究は公開されたプロトコルのもとで4つの実装を測定したものであり、最適化されたReActシステムとの比較ランキングでも、一般的な優位性を示す証拠でもありません。

以前の開発時再実行：フィードバックを詳細化し、同じ8ケースを使用。 v1を調査した後、係数の不一致を厳密に示すフィードバックを追加し、既知のタスクを再実行しました。

エージェント戦略	開発版v2での正解数	転移時の呼び出し数
ReAct形式のベースライン	5/8	8
検証して再試行	7/8	17
残差推論	6/8	22
残差推論＋検証済みの知識成長	7/8	20

3つのゲート付き条件はいずれも、今回も無効な回答を一切提出しませんでした。知識成長では引き続き、発見に3回の呼び出しが必要で、タスク間のルール適用を3回記録しています。完了数では検証して再試行と同数で、呼び出し数はそれより多くなります。今回の再実行では、更新したフィードバックによって残差推論または知識成長の完了数は向上しませんでした。これは既知のケースで結果を得た後に行った開発であり、新たな保留ケースでの結果ではありません。v1は変更せずに引き続き利用できます。

プロトコル、タスクごとの結果、トークン、制限事項 → · v1 JSON · 開発版v2 JSON

実装の履歴：v0.9～v0.13

v0.13：検証済みメモリとコンパクトな計算の融合

lifelong math adapterでは、共有式DAG、検証済みの疎な出力、適用可能なルールの検索、明示的な学習／固定メモリを追加しています。python -m resimind demo --domain lifelongをお試しください。240タスクの開発時比較では、コンパクトのみ、メモリ、ポリシーの各アブレーションを含みますが、最先端の定理証明性能を主張するものではありません。

オプトイン方式の検索アダプターが、依存関係を解消した作業、代替経路、検証済みのルール抽象化、固定済みの戦略学習を新たに連携します。ブリッジアダプターは、入力変更後も影響を受けない検証済みのケースを再利用します。ワークフローを実行し、測定された改善、コスト、残された失敗を確認してください。

v0.12の新機能：難しいケースで、上限付きの予備枠を使用

適応型の数学エージェントは通常のローカル作業予算を維持しつつ、通常より大きな記号計算のステップに対して、明示的に累積する予備枠を使用できます。受け入れられた各ステップで支払うのは、推定された超過分のみです。確定するかどうかは引き続き、厳密な等式、目標への進捗、任意のLeanゲートによって決まります。デフォルトの予備枠は0のため、既存の呼び出し元では従来の予算動作が維持されます。

### v0.11 の新機能：目標に向けた推論を維持

等式が正しくても、元の問題が未完了のままになることがあります。数学エージェントは、Lean による証明チェックを実行する前に目標の進捗を確認するようになりました。見た目だけの書き換えには具体的なフィードバックが返され、有用な分解では式が大きくなることがあり、不確かな中間ステップには有限の探索枠が設けられます。コミットされる各ステップには、引き続き厳密な検証と、Lean が有効な場合は Lean による確認が必要です。

見た目だけの書き換えの回復と有用な分解を実行 →

v0.10 の新機能：既知の情報を活用し、必要な場合にモデルを呼び出す

数学アダプターは、モデルにリクエストする前に、検証済みルールの上限付きプレビュー、コンパクション、ローカル展開を比較するようになりました。タスクを完了できるルールは、その式がより大きくても選ばれることがあります。一方、より単純なローカル処理のほうが低コストに見える場合は、条件に一致するルールをスキップできます。選択された各ステップには、引き続き独立した検証が必要で、Lean が有効な場合は Lean による確認も必要です。

ローカル選択、コールバック不要の再利用、明示的なフォールバックを試す →

v0.9 の新機能：数式をコンパクトに保ち、Lean を活用

項の厳密な収集と上限付きのローカル分配により、中間式を小さく保ちます。Lean が有効な場合、受理される各ステップにはカーネルで検証された証明も必要です。未完了の証明は、実際の Lean の目標と診断情報を次の提案に渡します。有限の予算内であれば、戦術や書き換えを変更できます。

式の増大比較と Lean の実フィードバックのデモを実行 →

現在の対象範囲

ResiMind は、実験的な同期型エージェントフレームワークです。ツールの根拠情報はループの前に収集されます。オプションの DeepSeek/OpenAI コールバック、LangGraph 検証サブグラフ、上限付き探索、JSON 永続化に対応した独立検証済みナレッジライブラリが含まれます。上限付き代数アダプターは、導出結果を再利用する学習ループを実装しています。動的なツールのスケジューリング、自動化された複数ロールの計画、汎用 CAS/SMT/証明器コネクター、分散実行は含まれていません。

ドメイン検証器と残差ビルダーは信頼されたアプリケーションコードであり、その正しさによって solved の意味が決まります。根拠情報のラベルは、現実世界の入力を認証するものではありません。ダイジェストは結果の取り違えを検出しますが、悪意のあるプラグインを検出するものではありません。呼び出し側はモデル／ツールのタイムアウトとリソース制限を適用する必要があります。ステップ予算では、ブロックされたコールバックを中断できません。オプションのモデルラッパーは、応答トークン数と API の試行回数に上限を設けますが、総コストの上限や実行全体の厳密な期限を保証するものではありません。

このリポジトリには、Bridge Doctor アプリケーションのワークフローから抽出した、汎用的な実装と合成データの例が含まれています。元のアプリケーションの記録、顧客データ、認証情報、非公開のモデルログは含まれていません。由来、アーキテクチャと信頼境界、セキュリティをご覧ください。

著作者と引用

ResiMind は、作者の Bridge Doctor アプリケーションに基づき、@1105216375-alt が着手して最初に公開しました。元のリポジトリは 1105216375-alt/resimind です。リリースには公開済みバージョンが記録されています。抽出範囲については由来をご覧ください。

ResiMind を利用または紹介する場合は、プロジェクトを引用し、元のリポジトリへのリンクを記載してください。引用例：

1105216375-alt. ResiMind (version 0.16.0), 2026. https://github.com/1105216375-alt/resimind

機械可読な引用メタデータは CITATION.cff に記載されています。引用は歓迎しますが、追加のライセンス条件ではありません。商用利用は MIT License のもとで許可されています。同ライセンスでは、ソフトウェアの複製物または実質的な部分に、著作権表示と許諾表示を保持する必要があります。

新しいドメインアダプター、反例、検証器の失敗テストを歓迎します。CONTRIBUTING.mdをご覧ください。