Curate Ipsum

🚀 Curate-Ipsum

Curate-Ipsum 是一款圖譜 MCP 服務器，可通過信念修正實現經過驗證的代碼合成。

它彌合了大語言模型（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                 # 包括集成測試

✨ 主要特性

• 彌合大語言模型生成代碼與形式驗證補丁之間的差距。
• 將變異測試作為維護代碼庫元數據系統的一部分，支持可達性分析、符號執行和自動化測試生成。
• 提供 30 種工具，分為六個組，涵蓋測試、信念修正、回滾與失敗處理、圖譜分析、驗證、合成與檢索增強生成（RAG）等功能。

📦 安裝指南

PyPI 安裝

pip install curate-ipsum

使用 uv 安裝

uv pip install curate-ipsum

Docker 安裝（包含預嵌入模型）

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

💻 使用示例

Curate-Ipsum 通過 MCP 標準輸入輸出傳輸暴露了 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

📚 詳細文檔

規劃與設計

• 階段 2 計劃 - 進行中：圖譜基礎設施（9 個步驟）
• 進度 - 當前狀態、已完成事項和下一步計劃
• 決策 - 帶有推理的架構決策（從 D - 001 到 D - 008）
• M1 多框架計劃 - 區域模型與解析器設計（已完成）
• BRS 集成計劃 - 信念修正集成
• BRS v2 重構計劃 - 模塊化架構
• 路線圖 - 完整里程碑跟蹤

架構

• 架構願景 - 圖譜框架
• 合成框架 - CEGIS/CEGAR/遺傳算法方法
• 信念修正 - AGM 理論與出處

參考

• 總結 - 功能目錄
• 潛在方向 - 增強路線圖
• 協同作用 - 工具生態系統集成
• 上下文 - AI 助手的會話上下文
• 文檔索引 - 文檔快速參考

🔧 技術細節

問題所在

大語言模型生成的代碼存在以下問題：

• ✅ 語法通常有效
• ✅ 統計上看似合理
• ❌ 語義有時不正確
• ❌ 類型安全往往是偶然的
• ❌ 從未經過形式驗證

當前的方法要麼盲目信任大語言模型的輸出，要麼完全拒絕它，這兩種方法都不是最優的。

解決方案

使用大語言模型進行低成本候選生成，然後投入計算資源以實現形式保證：

LLM 候選（k 個樣本）
        ↓
   種子種群
        ↓
┌───────────────────────────┐
│  CEGIS + CEGAR + 遺傳算法  │  ← 驗證循環
│  + 信念修正               │
└───────────────────────────┘
        ↓
  強類型補丁
  (帶有證明證書)

與現有技術的關鍵區別

與傳統變異測試（Stryker、mutmut、cosmic - ray）相比

與大語言模型代碼生成（Copilot、Claude、GPT）相比

與程序合成（Sketch、Rosette、SyGuS）相比

與符號執行（KLEE、S2E）相比

新穎貢獻

1. 圖譜代碼分解

   • Fiedler 向量分區以實現最佳可達性
   • 分層強連通分量（SCC）凝聚
   • 平面子圖識別 → O(1) Kameda 查詢
   • 庫拉托夫斯基子圖作為原子非平面單元

2. 用於合成的信念修正

   • 符合 AGM 的理論修正
   • 用於最小收縮的根深蒂固排序
   • 用於故障模式分析的出處有向無環圖（DAG）
   • 回滾增強有效性（故障改進通用模型）

3. 隱式區域檢測

   • 譜異常揭示測試不足的代碼
   • 跨框架變異抗性識別關鍵區域
   • 歷史可變性指導分區優化

4. 數學約束重構

   • 布爾難解問題 → 微分/根查找
   • SymPy 路徑條件編碼
   • 混合 SMT + 數值求解

架構

flowchart TB
    subgraph MCP["MCP 接口"]
        direction TB

        subgraph Sources["分析源"]
            direction LR
            MUT["🧬 變異<br/>編排器<br/><small>Stryker<br/>mutmut<br/>cosmic-ray</small>"]
            SYM["🔬 符號<br/>執行<br/><small>KLEE · Z3<br/>SymPy</small>"]
            GRAPH["📊 圖<br/>分析<br/><small>Joern<br/>Neo4j<br/>Fiedler</small>"]
        end

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

        BRE["🧠 信念修正引擎<br/><small>AGM 理論 · 根深蒂固 · 出處 DAG</small>"]

        BRE --> SYNTH

        SYNTH["⚙️ 合成循環<br/><small>CEGIS · CEGAR · 遺傳算法</small>"]

        SYNTH --> |"反例"| BRE

        SYNTH --> OUTPUT

        OUTPUT["✅ 強類型補丁<br/><small>證明證書 · 類型簽名<br/>前置/後置條件</small>"]
    end

    LLM["🤖 大語言模型候選<br/><small>前 k 個樣本</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] 調用圖提取（基於抽象語法樹）
• [x] ASR 提取器（導入/類分析）
• [x] 依賴圖提取（模塊級導入）
• [x] 從調用/依賴圖構建拉普拉斯矩陣
• [x] Fiedler 向量計算（scipy.sparse.linalg）
• [x] 帶有虛擬匯/源的遞歸 Fiedler 分區
• [x] SCC 檢測和分層凝聚
• [x] 平面子圖識別（Boyer - Myrvold）
• [x] Kameda 預處理以實現 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] 基於大語言模型種子的 CEGIS 實現
• [x] 具有 AST 感知交叉的遺傳算法
• [x] 熵監測和多樣性注入
• [x] 反例導向的變異
• [x] CEGAR 預算升級（10 秒 → 30 秒 → 120 秒）

階段 6：驗證後端 ✅

• [x] Z3 集成用於 SMT 求解（默認後端）
• [x] angr Docker 符號執行（昂貴級別）
• [x] 帶有預算升級的 CEGAR 編排器
• [x] 驗證框架構建器（C 源生成）
• [x] 用於測試的模擬後端
• [ ] 替代求解器（CVC5、Boolector）
• [ ] SymPy 路徑條件編碼

階段 7：圖持久化 ✅

• [x] 抽象圖存儲 ABC
• [x] SQLite 圖存儲（主要）
• [x] Kuzu 圖存儲（可選）
• [x] 合成結果持久化
• [x] Kameda 和 Fiedler 持久化
• [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

📄 許可證

本項目採用 MIT 許可證，請參閱 LICENSE 瞭解詳細信息。

🔍 關鍵參考文獻

• 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)