Source-linked AI summary
Program Synthesis from Polymorphic Refinement Types
Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama
TL;DR
The paper addresses how to synthesize recursive functions from expressive yet decidable specifications that can be decomposed for modular verification. It introduces local liquid type checking and evaluates SYNQUID, which synthesizes complex programs and handles most challenging competing benchmarks with concise, provably correct specifications. The approach remains bounded by refinement expressiveness and guard-type restrictions.
Problem
Program synthesis needs specifications more precise than coarse types, while existing example- and condition-based verification procedures provide less modularity for scalable synthesis.
Method
The paper synthesizes recursive programs from polymorphic refinement types using local liquid type checking with top-down over-approximate propagation, incremental constraint solving, and liquid abduction.
Results
SYNQUID synthesizes complex list and tree programs, including five sorting algorithms and balanced search-tree operations, and handles most challenging benchmarks from competing synthesizers.
Takeaways & Limitations
Refinement-type specifications can provide concise inputs, automatic verification, and provably correct synthesized solutions while supporting modular search over complex programs.
Takeaways & Limitations
Round-trip type checking restricts valid guards to a specified form, excluding guards with function composition and requiring wrapper components for complex predicates.
Abstract
from arXiv · showhide
We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification---and hence synthesis---of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a new algorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.
1. Introduction
The paper presents refinement types as a concise, decidable interface for synthesizing provably correct recursive programs, supported by modular type checking that decomposes specifications and reduces search. Its prototype synthesizes complex data-structure programs and handles most challenging competing benchmarks with concise specifications and correctness guarantees.
- Motivation: Type-based specifications enable modular verification by pruning subprogram candidates independently before complete programs are assembled.This modularity reduces the combinatorial search space and detects type errors early.
- Motivation: Refinement types combine predicates from a decidable logic with polymorphism to express synthesis goals more precisely than coarse-grained types.The replicate signature constrains output length while polymorphism captures the repeated value's behavior.
- Method: Local liquid type checking combines bidirectional information flow, top-down over-approximate propagation, and liquid abduction for modular application and branching checks.Its incremental constraint solving uses MUSFIX to compute the more expensive greatest-fixpoint solutions required by top-down propagation.
- Evaluation: SYNQUID combines local liquid type checking with exhaustive program-term enumeration and evaluates 64 synthesis problems from varied sources.The implementation, benchmarks, and web interface are publicly available from the tool repository.
- Evaluation: SYNQUID synthesizes five sorting algorithms and operations on binary search, AVL, and Red-Black trees, while handling complex invariants and custom data structures.The evaluation identifies local checking's modularity features and MUSFIX as crucial for system performance.
- Evaluation: Compared with existing tools, SYNQUID handles most challenging benchmarks with similar or shorter runtimes, concise specifications, provable correctness, and more complex verification than Hoare-style systems.The comparison spans example-based and Hoare-style synthesizers.
2. Overview
SYNQUID synthesizes recursive programs from polymorphic refinement-type specifications by decomposing goals, inferring local requirements, and checking candidates modularly. The approach supports complex data-structure programs and reduces synthesis effort through incremental refinement checking and early filtering.
- Specification and Language: SYNQUID defines synthesis problems using a goal refinement type, typing environment, and logical qualifiers.The environment supplies available components and path conditions, while qualifiers build unknown refinements and branch guards.
- Specification and Language: The system combines candidate enumeration with recursive decomposition into simpler subproblems, then validates assembled candidates through subtyping constraints.Decomposition may be incomplete, so final constraint checking determines whether the combined term has the desired type.
- Evaluation and Scope: SYNQUID synthesizes complex list and tree programs, including five sorting algorithms and operations on binary search, AVL, and Red-Black trees.Its evaluation also reports that disabling early filtering increases one example’s synthesis time from less than two seconds to over two minutes.
- Evaluation and Scope: Refinement types have a scope boundary: decidable refinements cannot fully specify every program, and some specifications may be cumbersome compared with examples or richer languages.Abstract refinements extend expressiveness to properties such as the order of list elements.
- Higher-Order Synthesis: Higher-order combinators such as map and fold allow SYNQUID to infer auxiliary-function requirements from the main program’s refinement specification.For insertion sort, the inferred auxiliary signature describes inserting an element into a sorted list, enabling independent synthesis of that function.
3. The SYNQUID Language
SYNQUID combines round-trip refinement-type checking with incremental constraint solving to support modular, sound program synthesis from polymorphic specifications.
- Syntax and Types: SYNQUID types include refined scalar types, dependent function types, polymorphic schemas, and user-defined datatypes.Type variables are restricted to scalar types, a limitation the authors found not too restrictive in practice.
- Round-Trip Type Checking: Round-trip checking propagates approximate goal information top-down, then reconstructs stronger types bottom-up for local verification.This extends bidirectional checking and retains useful goal information when perfect decomposition is unavailable.
- Type System Extensions: Function-application rules decompose higher-order goals, while condition abduction infers branch assumptions that can specify conditional guards.Match abduction adds efficient pattern matching when scrutinees satisfy liquid-type restrictions, otherwise reverting to the original rule.
- Soundness and Completeness: The system is sound, and completeness is established relative to bottom-up liquid type inference, with a weakened system needed when termination cannot be shown.Synthesis inherits soundness because candidates are constructed with round-trip typing derivations.
- Local Liquid Type Checking: Local liquid checking solves refinement subtyping incrementally using Horn constraints and greatest-fixpoint reasoning.Incremental unification supports early error detection, while MUSFIX addresses the smallest-predicate search needed by Strengthen.
- Synthesis: Synthesis rules reinterpret round-trip checking judgments with unknown terms, constructing programs by recursively applying rules whose conclusions match the goal schema.Soundness follows from the underlying checking system; completeness relies on rewriting programs into the restricted conditional form explored by synthesis.
4. Evaluation
The evaluation uses 64 synthesis challenges spanning prior benchmarks and independent verification case studies to assess expressiveness, concision, usability, scalability, and feature impact. SYNQUID fully synthesized and verified all benchmarks, handled complex programs, and generally offered concise specifications and competitive performance.
- Benchmark suite: 64 synthesis challenges span prior synthesizer benchmarks and independent LiquidHaskell verification case studies.The suite includes three especially complex expressible challenges from each source paper, plus easier or particularly interesting problems.
- Evaluation measures: The benchmarks measure synthesis goals, components, measures, specification and code size, and multiple synthesis-time configurations.Reported timing variants include minimal and default exploration bounds, plus disabled round-trip checking, consistency checking, and MUSFIX.
- Overall results: SYNQUID synthesized and fully verified solutions for all 64 benchmarks.The evaluation reports solution sizes in AST nodes and synthesis times in seconds.
- Scalability and concision: All but 7 benchmarks finished within 5 seconds, while synthesized programs included red-black tree insertion of size 69 and a binary heap constructor of size 246.Specifications for three main binary-search-tree operations were over six times more concise than their implementations.
- Scalability and concision: With shared default exploration bounds, only three benchmarks exceeded the two-minute timeout.Using common bounds inevitably slowed synthesis, but penalties were not drastic on most benchmarks.
- Ablation results: Removing MUSFIX or round-trip type checking caused 37 or 33 of 64 benchmarks, respectively, to time out.Consistency checks produced significant speedups mainly on the most complex examples.
- Comparative evaluation: Type-based specifications were reported as more concise than competing specifications and less laborious than bulky input-output examples for binary-search-tree insertion.The authors also argue that refinement types suit operations with complex representation invariants but simple abstract effects.
- Comparative evaluation: SYNQUID solved all problems tackled by the compared formal tools and synthesized some benchmarks requiring invariant discovery unsupported by them.On shared benchmarks, the authors report considerably smaller running times.
5. Related Work
SYNQUID combines refinement-type synthesis with ideas from recursive functional-program synthesis and refinement-type inference. Related systems differ in specification form, type expressiveness, verification power, and abduction scope.
- Positioning: The paper combines recursive functional-program synthesis with refinement type inference, extending type-directed synthesis with general decidable refinement types.The authors position this as the first use of general decidable refinement types for synthesis.
- Recursive functional synthesis: MYTH uses bidirectional type checking but lacks polymorphism and refinement types, relying instead on input-output examples.Examples can be easy for some functions but do not fully specify programs in general.
- Recursive functional synthesis: MYTH2 reduces example verbosity through singleton, intersection, union, and parametric polymorphic types, but lacks dependent function types for full specification of many interesting programs.The paper suggests combining these features with SYNQUID’s dependent types as future work.
- Formal verification: LEON uses recursive first-order specifications and semi-decision-based verification but lacks invariant inference for examples such as sorted-list or binary-search-tree insertion.Its general strategy also decomposes specifications before switching exploration methods.
- Adjacent approaches: Hole-driven systems such as Agda, Idris, and Djinn use rich types interactively for development rather than performing complete synthesis.Type-directed code-completion systems make different trade-offs because their problems are highly under-constrained.
- Refinement type checking: SYNQUID integrates liquid type inference with bidirectional checking, using greatest-fixpoint predicate abstraction as a distinguishing refinement-type design choice.The related-work discussion contrasts this with earlier liquid-type approaches.
- Logical abduction: SYNQUID’s predicate-abstraction and MUS-enumeration abduction applies more broadly than restricted quantifier-elimination or theory-specific methods, but is limited by the available logical qualifiers.The paper characterizes the trade-off as broader applicability versus lower precision.
A. Soundness and Completeness of Round-trip Type Checking
The appendix compares round-trip type checking with bottom-up liquid type inference, using bidirectional checking as an intermediate system.
- Comparison framework: Round-trip type checking is evaluated relative to bottom-up liquid type inference through a bidirectional type-checking system.The comparison establishes the intermediate formalism used in the appendix.
A.1 Soundness of round-trip type checking
The appendix proves soundness of round-trip type checking by relating it to bidirectional checking and then to bottom-up typing. The theorem establishes that a round-trip derivation yields an inferred type that is a subtype of the checked goal.
- Soundness theorem: Theorem 1 states that a round-trip derivation produces an inferred type S′ satisfying S′ <: S under the stated well-formedness assumptions.This is the central soundness guarantee for the round-trip system.
- Proof structure: Round-trip checking performs subtyping checks more locally than bidirectional checking while subsuming its boundary check.The correspondence is established by induction over the derivation structure and matching rules.
- Proof structure: The proof first translates round-trip derivations into bidirectional derivations while preserving inferred types for expression terms.Lemma 2 gives the round-trip-to-bidirectional direction.
- Proof structure: It then translates bidirectional derivations into bottom-up typing derivations and preserves the subtype relation between inferred and checked types.The bottom-up correspondence is used to establish the final soundness property.
- Proof structure: The conclusion follows by combining the round-trip-to-bidirectional and bidirectional-to-bottom-up lemmas.The appendix explicitly identifies this combination as the proof of Theorem 1.
A.2 Completeness of round-trip type checking
Theorem 2 establishes completeness of round-trip type checking by composing translations from bottom-up to bidirectional judgments and from bidirectional to round-trip judgments. The latter translation handles early subtyping checks through induction over application, let, branching, and other rules.
- A.2 Completeness of round-trip type checking: Theorem 2 states that every bottom-up typing derivation yields a derivation in the termination-oblivious round-trip system.The theorem follows directly by combining Lemma 4 and Lemma 5.
- A.2 Completeness of round-trip type checking: The completeness proof proceeds in two stages: bottom-up derivations become bidirectional derivations, which then become round-trip derivations.The second stage shows that early checks on incomplete applications reject only terms that the bidirectional system would later reject.
- A.2 Completeness of round-trip type checking: Lemma 4 constructs bidirectional derivations by replacing inference judgments for I-terms with checking judgments and handling applications by argument form.For function-term arguments, the inferred context is empty because abstraction does not generate contextual types; subtyping then supplies the required application premise.
- A.2 Completeness of round-trip type checking: Context-free inference rules translate straightforwardly because their premises are contained in the corresponding bidirectional checking rules.This provides the routine cases of the bottom-up-to-bidirectional direction.
- A.2 Completeness of round-trip type checking: Lemma 5 lifts bidirectional derivations to round-trip derivations by selecting suitable goal types and proving the required subtyping relations.The proof treats first-order and higher-order applications, let expressions, conditionals, and matches; most remaining rules share the same shape across systems.