提出可证明的元模式发现框架,解决测试中关系识别难题
NOETHER: A Constructive Framework for Metamorphic Pattern Discovery from Operator Algebras
- 基于算子代数构建分层分析框架,从数学结构推导测试关系
- 生成具有代数封闭性和多项式可判定性的元模式集,实证有效
- 适合软件测试、AI验证领域研究者,尤其关注形式化方法的团队
元模式测试被纳入IEEE/ISO标准,但其发展受限于元关系(MR)的识别。现有方法(结构化框架、挖掘与进化管道、大模型辅助、元模式目录)均依赖归纳假设,未解决起源、封闭性与可迁移性三大基础问题。本文提出NOETHER框架:上游为八模块分解,涵盖对称性、序、自伴性、时间反演、极限、定性动力学、方法比较、关系等价等递归数学结构;下游的CONSTRUCT-MP算法在代数封闭性(定理1)和多项式时间可判定性(定理2)上提供保证。在玻尔兹曼反应堆物理、等变机器学习与关系查询优化器三个算子代数领域进行验证:系统化了先前归纳目录;推导出旋转不变性、伴随对偶性、训练轨迹可逆性等可执行元关系;应用关系等价模块。核心可证伪预测(L*-盲于保同构扰动)在限定底物上成立;绝对完备性猜想(定理1')在压水堆扩散问题中被两个独立反例否定,揭示五个平移-扩展维度。结论:归纳从逐程序采样转向领域代数层,下游步骤变为演绎与机械化。
原文摘要 · Abstract (English)
Context. Metamorphic Testing is recognised in IEEE/ISO software-testing standards and increasingly recommended for AI systems, but its progress is bottlenecked by metamorphic relation (MR) identification: existing approaches (structured frameworks, mining and evolutionary pipelines, LLM-assisted methods, MetaPattern catalogues) share an inductive grounding that leaves three foundational questions open: origin, closure, and transferability. Objective. We propose a framework whose downstream step from program-induced operator algebra to MetaPattern set is mechanical and provable, while the upstream curation of the algebra is a stated empirical hypothesis with explicit scope precondition. Method. NOETHER is a two-layer framework. The upstream layer is an eight-block decomposition over recurrent mathematical structures (symmetry, order, self-adjoint, time-reversal, limit, qualitative-dynamics, method-comparison, relational equivalence). The downstream CONSTRUCT-MP algorithm produces a MetaPattern set with algebraic-closure (Theorem 1) and polynomial-time decidability (Theorem 2) guarantees. We test the framework on three operator-algebraic domains. Results. On Boltzmann reactor physics NOETHER systematises a prior inductive catalogue; on equivariant ML it derives executable MRs for rotation invariance, adjoint duality, and training-trajectory reversibility; on relational query optimisers it exercises the relational-equivalence block. The central falsifiable prediction (L*-blindness on homogeneity-preserving mutators) holds on the in-scope substrate. The absolute-completeness conjecture (Theorem 1') is falsified on PWR core diffusion via two pairwise-independent counterexamples that identify five Translate-extension dimensions. Conclusion. Induction is relocated from per-program MR sampling to a per-domain algebraic layer; the downstream step is deductive and mechanical.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。