💻 computer science

ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

ScratchLens 通过将 Scratch 程序编译为因果中间表示、应用规范化和偏序归约以处理并发性，并利用基于 SMT 的细化来提供带有证据的可靠判定，从而引入了一种用于确定 Scratch 程序行为等价性的透镜参数化框架，进而克服了自动评分和修复中语法差异分析及单次运行动态分析的局限性。

原作者： Yuan Si, Jialu Zhang

发布于 2026-06-16

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Yuan Si, Jialu Zhang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一位老师，正在为一班正在学习使用 Scratch（一种色彩鲜艳、基于积木的编程语言）的学生评分。两名学生，Alice 和 Bob，提交的项目在屏幕上看起来完全不同。Alice 重命名了所有的变量，将她的代码拆成了许多细小的碎片，并重新排列了指令。Bob 则保持代码简单，但只改动了一个微小的积木块。

老师面临的大问题是：这两个程序实际上是在做同样的事情，还是其中一个出错了？

这正是这篇论文引入 ScratchLens 的原因。把 ScratchLens 想象成一个超级聪明、神奇的放大镜，它不仅能观察“词汇”（代码积木），还能理解背后的“故事”（行为）。

以下是该论文对这个工具的解释，通过简单的概念进行了拆解：

1. 问题所在：“同样的故事，不同的章节”

在 Scratch 中，你可以用无数种方式讲述同一个故事。

“重命名”的小把戏： 如果 Alice 把一个变量叫做 score（分数），而 Bob 叫它 points（点数），一个简单的计算机程序可能会认为它们完全不同。但人类知道它们是同一个东西。
“单块积木”陷阱： 有时，仅仅改变一个微小的积木（比如删掉一个“等待”指令）就会破坏程序的时序。程序看起来可能仍然在运行，但如果你仔细观察，角色的动作可能会不同步。

现有的工具在这方面表现很差。有些太严格了（仅仅因为代码看起来不同就说“不同！”）；有些则太宽松了（运行一次程序，看到它能跑通，就说“相同！”，即便它实际上已经坏掉了）。

2. 解决方案：“透镜”概念

作者意识到，“等价性”取决于你在观察什么。他们称之为透镜（Lens）。

想象一下通过不同颜色的眼镜看电影：

“最终状态”透镜（Final State Lens）： 你只关心游戏结束时的得分是否一致。（玩家赢了吗？）
“帧”透镜（Frame Lens）： 你关心动画效果。（角色是平滑地滑动，还是瞬间跳跃？）
“事件”透镜（Event Lens）： 你关心时序。（角色是否在音乐开始前等待着开始跳舞？）

ScratchLens 不仅仅给出一个“是/否”的答案。它会说：“在‘最终状态’透镜下，它们是相同的。但在‘帧’透镜下，它们是不同的，因为一个在跳跃，而另一个在滑动。” 这防止了当人们对问题的看法不同时，工具给出令人困惑的答案。

3. 它是如何工作的： “食谱” vs “美食”

它不是通过对比食材清单（代码积木）来工作的，而是通过一种特殊的方式烹饪“美食”并分析“食谱”：

“因果图”（CSIR）： 它将那些彩色的积木转化为一张严格的、数学化的因果关系图。它追踪谁读取了什么，谁写入了什么，以及谁在等待谁。
“魔法排序”（规范化/Canonicalization）： 它获取代码并将其重新组织成一种标准格式。如果 Alice 写的是 A + B，而 Bob 写的是 B + A，工具知道这是同一个数学问题。它会剥离掉“噪音”（重命名、重排序）以观察核心逻辑。
“竞态检测器”（Race Detector）： 在 Scratch 中，很多事情是同时发生的。工具会检查是否有两个动作在争夺同一个资源（比如两个人在同一块白板上书写）。如果是这样，它会将其标记为一个潜在的“竞态条件”（timing bug）。

4. “侦探”模式

如果工具不能 100% 确定，它不会瞎猜。它会像侦探一样使用反例生成器（Counter-Example Generator）：

它会说：“我认为它们不同，但我需要证据。”
然后它会运行一个特定的、有针对性的测试（类似于“压力测试”），看看能否迫使程序表现出差异。
如果测试失败，它会捕捉到错误，并向老师展示具体为什么出错（例如：“缺少‘等待’指令导致角色移动过早”）。
如果它仍然无法证明差异存在，它会诚实地说：“未知（Unknown）”。这至关重要。说“我不知道”总比在可能出错的情况下谎称“它们是相同的”要好。

5. 结果：“满分成绩”

作者在大量的真实学生项目和“变异版”（即故意破坏代码的版本）上测试了 ScratchLens。

测试： 他们对比了 444 对程序。
结果： ScratchLens 达到了 100% 的准确率。
“假阳性”安全性： 最重要的是，它从未声称一个损坏的程序是正确的。在评分的世界里，说一个坏掉的程序是“好的”是最严重的错误。ScratchLens 完全避免了这种情况。
对比： 其他方法（如简单的文本对比、运行几次代码，甚至先进的 AI 聊天机器人）都会犯错。它们要么漏掉了 Bug，要么认为坏掉的代码没问题。ScratchLens 是唯一一个每次都能做对的工具。

总结类比

想象两位厨师提交了蛋糕食谱。

旧工具： 查看食材清单。如果厨师 A 说“糖”，而厨师 B 说“糖精”，它们会说“不同！”或者，它们尝了一口后说“相同！”，即便蛋糕稍后塌陷了。
ScratchLens： 它阅读食谱，理解“糖”和“糖精”在这种语境下可能具有相同的功能，但它也会检查“烘焙时间”是否不同。它会告诉你：“这些蛋糕的味道会一样（最终状态），但厨师 B 的蛋糕会升得更快（帧/事件）。”如果它不确定，它会说：“我需要做一个测试蛋糕来确定，”而不是瞎猜。

论文得出结论：对于编程教学，我们需要能够理解语境（透镜）和因果关系（地图）的工具，而不仅仅是比较文本。ScratchLens 是第一个针对 Scratch 程序完美实现这一点的工具。

技术摘要：ScratchLens：面向 Scratch 程序的透镜参数化行为等价性研究

问题陈述
Scratch 是一种被超过 1.4 亿儿童使用的基于积木的视觉编程环境，它为自动化程序比较带来了独特的挑战。两个 Scratch 程序在语法上可能差异巨大（由于变量重命名、脚本拆分、自定义积木提取或初始化顺序重排），但在行为上却是等价的。反之，一个单积木级的编辑（例如，将一个阻塞式广播替换为异步广播）可能会引入仅在特定调度、随机输入或计时条件下才会显现的差异。

现有的比较方法在此背景下表现不佳：

**树差异化（Tree differencing）**过于严格，会标记那些并未改变语义的语法变化（如脚本边界的变化）。
**单次运行动态比较（Single-run dynamic comparison）**对于并发、随机和依赖时序的行为是不健全的，因为它仅采样了一个调度序列和一个输入轨迹。
**错误等价（False equivalence）**在教育场景中代价尤为高昂，因为它可能会错误地验证一个有缺陷的学生程序，从而过早结束调试过程。

核心难点在于，Scratch 中的行为等价性并非绝对的，而是在观察透镜中具有参数化特征的。例如，“滑行”与“跳跃”可能在最终状态上达成一致，但在帧级视觉轨迹上却存在分歧；两个脚本可能在一个调度下表现一致，但在另一个调度下则会产生分歧。

方法论
作者提出了 ScratchLens，这是一个围绕行为差异分类法和透镜参数化观察模型构建的等价性检查器。

差异分类法（Taxonomy of Divergence）：
系统沿两个轴向组织行为差异：
- 观察透镜（Observation Lenses）： 从具体执行轨迹到特定观察结果的投影（例如：最终状态、帧边界快照、舞台效果、监视器数值、事件因果关系或调试轨迹）。
- 因果现象（Causal Phenomena）： 八个载体族（状态、事件因果、调度敏感性、随机性、时间/帧、克隆生命周期、交互队列、持久输出），它们映射到类型的根因（例如：MISSINGJOINEDGE、UninitializedRead）。
因果中间表示（CSIR）：
Scratch 项目被编译为 CSIR，这是一种关于资源（变量、列表、角色、广播等）和**事务（transactions）**的类型化表示。
- 足迹（Footprints）： 每个事务都会记录类型化的足迹（读、写、消耗、生成、汇合、销毁）。
- 规范化（Canonicalization）： 系统通过使用谱系（usage profiles）和 Weisfeiler–Leman 精炼进行 $\alpha$ -重命名不变的规范化。过程通过对归一化原语的特征值摘要进行比较。
- 轨迹正规型（Trace Normal Forms）： 为了处理并发，ScratchLens 在保守的独立关系上应用 Mazurkiewicz 轨迹正规型。它将程序顺序与竞态条件分离，使得可交换的脚本可以被视为等价，同时保留调度承诺（例如：汇合边）。
比较算法：
算法通过以下层级进行检查：
- 静态等价性： 比较规范特征多重集。如果相等且侧条件封闭，则返回等价性，并附带显式的双射和轨迹商。
- 有界双射搜索： 如果初始谱系持平，则搜索坐标下降双射以最小化解释增量。
- 抽象传递（Abstract Transfer）： 对于 $L_{final}$ （最终状态）透镜，系统检查数值、字符串和列表域上的抽象传递是否证明了等价性，尽管存在结构差异。
- 分类与义务（Obligations）： 不匹配会被分类为类型的根因。条件差异（例如：守卫可行性）会转化为义务。
- 基于插桩 VM 的 CEGAR： 未解决的前沿情况会触发基于反例引导的抽象精化（CEGAR）。系统会在插桩的 Scratch VM 上合成针对性的场景（例如：特定的随机令牌或接收者压力测试运行）来确认或驳回差异。
判定（Verdicts）：
每个确定的判定都携带显式证据：
- 等价： 由双射和轨迹商（或抽象传递）证明。
- 差异： 由类型化的见证（例如：缺失的汇合边）或具体的 VM 反例证明。
- 未知： 对于未解决的前沿情况明确报告，以防止误报等价。

主要贡献

双轴分类法： 一个将因果机制、观察透镜和类型化根因联系起来的 Scratch 程序形式化框架。
透镜参数化等价性： 一种显式考虑观察者的等价性定义，允许同一对程序在不同透镜下得出不同的判定（例如：在 $L_{final}$ 下等价，但在 $L_{frame}$ 下不同）。
CSIR 与比较算法： 一种结合了重命名不变规范化、轨迹正规型以及由 SMT/VM 支持的精化过程的因果中间表示与比较内核。
可复现的评估方法： 一个完全自动化的、由 VM 见证的变异语料库。它包含基于每个透镜的地面真值标签，以及一个“深层组合”层，该层将缺陷隐藏在多层等价保持的重构之下。

结果
系统在包含 444 个验证对（包括 158 个 VM 见证的差异对）和 88 个模糊变异体的语料库上进行了评估。

准确率： ScratchLens 在验证语料库上达到了 1.000 的准确率，且在 158 个标记为“不同”的对中实现了 0 个错误等价声明。
诊断： 它成功恢复了 98.7% 不同对的判定结果及其注入的根因。
基准测试： 结构化、操作码抽象化和仅动态测试的基准方法在特定分类（由分类法预测）上均表现失败（例如：动态测试产生了 28 个错误等价；LLM 产生了 8–15 个）。
消融实验： 移除部分序规约（POR）会增加错误差异；仅限于 $L_{final}$ 会导致召回率大幅下降（0.215），因为事件和帧差异变得不可见。
针对性场景： 在 88 个随机测试无法解决的模糊变异体中，ScratchLens 生成的针对性场景暴露了 14 个随机测试未能发现的具体差异。

意义
论文指出，事件驱动型视觉程序的行为等价性必须是透镜参数化的。单一的二元判定是不够的；观察者（最终状态 vs. 帧轨迹 vs. 事件因果关系）必须是显式的。ScratchLens 证明了通过结合静态因果分析与针对性动态精化，可以实现高精度的等价性检查，从而避免树差异化的误报和单次运行测试的不健全性。这项工作建立了一种“严格评分”的方法论，即优先选择弃权（UNKNOWN）而非错误等价，这是自动化反馈和教育评分系统中至关重要的要求。其发布的成果提供了一个用于语义等价性检查的基准，实现了语义推理与文本差异检测的分离。