Occam Learning Meets Synthesis Through Unification

TL;DR

This paper introduces PolyGen, a new program synthesis solver with theoretical generalizability guarantees based on Occam learning, demonstrating superior performance on conditional linear integer arithmetic compared to existing solvers.

Contribution

The paper unifies Occam learning theory with synthesis through unification, designing PolyGen with proven generalizability and improved performance on CLIA domains.

Findings

PolyGen outperforms Eusolver and Euphony on CLIA in generalizability.

PolyGen demonstrates higher efficiency in synthesis tasks.

Theoretical guarantees of generalizability are established for PolyGen.

Abstract

The generalizability of PBE solvers is the key to the empirical synthesis performance. Despite the importance of generalizability, related studies on PBE solvers are still limited. In theory, few existing solvers provide theoretical guarantees on generalizability, and in practice, there is a lack of PBE solvers with satisfactory generalizability on important domains such as conditional linear integer arithmetic (CLIA). In this paper, we adopt a concept from the computational learning theory, Occam learning, and perform a comprehensive study on the framework of synthesis through unification (STUN), a state-of-the-art framework for synthesizing programs with nested if-then-else operators. We prove that Eusolver, a state-of-the-art STUN solver, does not satisfy the condition of Occam learning, and then we design a novel STUN solver, PolyGen, of which the generalizability is theoretically guaranteed by Occam learning. We evaluate PolyGen on the domains of CLIA and demonstrate that PolyGen significantly outperforms two state-of-the-art PBE solvers on CLIA, Eusolver and Euphony, on both generalizability and efficiency.