Curate-Ipsum

Curate-Ipsum

信念改訂による検証済みコード合成を実現する、グラフスペクトルベースの MCP サーバー

Curate-Ipsum は、LLM が生成したコード（高速で、もっともらしいものの、未検証）と、形式検証済みのパッチ（低速で、正確かつ信頼できるもの）の間のギャップを埋めます。ミューテーションテストを、到達可能性解析、シンボリック実行、自動テスト生成を支える、堅牢で自己修復するコードベースメタデータを維持するための大規模なシステムの一要素として扱います。

インストール

# PyPI
pip install curate-ipsum

# or with uv
uv pip install curate-ipsum

# Docker (includes baked-in embedding model)
docker pull ghcr.io/egoughnour/curate-ipsum:latest

Claude Desktop / MCP クライアント

claude_desktop_config.json に追加します：

{
  "mcpServers": {
    "curate-ipsum": {
      "command": "uvx",
      "args": ["curate-ipsum"]
    }
  }
}

または Docker を使用します（埋め込みモデルが事前に読み込まれており、Python は不要です）：

{
  "mcpServers": {
    "curate-ipsum": {
      "command": "docker",
      "args": ["run", "-i", "--rm", "ghcr.io/egoughnour/curate-ipsum:latest"]
    }
  }
}

MCP ツール

Curate-Ipsum は、MCP の stdio トランスポート経由で 6 つのグループに整理された 30 個のツールを公開します：

テスト — run_unit_tests、run_integration_tests、run_mutation_tests、get_run_history、get_region_metrics、detect_frameworks、parse_region、check_region_relationship、create_region

信念改訂 — add_assertion、contract_assertion、revise_theory、get_entrenchment、list_assertions、get_theory_snapshot、store_evidence、get_provenance、why_believe、belief_stability

ロールバックと失敗 — rollback_to、undo_last_operations、analyze_failure、list_world_history

グラフスペクトル — extract_call_graph、compute_partitioning、query_reachability、get_hierarchy、find_function_partition、incremental_update、persistent_graph_stats、graph_query

検証 — verify_property（Z3/angr）、verify_with_orchestrator（CEGAR の予算段階的増加）、list_verification_backends

合成と RAG — synthesize_patch（CEGIS + 遺伝的アルゴリズム + LLM）、synthesis_status、cancel_synthesis、list_synthesis_runs、rag_index_nodes、rag_search、rag_stats

現在の状況

最終更新：2026-02-08

コンポーネント	状況
マルチフレームワーク解析（5 フレームワーク）	完了
グラフ基盤（Spectral/Kameda）	完了
信念改訂エンジン（AGM/Provenance）	完了
合成ループ（CEGIS/Genetic）	完了
検証バックエンド（Z3/angr）	完了
グラフ永続化（SQLite/Kuzu）	完了
RAG / セマンティック検索（Chroma）	完了

課題

LLM が生成するコードは、次のようなものです：

• ✅ 構文的に有効（通常）
• ✅ 統計的にもっともらしい
• ❌ 意味的に正しい（場合による）
• ❌ 型安全（偶然に頼る）
• ❌ 形式検証済み（まったくない）

現在のアプローチは、LLM の出力を無条件に信頼するか、完全に拒否するかのどちらかです。どちらも最適ではありません。

ソリューション

LLM は低コストの候補生成に使用し、その後、形式的な保証を実現するために計算リソースを投入します。

LLM Candidates (k samples)
        ↓
   Seed Population
        ↓
┌───────────────────────────┐
│  CEGIS + CEGAR + Genetic  │  ← Verification loop
│  + Belief Revision        │
└───────────────────────────┘
        ↓
  Strongly Typed Patch
  (with proof certificate)

最先端技術との主な差別化要因

従来のミューテーションテストとの比較（Stryker、mutmut、cosmic-ray）

従来	Curate-Ipsum
単一のツール、単一の言語	複数フレームワークのオーケストレーション
フラットなファイル単位の解析	階層的なグラフスペクトル分解
出力はミューテーションスコア	合成への入力としてミューテーションテストを使用
形式的検証なし	CEGIS/CEGAR 検証ループ
手動でのテスト作成	パッチの自動生成

LLM によるコード生成との比較（Copilot、Claude、GPT）

LLM のみ	Curate-Ipsum
モデルの出力を信頼	モデルの出力を検証
単一サンプル、またはベスト・オブ・k	集団ベースの改善
形式的な保証なし	証明書
ステートレスな生成	プロヴェナンスを伴う信念改訂
もっともらしいコード	正しさが証明されたコード

プログラム合成との比較（Sketch、Rosette、SyGuS）

従来の合成	Curate-Ipsum
手書きのスケッチ	LLM が生成する候補
コールドスタート検索	LLM の集団からのウォームスタート
実行をまたいだ学習なし	全域化理論が知識を蓄積
単一の仕様	複数フレームワークにまたがる暗黙的領域

シンボリック実行との比較（KLEE、S2E）

シンボリック実行	Curate-Ipsum
パス探索のみ	合成と統合
ブール制約の求解	数学的な再定式化（SymPy）
単一ツールによる解析	グラフ DB + SMT + ミューテーションのオーケストレーション
コード生成なし	検証済みパッチを生成

新たな貢献

1. グラフスペクトルによるコード分解

   • 最適な到達可能性を実現するフィードラー・ベクトル分割
   • 階層的な SCC 凝縮
   • 平面部分グラフの特定 → O(1) の Kameda クエリ
   • クリストフェル記法による部分グラフを原子的な非平面単位として扱う

2. 合成のための信念改訂

   • AGM 準拠の理論改訂
   • 最小限の縮小を実現するエントレンチメント順序
   • 失敗モード分析のためのプロヴェナンス DAG
   • ロールバックにより妥当性を向上（失敗によって普遍モデルを洗練）

3. 暗黙的領域の検出

   • スペクトル異常からテストが不十分なコードを特定
   • フレームワーク間でのミューテーション耐性から重要な領域を特定
   • 過去の変更可能性をパーティション最適化に活用

4. 数学的な制約の再定式化

   • ブール制約の難問 → 微分／根の探索
   • SymPy によるパス条件のエンコーディング
   • SMT と数値解法のハイブリッド

アーキテクチャ

flowchart TB
    subgraph MCP["MCP Interface"]
        direction TB

        subgraph Sources["Analysis Sources"]
            direction LR
            MUT["🧬 Mutation<br/>Orchestrator<br/><small>Stryker<br/>mutmut<br/>cosmic-ray</small>"]
            SYM["🔬 Symbolic<br/>Execution<br/><small>KLEE · Z3<br/>SymPy</small>"]
            GRAPH["📊 Graph<br/>Analysis<br/><small>Joern<br/>Neo4j<br/>Fiedler</small>"]
        end

        MUT --> BRE
        SYM --> BRE
        GRAPH --> BRE

        BRE["🧠 Belief Revision Engine<br/><small>AGM Theory · Entrenchment · Provenance DAG</small>"]

        BRE --> SYNTH

        SYNTH["⚙️ Synthesis Loop<br/><small>CEGIS · CEGAR · Genetic Algorithm</small>"]

        SYNTH --> |"counterexample"| BRE

        SYNTH --> OUTPUT

        OUTPUT["✅ Strongly Typed Patch<br/><small>Proof Certificate ·Type Signature<br/>Pre/Post Conditions</small>"]
    end

    LLM["🤖 LLM Candidates<br/><small>top-k samples</small>"] --> SYNTH

    style MCP fill:#1a1a2e,stroke:#16213e,color:#eee
    style Sources fill:#16213e,stroke:#0f3460,color:#eee
    style MUT fill:#0f3460,stroke:#e94560,color:#eee
    style SYM fill:#0f3460,stroke:#e94560,color:#eee
    style GRAPH fill:#0f3460,stroke:#e94560,color:#eee
    style BRE fill:#533483,stroke:#e94560,color:#eee
    style SYNTH fill:#e94560,stroke:#ff6b6b,color:#fff
    style OUTPUT fill:#06d6a0,stroke:#118ab2,color:#000
    style LLM fill:#ffd166,stroke:#ef476f,color:#000

ロードマップ

フェーズ 1：基盤 ✅

• MCP サーバーのインフラストラクチャ
• Stryker レポートの解析
• 実行履歴と PID メトリクス
• 柔軟な領域モデル（階層：ファイル → クラス → 関数 → 行）
• mutmut パーサーの統合
• フレームワークの自動検出
• 統合パーサーインターフェース

フェーズ 2：グラフインフラストラクチャ ✅

• グラフモデル（CodeGraph、Node、Edge）
• 呼び出しグラフの抽出（AST ベース）
• ASR 抽出器（インポート／クラス分析）
• 依存関係グラフの抽出（モジュールレベルのインポート）
• 呼び出しグラフ／依存関係グラフからのラプラシアン構築
• フィードラー・ベクトルの計算（scipy.sparse.linalg）
• 仮想シンク／ソースを使った再帰的なフィードラー分割
• SCC 検出と階層的凝縮
• 平面部分グラフの特定（Boyer-Myrvold）
• O(1) の到達可能性を実現する Kameda 前処理
• MCP ツール（抽出、分割、到達可能性、階層、検索）

フェーズ 3：複数フレームワークのオーケストレーション ✅

• 統合ミューテーションフレームワークインターフェース
• cosmic-ray パーサー
• poodle パーサー
• universalmutator パーサー

フェーズ 4：信念改訂エンジン ✅

• py-brs ライブラリの統合（AGM コア）
• エビデンスアダプター（変更結果 → 信念）
• curate-ipsum 用の理論マネージャー
• AGM 縮約（py-brs v2.0.0 リリース済み）
• 固執度の計算（py-brs v2.0.0）
• 来歴 DAG の保存とクエリ
• 失敗モードアナライザー
• ロールバック機構

フェーズ 5：統合ループ ✅

• LLM によるシード生成を含む CEGIS の実装
• AST を考慮した交叉を用いる遺伝的アルゴリズム
• エントロピーの監視と多様性の注入
• 反例に基づく変更
• CEGAR の予算拡大（10s → 30s → 120s）

フェーズ 6：検証バックエンド ✅

• SMT ソルバー用の Z3 統合（デフォルトのバックエンド）
• angr Docker によるシンボリック実行（高コスト層）
• 予算拡大を備えた CEGAR オーケストレーター
• 検証ハーネスビルダー（C ソース生成）
• テスト用のモックバックエンド
• 代替ソルバー（CVC5、Boolector）
• SymPy パス条件のエンコーディング

フェーズ 7：グラフの永続化 ✅

• 抽象 GraphStore ABC
• SQLite グラフストア（プライマリ）
• Kuzu グラフストア（オプション）
• 統合結果の永続化
• Kameda & Fiedler の永続化
• 増分更新エンジン

フェーズ 8：RAG / セマンティック検索 ✅

• ChromaDB ベクトルストアの統合
• sentence-transformers 埋め込みプロバイダー（all-MiniLM-L6-v2）
• グラフ拡張 RAG パイプライン（ベクトル top-k → 隣接ノードの展開 → 再ランク付け）
• 時間的関連性のための減衰スコアリング
• コンテキストを考慮した統合のための CEGIS 統合

フェーズ 9：本番環境向けの堅牢化 ✅

• CI/CD（GitHub Actions — lint、テストマトリックス、統合、ロックファイル）
• リリースパイプライン（タグのプッシュ → PyPI + GHCR + MCP レジストリ）
• uv ロックファイル（149 パッケージ）
• pre-commit フック（ruff format + lint + ロックチェック）
• MCP バンドルのパッケージ化（server.json、smithery.yaml、manifest.json）
• HTML/SARIF レポート
• IDE 拡張機能（VSCode）
• リグレッション検出とアラート

今後の作業

高度なオーケストレーション（延期）

• 暗黙的な領域の検出（スペクトル異常）
• 矛盾のないフレームワークの割り当て
• フレームワーク横断の生存分析

セマンティック検索と RAG

• セマンティック検索用の Code Graph RAG
• セマンティック検索インデックス（ChromaDB）
• グラフ拡張を用いた RAG 検索パイプライン
• テキストから Cypher クエリへの変換

クイックスタート

# Clone and install (dev)
git clone https://github.com/egoughnour/curate-ipsum.git
cd curate-ipsum
uv sync --extra dev --extra verify --extra rag --extra graph --extra synthesis

# Run the MCP server
uv run curate-ipsum

# Or run tests
make test                     # fast suite (no Docker/model needed)
make test-all                 # including integration tests

設定

すべての設定は環境変数で行います（.env.example を参照）。

CURATE_IPSUM_GRAPH_BACKEND=sqlite   # or kuzu
MUTATION_TOOL_DATA_DIR=.mutation_tool_data
MUTATION_TOOL_LOG_LEVEL=INFO
CHROMA_HOST=                         # empty = in-process, or localhost:8000
EMBEDDING_MODEL=all-MiniLM-L6-v2

サービススタック全体（ChromaDB + angr runner）を利用する場合：

make docker-up-verify         # starts Chroma + angr via Docker Compose

ドキュメント

計画と設計

• フェーズ 2 の計画 - 進行中：グラフ・スペクトル基盤（9 ステップ）
• 進捗 - 現在の状況、完了した項目、次の作業
• 決定事項 - 根拠を含むアーキテクチャ上の決定事項（D-001 から D-008）
• M1 マルチフレームワーク計画 - 領域モデルとパーサーの設計（完了）
• BRS 統合計画 - 信念改訂の統合
• BRS v2 リファクタリング計画 - モジュラーアーキテクチャ
• ロードマップ - すべてのマイルストーンの追跡

アーキテクチャ

• アーキテクチャのビジョン - グラフ・スペクトルフレームワーク
• 統合フレームワーク - CEGIS/CEGAR/遺伝的アプローチ
• 信念改訂 - AGM 理論と来歴

リファレンス

• 概要 - 機能カタログ
• 今後の方向性 - 機能強化のロードマップ
• シナジー - ツールエコシステムの統合
• CONTEXT - AI アシスタント向けのセッションコンテキスト
• DOCS_INDEX - ドキュメントのクイックリファレンス

主要な参考文献

• Alchourrón、Gärdenfors、Makinson（1985）。On the Logic of Theory Change
• Fiedler（1973）。Algebraic Connectivity of Graphs
• Kameda（1975）。On the Vector Representation of Reachability in Planar Directed Graphs
• Solar-Lezama（2008）。Program Synthesis by Sketching（CEGIS）
• Clarke ほか（2000）。Counterexample-Guided Abstraction Refinement（CEGAR）

ライセンス

MIT License — 詳細は LICENSE を参照してください。

---