用布尔集合覆盖加速时序逻辑公式的自动学习，速度超百倍。
LTL$_f$ Learning Meets Boolean Set Cover
- 将布尔集合覆盖作为组合逻辑公式的子程序
- 在70%基准上提速超100倍，公式更小或相当
- 适合需要快速生成简洁时序逻辑的AI与系统验证场景
从有限轨迹中学习线性时序逻辑（LTLf）公式是人工智能、软件工程、形式化方法、网络物理系统控制及机器人等领域中的基础研究问题。我们实现了一款名为Bolt的新CPU工具，相比现有最佳方法，在70%的基准测试中学习速度提升超过100倍，且98%的情况下生成的公式规模更小或相当。核心思路是利用布尔集合覆盖问题作为子程序，通过布尔连接词组合已有公式。得益于该组件，本方法在效率与公式大小之间提供了新颖的权衡。
原文摘要 · Abstract (English)
Learning formulas in Linear Temporal Logic (LTLf) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and robotics. We implement a new CPU tool called Bolt improving over the state of the art by learning formulas more than 100x faster over 70% of the benchmarks, with smaller or equal formulas in 98% of the cases. Our key insight is to leverage a problem called Boolean Set Cover as a subroutine to combine existing formulas using Boolean connectives. Thanks to the Boolean Set Cover component, our approach offers a novel trade-off between efficiency and formula size.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。