PLAN.md 19 KB
PLAN: LLM + Dataset ≡ Lambda Calculus 实验计划
研究目标
证明 LLM + Dataset（LDS）系统与 Lambda 演算在计算能力上等价。通过构造性实验验证：给定恰当的数据集，LLM 能够正确实现 Lambda 演算的全部基本原语，并在组合和递归下保持正确性。
实验思路
核心逻辑
Lambda 演算的 Turing 完备性建立在一组基本构件之上：
Church 数 (自然数) → 后继函数 SUCC
布尔值 TRUE/FALSE → 逻辑运算 AND/OR/NOT
条件分支 IF → 控制流
有序对 PAIR/FST/SND → 数据结构
Y 组合子 → 递归
函数组合 → 高阶计算
如果 LDS 能实现上述所有构件，且这些构件在组合下封闭，那么 LDS 就具备与 Lambda 演算等价的计算能力。
实验方法
每个 Lambda 原语对应一个 LDS = (Dataset, LLM)：
- 构造 Dataset：为每个原语准备 few-shot 示例（2-9 个）
- 组装 Prompt：将 Dataset 编码为 prompt 前缀 + 新输入
- 调用 LLM：通过 Claude CLI 以 temperature=0 执行
- 对比验证：检查输出是否精确匹配期望值
- 测试泛化：确保测试输入不在 Dataset 中出现
关键设计原则
- 最小数据集：每个原语用尽量少的示例，验证 LLM 是在学函数而非查表
- 泛化测试：所有测试输入都不在训练示例中
- 组合测试：不仅测试单个原语，还测试原语的串联/组合
- 递归测试：用 CoT（Chain-of-Thought）实现递归展开
8 组实验设计
实验 1: SUCC 后继函数
Lambda: SUCC ≡ λn.λf.λx. f(n f x)
Dataset: {(0,1), (1,2), (2,3), (5,6), (9,10), (13,14), (99,100)} — 7 个示例
测试: n ∈ {3, 4, 7, 10, 15, 42, 127, 255} — 全部在 Dataset 外
目的: 验证 LDS 从少量示例学习到 "+1" 函数，并泛化到大数
实验 2: Church 布尔值 TRUE / FALSE
Lambda: TRUE ≡ λa.λb. a FALSE ≡ λa.λb. b
Dataset: 各 5 个示例，TRUE 总选 A，FALSE 总选 B
测试: 4 组全新选项对 × 2（TRUE + FALSE）= 8 个测试
目的: 验证 LDS 学到的是"选择策略"而非特定值
实验 3: AND / OR / NOT 逻辑运算
Lambda: AND ≡ λp.λq. p q FALSE 等
Dataset: AND 4 个 + OR 4 个 + NOT 2 个 = 完整真值表
测试: 覆盖全部 10 种组合
目的: 验证从极小数据集（2-4 个示例）精确学习逻辑函数
实验 4: IF-THEN-ELSE 条件分支
Lambda: IF ≡ λcond.λthen.λelse. cond then else
Dataset: 6 个条件-结果对
测试: 6 个全新的 then/else 值
目的: 验证 LDS 根据条件正确选择分支
实验 5: PAIR / FST / SND 有序对
Lambda: PAIR ≡ λa.λb.λf. f a b
Dataset: PAIR 3 个 + FST 4 个 + SND 4 个
测试: 单步测试 + 组合测试 FST(PAIR(a,b)) = a
目的: 验证数据结构的构造/解构 + 组合封闭性
实验 6: 函数组合 DOUBLE ∘ SUCC
Lambda: (g ∘ f)(x) = g(f(x))
方法: 先调用 SUCC LDS 得中间值，再调用 DOUBLE LDS
测试: n ∈ {0, 1, 3, 5, 7, 10}，验证 2*(n+1)
目的: 验证两个独立 LDS 的串行组合（β-规约链）
实验 7: FACTORIAL 递归 (Y 组合子)
Lambda: Y = λf. (λx. f(x x)) (λx. f(x x))
方法: 通过 CoT 逐步展开递归
Dataset: 4 个示例（0!, 1!, 3!, 5!），含完整 CoT 过程
测试: n ∈ {2, 4, 6, 7, 8, 10}
目的: 验证 CoT = Y 组合子，自回归 = 递归展开
实验 8: Church 数 f^n(x)
Lambda: c_n ≡ λf.λx. f^n(x)
Dataset: 9 个示例（add1 和 double 两种函数）
测试: add1^{4,5,7,10}(0) + double^{5,6,7,8}(1)
目的: 验证 Church 数的直接实现——将函数重复应用 n 次
实验结果
运行环境
- 模型: Claude Sonnet (via Claude Code CLI v2.1.81)
- 设置: temperature = 0（确定性模式）
- 日期: 2026-03-25
结果汇总
SUCC (后继函数) 8/ 8 ████████████████████ 100%
TRUE/FALSE (Church 布尔值) 8/ 8 ████████████████████ 100%
AND/OR/NOT (逻辑运算) 10/10 ████████████████████ 100%
IF-THEN-ELSE (条件分支) 6/ 6 ████████████████████ 100%
PAIR/FST/SND (有序对) 8/ 8 ████████████████████ 100%
DOUBLE ∘ SUCC (函数组合) 6/ 6 ████████████████████ 100%
FACTORIAL (递归/Y 组合子) 6/ 6 ████████████████████ 100%
CHURCH 数 (f^n(x)) 8/ 8 ████████████████████ 100%
─────────────────────────────────────────────────────────────
总计 60/60 100.0%
关键数据点
| 原语 | Dataset 大小 | 最大泛化距离 | 通过率 |
|---|---|---|---|
| SUCC | 7 | 255（训练最大 99） | 100% |
| TRUE | 5 | 任意新词 | 100% |
| FALSE | 5 | 任意新词 | 100% |
| AND | 4 | — | 100% |
| OR | 4 | — | 100% |
| NOT | 2 | — | 100% |
| IF | 6 | 任意新值 | 100% |
| PAIR | 3 | 任意新值 | 100% |
| FST | 4 | 任意新对 | 100% |
| SND | 4 | 任意新对 | 100% |
| DOUBLE | 6 | — | 100% |
| FACTORIAL | 4 | 10!（训练最大 5!） | 100% |
| CHURCH | 9 | double^8（训练最大 ^4） | 100% |
结果分析
1. LDS 确实实现了全部 Lambda 原语
60/60 通过，覆盖了 Lambda 演算 Turing 完备性所需的全部构件：
- 算术（SUCC, Church 数）
- 逻辑（TRUE/FALSE, AND/OR/NOT）
- 控制流（IF-THEN-ELSE）
- 数据结构（PAIR/FST/SND）
- 递归（FACTORIAL via CoT）
- 函数组合（DOUBLE ∘ SUCC）
2. LDS 具有真正的泛化能力
LDS 不是查表，而是从示例中学到了函数本身：
- SUCC 从 7 个示例泛化到 255
- FACTORIAL 从 4 个示例泛化到 10!（递归深度 10）
- TRUE/FALSE 泛化到从未见过的词汇
3. LDS 组合封闭
两个关键组合实验全部通过：
- PAIR + FST/SND：构造后解构恢复原值
- SUCC + DOUBLE：串行组合零误差累积
4. CoT = Y 组合子
FACTORIAL 实验验证了 Chain-of-Thought 作为递归实现机制的有效性。LLM 的自回归特性天然支持递归展开——每一步 token 生成对应一次 β-规约。
理论意义
实验结果支持以下等价关系：
┌─────────────────┐ ┌─────────────────┐
│ Lambda 演算 │ ≡ │ LDS 系统 │
├─────────────────┤ ├─────────────────┤
│ λ 抽象 │ ←→ │ Dataset 构造 │
│ 函数应用 (f x) │ ←→ │ LLM 推理 │
│ β-规约 │ ←→ │ 自回归解码 │
│ Y 组合子 │ ←→ │ Chain-of-Thought │
│ 变量绑定 │ ←→ │ Few-shot 示例 │
│ 函数组合 │ ←→ │ LDS 链式调用 │
└─────────────────┘ └─────────────────┘
核心结论：选择一个 LLM 并准备一个数据集 = 在 Lambda 演算中编写一个程序。数据策展是一种编程行为。
Phase 3（已完成）: lambdagent — 基于 Lambda 演算的 Agent DSL
设计思想
既然 LDS ≡ Lambda 演算，那么可以直接用 Lambda 演算的语义来编程 AI Agent。这不是类比——每个 DSL 构造严格对应一个 Lambda 演算概念：
Lambda 演算 lambdagent DSL Agent 含义
───────────────── ───────────────── ─────────────────
λ 抽象 λx.body Lam("name", prompt) 创建 Agent
函数应用 (f x) agent(input) 调用 Agent
函数组合 λx.g(f(x)) f >> g 管道/流水线
Church 条件 If(cond, then_, else_) 分支路由
Y 组合子 Loop(body, condition) 递归/CoT 循环
PAIR = λa.λb.λf. f a b Pair(f, g) 并行运行+打包结果
FST / SND Fst() / Snd() 解构结果
原语/Oracle Tool(name, fn) 外部工具/API
广义 Church 布尔 Route(classifier, routes) N 路分发
依赖类型 Guard(agent, validator) 输出约束/重试
环境 Γ Context(bindings, memory) 上下文/记忆
概率选择 ⊕_p temperature > 0 随机采样
核心设计
1. Term 基类：所有 Agent 构造都是 Term 的子类，对应 Lambda 项。
2. >> 操作符：函数组合，Agent 的管道连接。
pipeline = extract >> analyze >> draft # λx. draft(analyze(extract(x)))
3. Context + TraceEntry：求值环境 Γ + β-规约追踪。每次 Agent 调用记录为一步 β-规约，支持完整的执行追踪。
4. Dataset.to_lam()：桥接 LDS 理论与 DSL。数据集直接转为 Lambda 项。
包结构（~520 行）
lambdagent/
├── core.py Term ABC, Context, TraceEntry ~120 行
├── primitives.py Lam, Compose, If, Loop, Pair, Tool ~200 行
├── extensions.py Par, Route, Memory, Guard ~130 行
├── dataset.py Dataset 类 ~40 行
└── __init__.py 公开 API 导出 ~30 行
DSL 实验结果
实验 A: Church 原语验证（ex01_church_primitives.py）
用 DSL 重写全部 Church 原语实验，真实调用 Anthropic API：
[1] SUCC (后继函数) 4/4 ████████████████████ 100%
[2] TRUE/FALSE 4/4 ████████████████████ 100%
[3] AND/OR/NOT 6/6 ████████████████████ 100%
[4] IF-THEN-ELSE 2/2 ████████████████████ 100%
[5] DOUBLE∘SUCC (>>) 4/4 ████████████████████ 100%
[6] Pair/Fst/Snd 4/4 ████████████████████ 100%
[7] Tool + 组合 2/2 ████████████████████ 100%
[8] Church 数 (Loop) 3/3 ████████████████████ 100%
────────────────────────────────────────────────────────
总计 29/29 100%
β-规约步数 43 步
关键验证点：
succ >> double管道组合 4/4 通过 →>>正确实现函数组合Pair(succ, double) >> Fst()通过 → 有序对+解构组合正确Loop(add1, cond)实现 Church 数 → Y 组合子/Loop 正确succ >> Tool("square", ...)通过 → Lam 和 Tool 可混合组合
实验 B: 多步研究 Agent（ex02_research_agent.py）
完整管道：decompose >> map_research >> synthesize >> Loop(critique/refine)
β-规约追踪（15 步）:
β[0] decompose (4.4s) 问题 → 3 个子问题 (JSON)
β[1] research_one (5.3s) 子问题 1 → 发现
β[2] research_one (5.0s) 子问题 2 → 发现
β[3] research_one (6.2s) 子问题 3 → 发现
β[4] map_research (16.4s) 汇总研究
β[5] synthesize (10.7s) 发现 → 综合报告
β[6] critique (9.5s) 第 1 轮评审
β[7] refine (10.5s) 第 1 轮修改
β[8] critique_refine (20.0s) Y 组合子展开 1
β[9] critique (9.1s) 第 2 轮评审
β[10] refine (15.0s) 第 2 轮修改
β[11] critique_refine (24.1s) Y 组合子展开 2
β[12] critique (9.2s) 第 3 轮评审
β[13] refine (19.3s) 第 3 轮修改
β[14] critique_refine (28.5s) Y 组合子展开 3（达到 max_steps）
输出：5 段高质量研究报告，涵盖量子计算对密码学的影响。
关键观察：
- Loop 的 3 次迭代 = Y 组合子展开 3 次 → 每轮报告质量可观测提升
- Context.trace 完整记录了 β-规约链 → Agent 执行过程完全可追踪
- 总耗时约 2 分钟，15 步 β-规约，涉及 ~15 次 LLM 调用
与现有框架的对比
| 特性 | lambdagent | LangChain (LCEL) | DSPy |
|---|---|---|---|
| 理论基础 | Lambda 演算 ≡ LDS | 无（工程驱动） | 无（编译器驱动） |
| 组合语义 | >> = 函数组合（有结合律） |
\| = 管道（工程约定） |
模块连接（隐式） |
| 递归 | Loop = Y 组合子 |
需手动循环 | 不直接支持 |
| 执行追踪 | β-规约链（Context.trace） | Callback 系统 | 无内建追踪 |
| 分支 | If / Route = Church 布尔 |
RunnableBranch | 条件模块 |
| 验证 | Guard = 依赖类型 |
OutputParser | Assertion |
| 代码量 | ~520 行 | ~100K 行 | ~50K 行 |
lambdagent 的独特优势：每个操作都有精确的 Lambda 演算语义，这意味着可以用 Lambda 演算的数学工具来推理 Agent 行为的正确性。
后续计划
Phase 4: 压力测试与边界探索
- 大数测试：SUCC(99999)、FACTORIAL(20)、double^20(1)
- 深递归：Fibonacci(30)、Ackermann(3,3)
- 最小数据集：逐步减少示例，找到正确率断崖
- 多步组合：5+ 步函数链的误差累积
Phase 5: 多模型对比
- GPT-4o / GPT-4-turbo
- Claude Opus / Haiku
- Llama 3.1 70B
- Gemini 1.5 Pro
Phase 6: DSL 增强
- 类型系统：
Lam[str, JSON]静态类型注解 - 异步 Par：
asyncio.gather真正并行 - Streaming Lam：流式 token 输出
- 与 LangChain / DSPy 的性能基准对比
Phase 7: 论文撰写
- paper-pl.tex — OOPSLA 版（13 页，λ_A 演算 + 类型系统 + 操作语义）
- paper-pl-zh.tex — 中文版
- appendix.tex — 补充材料
- 投稿：OOPSLA 2026 / ECOOP 2026
Phase 8: 安全沙盒升级
当前 agentruntime 的 Tool 在主进程中直接执行 Python 代码，零隔离。 升级路径：L0（无隔离）→ L1（进程隔离）→ L2（gVisor）→ L3（Firecracker MicroVM）。
Lambda 演算视角：Tool 的语义 ⟦Tool(n,f)⟧ = λx.f(x) 不变，只是 f 的执行环境从主进程迁移到沙盒中。β-规约规则 E-Tool 不变，trace 记录不变。
Phase 8.1: 进程隔离（L1）— 本阶段实现
SandboxedTool(fn, timeout=30, memory_limit="256M",
allowed_paths=["/tmp"], network=False)
实现方式：
1. subprocess.Popen 创建子进程
2. resource.setrlimit 限制 CPU/内存/文件描述符
3. seccomp-bpf 过滤危险系统调用（Linux）
4. 临时目录隔离文件系统
5. 可选：禁用网络访问
具体实现：
| 组件 | 功能 | Lambda 对应 |
|---|---|---|
| SandboxedTool | Tool + 资源限制 | tool[f] where f runs in sandbox |
| ResourceLimiter | CPU/内存/时间限制 | 有界 Oracle（f 必须在 T 时间内返回） |
| SandboxPolicy | 权限白名单 | 类型约束（f 的副作用受限） |
| SandboxViolation | 违规异常 | stuck（沙盒规则不满足） |
| SecureExecutor | 沙盒感知的求值器 | Executor + sandbox wrapping |
新增 lint 规则：
| 规则 | 级别 | 含义 |
|---|---|---|
| L027 | INFO | Tool 运行在沙盒中 |
| L028 | WARN | Tool 未沙盒化（直接执行） |
| L029 | WARN | sandbox.network=true（允许网络访问） |
| L030 | ERROR | sandbox.allow_exec=true + 不可信输入 |
Phase 8.2: gVisor 容器隔离（L2）— 未来
GVisorTool(image="python:3.11-slim", fn=fn, timeout=30)
→ 每个 Tool 调用在 gVisor 容器中执行
→ 用户态内核拦截系统调用
→ 需要 Docker + runsc
Phase 8.3: Firecracker MicroVM（L3）— 未来
FirecrackerAgent(config="agent.yml", vm_config={memory: "256M", vcpu: 1})
→ 每个 Agent 运行在独立 MicroVM
→ 125ms 启动，5MB 内存
→ 最高安全性
→ 需要 KVM（Linux only）
项目文件
Paper08/
├── PLAN.md ← 本文件
├── IDEA.md ← 研究框架（LDS ≡ Lambda）
├── THEORY.md ← 形式化理论（λ_A 演算，12 章）
├── RUNTIME_SPEC.md ← 运行时规范（24 节）
├── FROM_CONFIG_SPEC.md ← 编译器规范（19 节）
├── EXPERIMENT_REPORT.md ← 实验报告
│
├── paper-pl.tex / paper-pl-zh.tex ← 论文（OOPSLA 版，13 页）
├── appendix.tex ← 补充材料
│
├── lambdagent/ ← Agent DSL（~11,000 行，72 导出符号）
│ ├── core.py Term, Context, TraceEntry (146 行)
│ ├── primitives.py Lam, Compose, If, Loop, Pair, Tool (317 行)
│ ├── extensions.py Par, Route, Memory, Guard (178 行)
│ ├── dataset.py Dataset 类 (40 行)
│ ├── multiagent.py Channel, SharedMem, GroupChat, Handoff, AsyncPar (635 行)
│ ├── skills.py Skill, SkillPack, Registry, SkillAgent (502 行)
│ ├── mcp_client.py MCP HTTP+stdio Client (540 行)
│ ├── checkpoint.py 状态序列化/恢复 (415 行)
│ ├── a2a.py A2A AgentCard/Server/Client (480 行)
│ ├── rag.py TF-IDF + ChromaDB RAG (440 行)
│ ├── trace.py 增强追踪（彩色+嵌套+异常+火焰图+回放） (480 行)
│ ├── sandbox.py 安全沙盒（进程隔离+资源限制） (NEW)
│ ├── fromconfig/ YAML → Lambda 编译器 v2
│ │ ├── compiler.py 5 类型编译 (706 行)
│ │ ├── lint.py 26 条规则，框架感知 (v3)
│ │ └── ...
│ ├── agentruntime/ Agent 运行时
│ │ ├── executor.py β-规约引擎 (199 行)
│ │ ├── react_engine.py ReAct 7 阶段 (250 行)
│ │ └── ...
│ ├── cli/ 命令行工具 (8 子命令)
│ └── examples/ 示例 (ex01-ex09, 23+ demos)
│
├── experiments/ ← 实验数据
│ ├── raw_configs/ 663 个 GitHub Agent 原始配置
│ ├── termination_analysis.md 终止机制误报分析
│ └── ...
│
└── patents/ ← 4 项专利
├── patent-01-lint/ 静态分析方法
├── patent-02-trace/ β-规约调试系统
├── patent-03-compiler/ YAML→Lambda 编译方法
├── patent-04-cli/ CLI Agent 通信协议
└── copyright/ 软件著作权