← 全部专题

形式化方法

从规格与证明到程序推导，探索验证代码生成及其保障边界。

2 篇笔记

从哪里开始

从 Proof-First 的具体示例理解规格与证明，再读 Dijkstra 方法的研究方案。

区分已检查示例、验证所覆盖的规格和待验证的生成方案。Kernel 的统计验证见系统专题。

规格与证明

  1. Proof-First Pipeline

    类型、规格与证明如何约束生成程序的行为？

    研究记录进阶示例与研究方案约 5 分钟

验证代码生成研究

  1. Dijkstra 方法与验证代码生成

    怎样从规格共同推导程序和证明，减少二者的不一致？

    研究记录研究研究方案约 2 分钟

跨专题延伸

  • 训练系统与 Kernel ↗

    把训练计算映射到 GPU 和分布式系统，理解数据布局、通信与性能边界。

  • 应用与 Agent ↗

    用工具调用、检索和结构化输出组织模型工作流程，并保留应用评测记录。

  • 强化学习 ↗

    沿策略梯度、Baseline、Advantage 和策略更新的主线，理解 LLM 如何从反馈中学习。