PL/FM/SE Seminar Series: Chentian Wu, "Efficient Meta-Synthesis for Finite-Aspect Checkable Languages."

Abstract: Inductive learning has achieved remarkable success, yet state-of-the-art synthesizers remain heavily domain-specific, requiring extensive manual engineering to adapt to new domains. Existing generic meta-synthesis frameworks attempt to unify this process but typically suffer a severe performance penalty. In this paper, we present Loom, an efficient meta-synthesis framework for Finite-Aspect Checkable (FAC) languages. To interface with Loom, we introduce Facet++, a synthesis-oriented specification language for describing FAC concept languages and corresponding inductive learning problems. Loom compiles Facet++ problems into the SyGuS-BV theory. By encoding finite evaluation aspects as bit-vectors, Loom achieves massive bit-level parallelism, evaluating multiple examples simultaneously via SIMD-like parallelism/optimization. Evaluated across six diverse domains on thousands of inductive learning problems, the generic Loom synthesizers consistently match and frequently outperform heavily engineered, domain-specific state-of-the-art tools, shattering the conventional wisdom that generic frameworks must sacrifice performance.