Curate-Ipsum

Curate-Ipsum

通过信念修订实现经过验证的代码合成的图谱谱 MCP 服务

Curate-Ipsum 填补了大模型生成的代码（快速、看似合理、未经验证）与形式化验证的补丁（缓慢、正确、可信）之间的鸿沟。它将变异测试视为一套更大型系统的组成部分，用于维护稳健、自愈的代码库元数据，支持可达性分析、符号执行和自动化测试生成。

安装

# 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 传输方式提供 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 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
信任模型输出	验证模型输出
单次采样或 best-of-k	基于群体的优化
无形式化保证	证明证书
无状态生成	带溯源的信念修正
看似合理的代码	可证明正确的代码

与程序综合（Sketch、Rosette、SyGuS）的比较

传统综合	Curate-Ipsum
手写草图	LLM 生成的候选项
冷启动搜索	从 LLM 候选群体热启动
运行之间不学习	全化理论不断累积知识
单一规范	多框架隐式区域

与符号执行（KLEE、S2E）的比较

符号执行	Curate-Ipsum
仅探索路径	与综合集成
布尔约束求解	数学重构（SymPy）
单一工具分析	图数据库 + SMT + 变异编排
不生成代码	生成经过验证的补丁

创新贡献

1. 图谱频谱代码分解

   • 使用 Fiedler 向量分区以实现最优可达性
   • 分层 SCC 凝缩
   • 平面子图识别 → O(1) Kameda 查询
   • Kuratowski 子图作为原子级非平面单元

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 提取器（导入／类分析）
• 依赖图提取（模块级导入）
• 根据调用图／依赖图构建拉普拉斯矩阵
• Fiedler 向量计算（scipy.sparse.linalg）
• 使用虚拟汇点／源点递归进行 Fiedler 分区
• SCC 检测和分层凝缩
• 平面子图识别（Boyer-Myrvold）
• Kameda 预处理，实现 O(1) 可达性查询
• MCP 工具（提取、分区、可达性、层级、查找）

阶段 3：多框架编排 ✅

• 统一变异框架接口
• cosmic-ray 解析器
• poodle 解析器
• universalmutator 解析器

Phase 4：信念修正引擎 ✅

• 集成 py-brs 库（AGM 核心）
• 证据适配器（突变结果 → 信念）
• curate-ipsum 理论管理器
• AGM 收缩（py-brs v2.0.0 已发布）
• 根深度计算（py-brs v2.0.0）
• 来源 DAG 存储与查询
• 失败模式分析器
• 回滚机制

Phase 5：综合循环 ✅

• 使用 LLM 种子的 CEGIS 实现
• 具备 AST 感知交叉操作的遗传算法
• 熵监控与多样性注入
• 反例导向突变
• CEGAR 预算递增（10s → 30s → 120s）

Phase 6：验证后端 ✅

• 集成 Z3 进行 SMT 求解（默认后端）
• angr Docker 符号执行（高开销层级）
• 带预算递增的 CEGAR 编排器
• 验证测试框架构建器（生成 C 源代码）
• 用于测试的模拟后端
• 替代求解器（CVC5、Boolector）
• SymPy 路径条件编码

Phase 7：图持久化 ✅

• 抽象 GraphStore ABC
• SQLite 图存储（主要）
• Kuzu 图存储（可选）
• 持久化综合结果
• 持久化 Kameda & Fiedler
• 增量更新引擎

Phase 8：RAG / 语义搜索 ✅

• 集成 ChromaDB 向量存储
• sentence-transformers 嵌入提供程序（all-MiniLM-L6-v2）
• 图扩展 RAG 流水线（向量 top-k → 邻居扩展 → 重排）
• 用于衡量时间相关性的衰减评分
• 集成 CEGIS，实现上下文感知综合

Phase 9：生产环境加固 ✅

• CI/CD（GitHub Actions — lint、测试矩阵、集成、锁文件）
• 发布流水线（推送标签 → PyPI + GHCR + MCP registry）
• uv 锁文件（149 个软件包）
• pre-commit 钩子（ruff format + lint + 锁文件检查）
• MCP bundle 打包（server.json、smithery.yaml、manifest.json）
• HTML/SARIF 报告
• IDE 扩展（VSCode）
• 回归检测与告警

后续工作

高级编排（暂缓）

• 隐式区域检测（谱异常）
• 非矛盾框架分配
• 跨框架生存分析

语义搜索与 RAG

• 用于语义搜索的代码图 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

文档

规划与设计

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

---