https://x.com/i/article/2110267213236113408
约翰霍普金斯「Machine Programming」最新课程：程序综合、代码大模型与智能体，“让机器编程”的前沿研究
约翰霍普金斯大学「Machine Programming」课程
约翰霍普金斯大学 2026 年秋季的研究生课程 EN.601.727「Machine Programming」，由计算机系助理教授 Ziyang Li（个人主页 liby99.github.io） 主讲，TA 为 Qi Sun，CA 为 Yuming Feng。
https://machine-programming.github.io/
课程的核心命题是程序综合（Program Synthesis），让机器自动生成程序。课程副标题式的立场非常鲜明：自动化程序生成正在深刻改变软件的构建方式，而“程序员的意图”如今可以通过三种载体传达给机器：示例（examples）、形式规约（specifications）、自然语言（natural language）。这三种意图表达方式，恰好对应了课程覆盖的两大技术脉络：
•经典符号方法：自底向上的归纳式综合、类型引导/规约引导的枚举综合、交互式综合；这是 MIT Armando Solar-Lezama、UCSD Nadia Polikarpova 等人建立的传统；
•LLM 方法：以大语言模型为核心的代码生成、迭代精化、智能体（agent）、以及 LLM 在定理证明、程序修复、形式验证中的应用。
“Machine Programming”这个术语本身值得注意：它由 Intel 实验室的 Justin Gottschlich 等人提出，指“让机器自己编程”的整个研究领域，意图统一程序综合、代码大模型、自动修复、形式验证等分散的子领域。这门课正是在这个统一视角下设计的，课程没有把“程序综合”和“代码大模型”当成两个割裂的世界，是把它们组织成一条连贯的技术演化叙事：从确定性搜索到神经生成。
课程结构：三模块的技术演化叙事
课程内容分为三个模块、15 周完成，结构本身就是一个精心设计的认知路径。
模块一：程序语言与综合（第 1–2 周） 基础部分
从语法、语义讲起，再到自底向上的归纳式综合（bottom-up inductive synthesis）、类型系统与自顶向下枚举综合、函数式规约与综合。这一部分的技术根基是 FlashFill 一脉的经典工作（微软 Excel 的公式自动填充就是这套技术的产业化成果）：给定输入输出示例，在程序空间中搜索满足约束的程序。涉及的语言/工具是 Python、C、Rust 和约束求解。这部分看似“过时”，实则是理解后续一切的基础：搜索空间、正确性规约、验证条件这些概念，在 LLM 时代不仅没有失效，反而以 reward、test、verifier 的形式全面回归。
模块二：编码大语言模型（第 3–7 周）课程的重心
这是篇幅最大的模块，覆盖面相当完整：
1.推理侧（第 3–4 周）：语言建模用于综合、解码策略与提示工程、迭代精化（iterative refinement）与智能体框架；
2.协议与工具（第 4–5 周）：MCP（Model Context Protocol）单独占了约一周半，这是 2024 年底 Anthropic 发布、如今已成为事实标准的 LLM-工具连接协议，把它纳入正式课程内容，说明课程内容更新到了工业界最前沿；
3.训练侧（第 6–7 周）：编码 LLM 的预训练（两讲）与后训练（SFT 与 RL，一讲）加专题。
从阅读材料看，这一模块的文献覆盖极为系统：模型侧有 Code Llama、StarCoder、DeepSeek Coder、CodeGen、SantaCoder、CodeT5+，基础设施侧有 The Stack 数据集、Fill-in-the-Middle、BPE、RoPE、Multi-Query Attention，训练技术侧还包括 SimCSE、DOBF 这类去噪自监督目标。甚至连 CodeFusion（扩散模型生成代码）和 DALL-E 2 都在列——后者的出现是为了讲授扩散模型原理再迁移到代码域。
模块三：机器编程的应用（第 8–15 周）纵向展开
后半学期不再按方法组织，是按应用领域组织，每个领域一讲：
•形式验证与定理证明（Lean、Coq）LLM 辅助形式化（autoformalization）
•可微编程与机器学习、安全与隐私（CodeQL 漏洞查询）
•硬件与高性能计算、设计/交互式/可视化编程
•神经符号编程（Neurosymbolic Programming，收尾两讲）
涉及语言清单非常能说明课程取向：Python、C、Rust、Lean、CodeQL、PDDL，通用语言、定理证明器、安全查询语言、规划领域语言各占其位。PDDL（规划）的出现尤其体现了"program = plan"的统一世界观。
第 11–14 周被学生口头报告占据，最后以神经符号编程专题收束，这是一个有意味的选择：神经与符号的融合正是整个领域公认的前沿方向，也是这门课两大脉络的自然汇合点。
教学设计：这是一门“研究者的训练课”，不是技能培训课
从评分结构（参与 10% + 口头报告 10% + 三次作业各 15% + 期末项目 35%）和各环节设计看，这门课的定位非常清晰：培养能做研究的人，而非使用工具的人。
三次作业构成一条能力递进线
1.作业一：实现一个枚举程序综合器（9 月 22 日截止）亲手写传统综合器，理解搜索、剪枝、验证的完整闭环；
2.作业二：评估编码 LLM（10 月 9 日截止）学校提供 $200 Amazon Bedrock 额度和 API key，学生系统性地评测真实的大模型；
3.作业三：构建编码智能体 实现基于 LLM 的 agent。
从“综合器 → 评测 → 智能体”，恰好复演了领域本身十五年的演化史。特别值得注意的是作业二的定位：评估（evaluation）被视为与生成同等重要的核心能力，这呼应了阅读清单里庞大的评测文献（HumanEval、MBPP、SWE-bench、LiveCodeBench、BigCodeBench、AlphaCode/CodeContest 等），也是当前学界“基准污染、榜单失真”大讨论下的务实选择。
口头报告：Defender–Attacker 制 迷你学术评审演练
每个学生认领一篇论文，选择两个角色之一：Defender（辩护者）负责讲清论文内容，Attacker（攻击者）以审稿人视角批判论文。每篇论文 20 分钟，六个 session、每场六人。这个设计非常精妙：它强制学生同时练习理解与批判两种学术核心技能，本质上是对真实 peer review 流程的课堂化模拟。课程明确允许选择“网上已有讲稿/视频的论文”以降低准备成本，同时也从七个候选主题中投票选出六个。
期末项目：一篇 NeurIPS 格式的迷你论文
占 35%，三人以内组队，产出包括 2 页 proposal（5%）、实现（20%）、至少 4 页、NeurIPS 2026 模板排版（LaTeX 或 Typst）的报告（5%）、10+5 分钟汇报（5%）。评分权重的分配（实现占 20%）说明课程最看重真做出来的东西。
九个建议选题方向透露了授课者对领域机会的判断，特别有洞察力的几条：
•低资源语言基准：给 Haskell、Prolog、Datalog、Lean、Coq、Z3、Racket、PDDL 这类语言建数据集，测 LLM 的能力边界，这是目前公认的高性价比研究切口；
•高资源语言的窄域：Linux 内核驱动、CUDA、Unreal Engine C++，真实工程场景中 LLM 的短板所在；
•设计 DSL 并测试 LLM 在其中的生成能力 把“综合”问题重新形式化；
•用 LLM 给现有程序综合出形式规约 规约自动生成是形式验证的最大瓶颈；
•LLM 生成代码的漏洞检测 安全方向。
课程明确鼓励把项目做成论文，并给出了去年（Fall 2025）三个成功案例：逻辑学的规模化自动形式化、Elements 证明的忠实形式化、OS 内核规约推断系统 BODHI，三个都是投稿中的论文。这门课的期末项目是一条真实的研究 pipeline 入口，不是课程作业的终点。
一条耐人寻味的 AI 使用政策
课程明确规定：鼓励使用 LLM，但不得让 LLM 代做全部作业；必须理解并能解释自己的代码；需在 acknowledgements.md 中记录与 LLM 的对话过程并随提交附上。在一门教“机器编程”的课上要求记录“人机协作过程”，这既是对诚实学术的底线要求，本身也构成了一种元层面的教学姿态，学生使用 LLM 完成作业的方式，就是课程内容的现场实践。
学术谱系与内容来源
阅读清单末尾列出的四门参考课程，勾勒出这门课的学术血统：
•Armando Solar-Lezama（MIT）的《Introduction to Program Synthesis》，符号综合的源头；
•Baishakhi Ray（Columbia）的《Generative Models for Code》，代码大模型方向；
•Nadia Polikarpova（UCSD）和 Ras Bodik / Emina Torlak（UW）的程序综合课，Bodik 的 CS294 是 SKETCH 与“synthesis for everyone”传统的发源地。
这门 JHU 课程可以视为对以上传统的一次融合与更新：保留了符号综合的严格基础，把重心移到 LLM，再以应用领域和神经符号专题收尾。从 Fall 2025 已有第二个版本迭代、且有“past versions”页面来看，课程本身也在快速演化。
如何评价这门课
第一，叙事结构出色。它没有做成“经典综合 + 大模型”的简单拼盘，是围绕“意图如何传达给机器”这条主线，把 15 年的技术演化组织成可理解的连续体。学生在第 1 周学到的“示例即规约”，与第 12 周接触的“Lean 中的形式化”，共享同一个概念骨架。
第二，内容时效性极强。MCP 协议、SWE-bench、LiveCodeBench、DeepSeek Coder、RL 后训练、Coding Agent（AutoCodeRover、MASAI）全部进入正式教学和作业，课程内容与工业前沿的时间差大约只有一年，这在大学课程里相当罕见，显然得益于授课者本人活跃的研究工作（李子阳的研究方向正是程序综合与代码大模型，典型工作包括 SimpLLM、CoCoMIC、RepoFusion 等仓库级代码模型研究，这些也在阅读清单中）。
第三，研究训练环节设计成熟。Defender–Attacker 报告制、NeurIPS 模板期末论文、$200 云额度支持的真实评测作业、“项目→论文”的成功先例展示，构成了一条完整的研究者养成路径。
给潜在学习者的建议
如果你无法正式修读（课程欢迎旁听，需邮件联系授课者），想沿这条路径自学，这门课的公开材料本身就是一份优秀的学习地图：
1.先攻符号综合基础：读 Solar-Lezama 的课程讲义，理解枚举综合、CEGIS（反例引导的归纳综合）；
2.再系统过代码 LLM：以《A Survey on Language Models for Code》为骨架，按“模型（Code Llama/StarCoder/DeepSeek Coder）→ 数据（The Stack、FIM）→ 评测（HumanEval→SWE-bench→LiveCodeBench 的演化）→ 改进（检索增强、仓库级上下文）”的顺序读论文；
3.动手做三个作业的等价物：写一个迷你综合器、跑一次严肃的模型评测、搭一个编码 agent，这三件事做完，对领域的理解会远超读论文；
4.选一个窄域做期末项目式的练手，低资源语言基准是性价比最高的切口。
一句话总结：这门课把“让机器编程”这个正在重写软件工程的研究领域，组织成了一条从经典程序综合到代码大模型、再到神经符号融合的完整认知路径；它用 Defender–Attacker 报告和 NeurIPS 格式期末项目把自己设计成研究者的孵化器，而不是工具使用者的培训班。对于想进入程序综合 / 代码智能研究方向的人来说，这可能是目前结构最完整、内容最新的公开课程蓝图之一。