paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Learning formulas in finite variable logics

有限变量逻辑中的公式学习
POPL 6(POPL)2022匹配度 3/10 · 论文属于程序合成与逻辑/自动机理论,研究有限变量逻辑中语法受限公式与项的精确学习及合成,与用户关注的静态分析、LLM/Agent 结合、浮点程序分析和贝叶斯程序分析均无直接关系;且偏纯理论,缺乏工程实现与工业落地线索。引用 5 inbox
Paul Krogmeier, P. Madhusudan
crossref: 2026-09-10

AI 速览

一句话:提出通用自动机理论技术,在有限变量逻辑中实现语法受限的公式与项精确学习、可实现性判定和合成。

本文研究有限变量逻辑中语法受限的公式与项精确学习问题:给定一组被正标记和负标记的有限结构,目标是学习一个公式或项,使其恰好分类这些结构。作者提出一种新颖且通用的自动机理论技术,将公式学习、可实现性判定与合成转化为自动机问题,并针对该问题给出算法以及复杂度上界和下界。该技术还被成功扩展至带最小不动点定义的一阶逻辑、高阶逻辑,以及查询与递归定义函数的项合成等变体。评估以理论结果为主,展示了方法在多种逻辑和学习问题上的适用性。

问题
如何在有限变量逻辑中,以语法受限方式从正负标记结构精确学习公式或项,并判定其可实现性与完成合成。
方法
提出一种通用的自动机理论技术,将公式学习与合成问题归约为自动机问题,并给出相应算法及复杂度上下界。
评估
以理论分析为主,给出可实现性与合成的上界和下界,并展示该技术可扩展到最小不动点一阶逻辑、高阶逻辑及递归函数项合成等变体。
原文摘要(Abstract)

We consider grammar-restricted exact learning of formulas and terms in finite variable logics. We propose a novel and versatile automata-theoretic technique for solving such problems. We first show results for learning formulas that classify a set of positively- and negatively-labeled structures. We give algorithms for realizability and synthesis of such formulas along with upper and lower bounds. We also establish positive results using our technique for other logics and variants of the learning problem, including first-order logic with least fixed point definitions, higher-order logics, and synthesis of queries and terms with recursively-defined functions.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1553,
  title = {Learning formulas in finite variable logics},
  author = {Paul Krogmeier and P. Madhusudan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {POPL},
  year = {2022},
  doi = {10.1145/3498671}
}