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)