Curate Ipsum

🚀 Curate-Ipsum

信念修正による検証済みコード合成のためのグラフスペクトルMCPサーバー

Curate-Ipsumは、LLMによって生成されたコード（高速であり、妥当性があるが、検証されていない）と、正式に検証されたパッチ（低速であるが、正確で、信頼できる）との間のギャップを埋めます。これは、ミューテーションテストを、到達可能性分析、シンボリック実行、および自動テスト生成をサポートする、堅牢で自己修復可能なコードベースメタデータを維持するための大規模なシステムの一部として扱います。

🚀 クイックスタート

# クローンしてインストール（開発用）
git clone https://github.com/egoughnour/curate-ipsum.git
cd curate-ipsum
uv sync --extra dev --extra verify --extra rag --extra graph --extra synthesis

# MCPサーバーを実行
uv run curate-ipsum

# またはテストを実行
make test                     # 高速なテストセット（Dockerやモデルは不要）
make test-all                 # 統合テストも含む

✨ 主な機能

Curate-Ipsumは、MCP標準入出力トランスポートを介して30のツールを公開しており、6つのグループに分類されています。

• テスト — 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

📦 インストール

# PyPI
pip install curate-ipsum

# またはuvを使用
uv pip install curate-ipsum

# Docker（組み込みの埋め込みモデルを含む）
docker pull ghcr.io/egoughnour/curate-ipsum:latest

Claude Desktop / MCP Client

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"]
    }
  }
}

📚 ドキュメント

計画と設計

• Phase 2 Plan - アクティブ：グラフスペクトルインフラストラクチャ（9ステップ）
• Progress - 現在の状況、完了したこと、次に行うこと
• Decisions - 理由付きのアーキテクチャ上の決定（D-001からD-008）
• M1 Multi-Framework Plan - 領域モデルとパーサーの設計（完了）
• BRS Integration Plan - 信念修正の統合
• BRS v2 Refactoring Plan - モジュール化されたアーキテクチャ
• ROADMAP - 完全なマイルストーントラッカー

アーキテクチャ

• Architectural Vision - グラフスペクトルフレームワーク
• Synthesis Framework - CEGIS/CEGAR/遺伝的アルゴリズムアプローチ
• Belief Revision - AGM理論とプロバナンス

リファレンス

• Summary - 機能カタログ
• Potential Directions - 拡張ロードマップ
• Synergies - ツールエコシステムの統合
• CONTEXT - AIアシスタントのセッションコンテキスト
• DOCS_INDEX - ドキュメントのクイックリファレンス

🔧 技術詳細

問題

LLMは以下のようなコードを生成します。

• ✅ 構文的に有効（通常）
• ✅ 統計的に妥当
• ❌ 意味的に正しい（時々）
• ❌ 型安全（偶然）
• ❌ 正式に検証された（決して）

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

解決策

LLMを安価な候補生成に使用し、その後、計算リソースを投資して正式な保証を達成します。

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

既存技術との主な違い

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

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

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

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

新しい貢献

1. グラフスペクトルコード分解
   • 最適な到達可能性のためのフィードラーベクトルパーティショニング
   • 階層的なSCC凝縮
   • 平面サブグラフの識別 → O(1)の亀田クエリ
   • クラトウスキーサブグラフを原子的な非平面ユニットとして
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: 基礎 ✅

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

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

• [x] グラフモデル（CodeGraph, Node, Edge）
• [x] 呼び出しグラフの抽出（ASTベース）
• [x] ASR抽出器（インポート/クラス分析）
• [x] 依存関係グラフの抽出（モジュールレベルのインポート）
• [x] 呼び出し/依存関係グラフからのラプラシアンの構築
• [x] フィードラーベクトルの計算（scipy.sparse.linalg）
• [x] 仮想シンク/ソースを用いた再帰的なフィードラーパーティショニング
• [x] SCC検出と階層的な凝縮
• [x] 平面サブグラフの識別（ボイヤー・マイルヴォルド法）
• [x] O(1)到達可能性のための亀田事前処理
• [x] MCPツール（抽出、パーティショニング、到達可能性、階層、検索）

フェーズ3: マルチフレームワークオーケストレーション ✅

• [x] 統一されたミューテーションフレームワークインターフェース
• [x] cosmic-rayパーサー
• [x] poodleパーサー
• [x] universalmutatorパーサー

フェーズ4: 信念修正エンジン ✅

• [x] py-brsライブラリの統合（AGMコア）
• [x] 証拠アダプター（ミューテーション結果 → 信念）
• [x] curate-ipsumの理論マネージャー
• [x] AGM収縮（py-brs v2.0.0リリース）
• [x] 固着計算（py-brs v2.0.0）
• [x] プロバナンスDAGの保存とクエリ
• [x] 失敗モード分析器
• [x] ロールバックメカニズム

フェーズ5: 合成ループ ✅

• [x] LLMシーディングによるCEGISの実装
• [x] AST認識クロスオーバーを持つ遺伝的アルゴリズム
• [x] エントロピーモニタリングと多様性注入
• [x] 反例指向のミューテーション
• [x] CEGAR予算エスカレーション（10秒 → 30秒 → 120秒）

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

• [x] SMT解決のためのZ3の統合（デフォルトバックエンド）
• [x] angr Dockerシンボリック実行（高コストのタイア）
• [x] 予算エスカレーションを持つCEGARオーケストレーター
• [x] 検証ハーネスビルダー（Cソース生成）
• [x] テスト用のモックバックエンド
• [ ] 代替ソルバー（CVC5, Boolector）
• [ ] SymPyパス条件のエンコーディング

フェーズ7: グラフ永続化 ✅

• [x] 抽象的なGraphStore ABC
• [x] SQLiteグラフストア（主要）
• [x] Kuzuグラフストア（オプション）
• [x] 合成結果の永続化
• [x] 亀田とフィードラーの永続化
• [x] 増分更新エンジン

フェーズ8: RAG / 意味検索 ✅

• [x] ChromaDBベクトルストアの統合
• [x] sentence-transformers埋め込みプロバイダー（all-MiniLM-L6-v2）
• [x] グラフ拡張されたRAGパイプライン（ベクトルの上位k → 近傍拡張 → 再ランク付け）
• [x] 時間的な関連性のための減衰スコアリング
• [x] コンテキスト認識合成のためのCEGISの統合

フェーズ9: 本番環境の強化 ✅

• [x] CI/CD（GitHub Actions — リント、テストマトリックス、統合、ロックファイル）
• [x] リリースパイプライン（タグプッシュ → PyPI + GHCR + MCPレジストリ）
• [x] uvロックファイル（149パッケージ）
• [x] プリコミットフック（ruffフォーマット + リント + ロックチェック）
• [x] MCPバンドルパッケージング（server.json, smithery.yaml, manifest.json）
• [ ] HTML/SARIFレポート
• [ ] IDE拡張（VSCode）
• [ ] 回帰検出とアラート

将来の作業

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

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

意味検索とRAG

• [x] 意味検索のためのコードグラフRAG
• [x] 意味検索インデックス（ChromaDB）
• [x] グラフ拡張を持つRAG検索パイプライン
• [ ] テキストからCypherクエリへの変換

設定

すべての設定は環境変数を通じて行われます（.env.exampleを参照）。

CURATE_IPSUM_GRAPH_BACKEND=sqlite   # またはkuzu
MUTATION_TOOL_DATA_DIR=.mutation_tool_data
MUTATION_TOOL_LOG_LEVEL=INFO
CHROMA_HOST=                         # 空 = プロセス内、またはlocalhost:8000
EMBEDDING_MODEL=all-MiniLM-L6-v2

完全なサービススタック（ChromaDB + angrランナー）の場合

make docker-up-verify         # Docker Composeを介してChroma + angrを起動

主要参考文献

• 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 et al. (2000). Counterexample-Guided Abstraction Refinement (CEGAR)

📄 ライセンス

MITライセンス - LICENSEを参照