stl2vec：时序逻辑的语义化与可解释向量表示

基于摘要分析。该研究针对离散符号知识与连续机器学习计算之间的表示鸿沟，提出 stl2vec，将 Signal Temporal Logic（STL，信号时序逻辑）公式映射为连续向量，以支持在公式语义空间中进行学习与优化。其主要研究对象是逻辑公式的表示，而非 EEG 信号或 BCI 解码。 核心机制是从基本原理定义公式嵌入，而非通过训练学习嵌入。作者称，该表示具有有限维、反映公式语义、无需学习和可解释四项性质。摘要未给出语义相似性的具体定义、嵌入计算公式、维度选择或可解释性的验证方式，这些内容尚需全文核对；“无需学习”仅指嵌入本身，不意味着下游模型无需训练。 作者报告了两类应用：一是学习模型检验，预测随机过程满足给定要求的概率；二是将嵌入接入神经符号框架，约束深度生成模型的输出符合指定逻辑规范。摘要未提供数据、对照基线或定量结果，因此尚不能判断性能增益、约束满足程度及计算成本；实验协议、消融及统计信息尚未验证。 平台推测（待验证）：若 EEG 任务能够明确写成关于可观测时序特征的 STL 规范，该表示可能用于编码时序先验或组织约束条件，而非直接替代信号特征提取器。该假设依赖可计算的时序谓词及有效规范；可复用部分是公式嵌入，需改造部分包括 EEG 特征到谓词的映射及下游约束接口。低信噪比、跨被试差异和通道变化可能使谓词不稳定，小数据下规范也可能难以校准。一个小规模检验可在固定 EEG 任务与数据划分下，比较同一下游模型加入或不加入 STL 嵌入时的任务指标和规范满足率，并施加时序扰动检查稳健性。已有 EEG 相关工作尚未检索确认。