viable/strict/1786348800: Fix Z3 translation validation for torch.sym_not (#185147)
PyTorch 的 torch.fx.experimental.validator.z3op 未翻译 torch.sym_not，导致 shape-env 图中的符号布尔取反在验证时回退到 Python not，引发 Z3Exception。修复将 torch.sym_not 映射到 z3.Not，并加入布尔参数集，同时移除 baddbmm 测试中的过时 expected-failure 标记。
Development
- First Reportviable/strict/1786348800: Fix Z3 translation validation for torch.sym_not (#185147)PyTorch Core
- Industry Responsetrunk/be9f8ddc6cecb14c60078b128fa3f3bed42185f7: Fix Z3 translation validation for torch.sym_not (#185147)PyTorch Core
- Current AssessmentPyTorch 持续完善其动态形状验证基础设施，这反映了框架对符号形状和编译正确性的重视。此类修复有助于提升 PyTorch 在动态形状场景下的可靠性，对依赖 torch.compile 和动态形状的深度学习项目有积极影响。Agent Pulse · analysis
PyTorch 修复了 Z3 翻译验证中 torch.sym_not 未处理的问题。此前 z3op 只翻译 operator.not_，而 shape-env 图可能记录 torch.sym_not 的符号布尔取反，导致验证器回退到公共辅助函数，该函数使用 Python not 尝试将 z3.BoolRef 转换为具体布尔值，从而抛出 Z3Exception。修复方案是在 z3op 中将 torch.sym_not 映射到 z3.Not，并将其加入布尔参数集以一致处理字面整数操作数。同时移除了 baddbmm 标量参数测试中过时的动态 expected-failure 标记。该修复避免了将验证器知识泄漏到公共符号辅助函数中，与现有 torch.sym_* 函数的处理方式保持一致。
该修复表明 PyTorch 的符号形状验证器需要显式处理每个 torch.sym_* 操作，否则会回退到 Python 语义导致 Z3 异常。将 torch.sym_not 映射到 z3.Not 并加入布尔参数集，确保了符号布尔取反在验证时被正确翻译。这提示开发者在使用 torch.sym_not 时需注意验证器的覆盖范围，未来可能需扩展更多符号操作。
PyTorch 持续完善其动态形状验证基础设施，这反映了框架对符号形状和编译正确性的重视。此类修复有助于提升 PyTorch 在动态形状场景下的可靠性，对依赖 torch.compile 和动态形状的深度学习项目有积极影响。
该修复提升了 PyTorch 动态形状验证的稳定性，减少了因符号操作未处理导致的异常，从而降低开发者在动态形状场景下的调试成本，增强 PyTorch 作为深度学习框架的可靠性。
未来可能看到更多 torch.sym_* 操作被纳入 Z3 验证器，以减少验证回退。开发者应关注 PyTorch 对符号操作验证的覆盖进展，以利用更可靠的动态形状支持。