编译通过，不等于它是对的

编译通过，不等于它是对的

牛顿被苹果砸中的故事里，真正的工序其实有两步：先看见苹果落地，再把这件事变成一条万有引力定律。物理学家几百年干的都是第二件事——把现象翻译成方程。港大团队牵头的一篇论文（MMFormalizer，arXiv 2601.03017）把这道工序交给了 AI：给它一张图——几何图、物理题的示意图、甚至手绘草图——它把图里的圆、线段、箭头，连同图上看不见的东西，一层层写成编译器能验证的形式化命题。

这个方向有个学名叫自形式化（autoformalization）：把人话写成的数学，翻译成 Lean 这类证明助手能读懂、能检查的语言。以前大家做的是纯文本的翻译，这篇论文往前推了一步：物理世界的题目天生带着图，而图里的信息是不完整的。一张斜面滑块的示意图，图上没有质量，没有摩擦系数，更不会画着「能量守恒」四个字——这些看不见的约束，得靠模型从视觉元素和领域知识里推断出来。论文管这个过程叫递归接地（recursive grounding）：先把图里的东西识别成基本原语（点、线段、角度、质量、温度），再用领域公理把原语一层层组装成命题链，每一步抽象都要有视觉证据撑着，最后由一个终止条件决定什么时候停下。质量、电荷、普朗克常数这些物理量各有各的接法，接不上就继续拆，拆到底才编译。

论文说，这是第一个能同时覆盖哈密顿经典力学、相对论、量子力学和热力学的多模态自形式化方法。配套放出了一个新基准 PhyX-AF：从 MathVerse、PhyX 和两类几何数据里精挑了 115 道题，专门考「看图形式化」这一件事。附录里的案例清单像一份物理课大纲——牛顿三定律、量子隧穿、相对论、正六棱柱，还有一个失败案例。视频里那个苹果的开场梗，大概就是从这里来的。

但真正值得看的不是翻译演示，而是成绩单上的一个缺口。论文对每个翻译结果查三道关：编译器过不过（Compile）、语义对不对（Semantics）、人工核验认不认（Human Check）。这三道关之间的落差，比任何单关的数字都扎眼。最强的 GPT-5 在 MathVerse 的图像题上，编译通过 24%，语义正确 20%，人工核验只剩 12%——三道关一路腰斩。也就是说，编译器点头的翻译里，差不多一半语义跑偏，再核下去对的更少。编译器只检查类型和语法，不检查物理世界是否真是这样：把「小球下落」写成「小球匀速上升」，只要类型写对了，编译照样通过。

其他几条成绩单线索也值得记下。几何是全场最难的域：合成几何和解析几何上，所有模型的精度都明显掉下来，模型对具体的长度和角度关系仍然抓不准，遇到训练时没见过的图形分布就更不行。图像和文本两个模态之间的缺口也大：同一个模型，文本题的成绩常常是图像题的好几倍。最强开源模型 Qwen3-VL-235B 在物理域和分布外的合成几何上几乎全军覆没。

消融实验里有几个反直觉的发现。一个是：在模型没见过的合成几何上，把从定理库里检索来的参考代码撤掉、让模型自由合成，成绩反而显著上升——给参考答案会锁死输出空间，不给反而泛化更好。另一个是：不写清楚递归的终止条件，递归树会长得又深又大，最后整个综合过程直接失败——「知道什么时候停」不是工程细节，是成败线。带图接地在相对论和量子这类硬域上提升明显，多采样几条路径（pass@k）也能换到分数。

还有一条容易被略过的发现：语义检查这一环，最弱的 Qwen2.5-VL-72B 去监督开源最强模型生成的代码，成绩与最强的 Gemini-3-Pro 打平。检查比生成便宜，弱模型也能当好审稿人——这句结论对做 agent 系统的人应该不陌生。

这篇论文挂在 arXiv 上的时间是今年 1 月 6 日，比不少视频里呈现的「最新突破」早了九个月。九个月里它没有被推翻，也没有被大规模用起来——因为三级检查的缺口摆在那里。形式化这件事的意义本来就不在一道题的对错，而在于它把「模型说的」变成「编译器可判的」，让下一步的验证有了抓手。但 PhyX-AF 的数字提醒我们，翻译成可验证的形式只是把问题搬了个地方：从「读不懂」搬到「编译过了但未必真对」。第一关的门牌已经挂好，后面两关的门槛，还是 12% 对 24% 的距离。