代数方法的时间反向推导
Backward through Time, Algebraically
浏览论文内容
中文总结 AI 辅助
针对线性时序逻辑可微语义的浅层嵌入困境，提出代数通用且支持求导的评估引擎，实现多种代数并审计其行为，成果属于PyTorch库telos。
中文摘要 AI 辅助
线性时序逻辑是命题逻辑的模态扩展，可用于描述系统随时间应呈现的行为。其标准应用域为布尔值，但离散值判断对软值系统（神经策略、自适应控制器、序列模型等）的调控作用有限。此类场景下，目标公式的（不）满足情况成为训练信号，可微性成为核心关注点。已有大量候选可微语义，但对其进行处理颇具挑战。现有实现（若存在）多为浅层嵌入，需预先选定单一语义代数及其（通常隐含的）行为。本文将读者设定为一名需应对此困境却拒绝妥协的函数式程序员，由此开发出一种代数通用且支持求导的评估引擎，以及其可接受代数的可执行规范。研究实现并审计了多种代数的正向与反向行为，发现每种代数本质是选择以何种方式、在哪个方向产生“弃权（不执行）”。本文所述及更多内容均属于PyTorch库telos，可在指定网址获取。
英文摘要
Linear temporal logic is a modal extension of propositional logic that allows one to state how a system should behave over time. Its canonical domain is the booleans, but discretely-valued judgements are of little use in steering softly-valued systems (neural policies, adaptive controllers, sequence models, etc). In such cases, the goal formula's (dis)satisfaction becomes a training signal, and differentiability becomes a prime concern. Candidate differentiable semantics abound, but navigating them is tricky. Implementations, where available, are shallow embeddings, demanding an upfront commitment to a single semantic algebra and its (usually implicit) conduct. The paper casts the reader as a functional programmer asked to come to terms with this predicament, and refusing. Out of that refusal comes an evaluation engine that is algebra-generic and amenable to differentiation, together with an executable specification of the algebras it can accept. Various algebras are implemented and audited for their behavior, both forward and backward. Each algebra turns out to be a choice of which direction to disappoint, and how. Everything described (and more) is part of the PyTorch library telos, to be found at https://github.com/konstantinosKokos/telos.
