总体目标（MVP）

• FastAPI 后端提供：创建项目、上传/指定 PDF、运行 pipeline、查询状态、查看报告。
• pipeline 做到端到端：
  1. PDF → 页级文本切分 → 提取少量英文 定理/定义/证明候选
  2. 生成每条内容的 英文 evidence anchor（en_anchor_id：页码 + snippet）
  3. 生成中文内容，且每条中文都能回溯到 en_anchor_id
  4. 生成可编译中文 LaTeX（先用最简模板；编译失败也必须记录日志并尝试修复）
  5. Lean 文件生成：在无 Lean 环境下先生成骨架，并输出日志
  6. QA checks 强制：无 anchor 则失败

---

搭骨架

目录：

├── backend/
│   └── main.py                # 后端入口文件
├── pipeline/
│   ├── compiler.py             # 使用 xelatex 编译 tex 文件并在失败时调用 Auto-Healing Agent 进行修复。
│   ├── core.py              # 定义整个数学处理流水线的核心流程
│   ├── formalizer.py              # 自动化将LaTeX证明文本转化为Lean4代码的辅助工具
│   ├── latex_generator.py              
│   ├── llm_agent.py              
│   ├── pdf_parser.py             
│   ├── schema.py              # 统一各模块输入/输出格式
├── artifacts/
│   ├── projects/
│   │   └── {id}/              # 按项目ID划分的专属目录
│   │       ├── inputs/        # 项目输入文件存储目录
│   │       ├── intermediate/  # 项目中间产物存储目录
│   │       └── logs/          # 单个项目的日志存储目录
│   └── projects_db.json       # 存储每个项目的状态信息
├── logs/                      # 全流程日志存储目录（全局日志）
└── static/                    # 前端静态页面目录
    ├── index.html
    └── project.html

---

💡

“PDF 解析 → 内容规范化 → LLM 智能优化 → LaTeX 生成 → 编译输出 → 前端展示”

PDF 解析与页级段级切分（pipeline/pdf_parser.py）

从数学 PDF 中精准提取普通文本、数学公式、章节结构，转化为结构化数据 页级读取，段落切分

• 用 pdfplumber 提取文本（保留页码，章节编号，章节标题，段落内容，生成一个唯一idp{页号}_s{行号}）
• 输出：intermediate/anchors.json

策略：

• 正则识别章节、数学实体（定理、定义、证明、remark）
• 逐页解析，逐行扫描文本，并缓存
  • CAS：若命中边界且缓存有内容：先保存缓存的文本块（上一个逻辑单元），再清空缓存
• 统一解析结果格式，让下游任务统一解析不同PDF，降低耦合度

---

Agent：中文生成 + 中文 LaTeX + Lean代码

将英文 LaTeX 格式的数学 / 学术论文片段，通过大模型转化

• 输入：待处理的英文片段
• 输出：包含中文翻译、逻辑拆解、Lean 4 代码骨架的结构化 JSON 数据
• prompt 多次调整
  • temperature=0.1：极低随机性，确保数学 / 逻辑类输出的准确性；
  • max_tokens=3072：限制输出长度，适配 LaTeX 片段的处理需求
• JSON 解析失败时候，引入Agent修复

---

Agent：编译中文pdf + Lean 4 代码骨架 + 形式化图谱 JSON

• 拼接全文 LaTeX 内容，合成 LaTeX 模板，写入project_path/main.tex
• 执行 LaTeX 编译（基于 XeLaTeX）
  • 失败，调用大模型分析报错、修复LaTeX 源码，重新生成 main.tex 并再编译
  • 成功

  • • 根据生成拓扑图谱，并保存

      节点字段	取值逻辑
      id	唯一节点 ID（如p1_step1_1）
      type	类型（Theorem/Lemma，基于lean_stub是否含theorem）
      title	子步骤标题（截取logic前 15 字 + 步骤 ID）
      description	推理描述 + 核心键点 + 来源（logic + key_point + 页码/片段ID）
      lean_code	子步骤的lean_stub（Lean 代码桩）
      其他（如source_page）	关联原始片段的页码、章节信息，用于溯源

Agent： 主定理抽取

分析项目全量逻辑片段，提炼并深度解构整篇论文最具代表性的主定理元 metadata

• 从全量片段中提炼论文最核心的主定理
• 输出结构化 JSON（含、、等），并落盘文件
  • 该定理在片段中对应的真实 ID
  • 主定理的标志性简短名称
  • 主定理的完整原始英文 LaTeX 、中文描述
  • 证明思路
  • Lean 声明

---

日志

1. 整个服务的总体日志：记录服务的运行状态和每个项目的编译进度
2. 项目的单独日志：保留每个项目的活动情况

---

Agent

1. Formalization Agent：将英文 LaTeX 片段转化为包含翻译、逻辑拆解和 Lean 骨架的结构化 JSON
2. Theorem Extractor Agent：分析项目全量逻辑片段，提炼并深度解构整篇论文最具代表性的主定理元 metadata
3. Console Agent：
   • 优先拦截物理操作命令（编译、查状态、查日志）→ 直接操作本地文件 / 执行编译；
     • 继续编译
     • 重新编译
   • 非操作命令就走自由对话 → 读取项目本地文件，带着真实上下文调用大模型回答学术问题。
4. Auto-Healing Agent：自愈逻辑：根据 XeLaTeX 的报错信息，让 AI 尝试修复 LaTeX 源码
5. Structured Output Repair Agent：将输入修复为严格合法的 JSON 并保持原始字段结构

---

服务自动重启

• 服务启动，自动检测未完成的待恢复任务，并尝试继续编译
• ~~BackgroundTasks、：~~适合轻量短任务，单线程队列执行，后面的任务会被前面的长任务阻塞
• 开启单独线程执行，多任务并行，不阻塞 API 接口

---

其他一些小tips

• 自动重启按钮：默认开启，因为开始继续编译之前未完成的项目会消耗token，所以设置按钮调节
• 项目在编译期间不能删除，按钮变灰
• 中断任务可删除

生产级别：数据量大，单体项目升级为分布式项目

1. 缓存层

• 项目数据缓存：将频繁访问的项目详情、锚点数据、形式化节点等缓存在Redis中，减少文件I/O操作
• 会话状态缓存：存储用户会话、临时状态等，提升响应速度

1. 消息队列 Redis List/RocketMQ/Redis Pub/Sub

• 任务队列：替代当前的threading，
• 实时通知：通过实现实时状态更新推送，替代轮询
• 分布式锁：使用Redis实现分布式锁，防止并发操作冲突

1. 数据库

• 将当前的JSON文件存储改为规范的关系型数据库表结构

• 利用数据库事务保证数据一致性

• 存储项目的历史状态变更记录

  查询优化

• 支持复杂的统计查询，如项目成功率、处理时长统计等

1. 异步处理-线程-携程

• 将当前的大块pipeline任务拆分为多个小任务（PDF解析、文本翻译、代码生成等）
• 任务优先级：为不同类型的任务设置不同优先级
• 重试机制：内置的重试和错误处理机制
• 进度追踪：实时追踪任务进度和状态

1. 负载均衡与多实例部署

• 水平扩展：部署多个API实例，通过负载均衡器分发请求
  • 将计算密集的pipeline任务部署到性能高的节点上
  • 将静态文件可以存储到便宜、容量大的服务中