PaperlayerView exact revision on arXiv

Source-linked AI summary

A Theory of Formal Synthesis via Inductive Learning

Susmit Jha, Sanjit A. Seshia

arXiv:1505.03953v4cs.AIcs.FL

TL;DR

Formal inductive synthesis seeks programs that satisfy formal specifications, but its relationship to traditional machine learning and the behavior of its oracle-guided methods call for theoretical characterization. The paper formalizes OGIS and analyzes CEGIS variants, finding that their synthesis power differs with counterexample type and learner memory. It also relates finite-class convergence to teaching dimension.

  • Problem

    Formal inductive synthesis and machine learning share the goal of learning concepts from observations, but differ in their problem formulations and techniques, motivating a theoretical framework for formal synthesis.

    Source: §1 · p. 2

  • Method

    The paper formalizes OGIS and theoretically analyzes CEGIS for recursive languages across counterexample types and bounded or unbounded learner memory.

    Source: §1 · pp. 2–3, §4 · p. 12

  • Results

    CEGIS variants can have different synthesis power, especially with bounded-memory learners, and finite-class termination bounds connect to teaching dimension.

    Source: §1 · p. 3, §7 · p. 27

  • Takeaways & Limitations

    The results provide a first step toward a theoretical foundation for formal inductive synthesis.

    Source: §7 · p. 27

    The analysis focuses on convergence in the limit and does not address synthesis computational complexity or how counterexample type affects convergence speed.

    Source: §2.3 · p. 10

Abstract

from arXiv · show

Formal synthesis is the process of generating a program satisfying a high-level formal specification. In recent times, effective formal synthesis methods have been proposed based on the use of inductive learning. We refer to this class of methods that learn programs from examples as formal inductive synthesis. In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how formal inductive synthesis differs from traditional machine learning. We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a family of synthesizers that operate by iteratively querying an oracle. An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS). We present a theoretical characterization of CEGIS for learning any program that computes a recursive language. In particular, we analyze the relative power of CEGIS variants where the types of counterexamples generated by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning algorithm. In the special case where the universe of candidate programs is finite, we relate the speed of convergence to the notion of teaching dimension studied in machine learning theory. Altogether, the results of the paper take a first step towards a theoretical foundation for the emerging field of formal inductive synthesis.

1 Introduction

Formal inductive synthesis learns programs from examples while emphasizing correctness, against a backdrop of growing interest in synthesizing systems from formal specifications. The paper frames OGIS as a theoretical framework for these methods and studies how oracle queries and learner resources shape CEGIS.

1 Introduction

  • Formal synthesis builds on advances in verification and program synthesis, with applications including integrated-circuit design, software bug finding, embedded-system analysis, and security vulnerability discovery.The passage names SAT solvers, BDDs, and SMT solvers among the computational reasoning engines at the heart of these advances.Source: §1 · p. 1
  • Formal inductive synthesis searches a restricted program space to find a program matching input-output examples, with correctness of the synthesized artifact emphasized.The paper contrasts this with deductive synthesis, which constructs a program by proving a theorem.Source: §1 · pp. 1–2
  • Unlike traditional machine learning, formal inductive synthesis targets general programs or automata, seeks exact specification-compliant learning, and treats oracle design as part of the synthesizer.Traditional machine learning more often uses specialized concept classes, approximate learning, and examples drawn from a corpus.Source: §1 · p. 2
  • OGIS unifies oracle-querying synthesis methods, with variations in concept-class characteristics, query types, and resources available to the learning engine.The paper focuses on CEGIS, comparing counterexample types and bounded versus unbounded memory, and connects finite-class convergence to teaching dimension.Source: §1 · pp. 2–3
  • For unbounded-memory learners, arbitrary and minimal counterexamples have equal synthesis power, exceeding positive-example-bounded counterexamples; with bounded memory, the bounded variant is incomparable to them.The paper also reports NP-hardness for solving finite-domain formal inductive synthesis over finite concept classes, and a teaching-dimension lower bound on CEGIS counterexamples needed to terminate.Source: §1 · p. 3

2 Oracle-Guided Inductive Synthesis: OGIS

This section presents OGIS as a framework for synthesis through learner–oracle interaction under an explicit specification, situating existing methods and setting up comparisons of CEGIS variants by counterexample type and learner memory. It also discusses convergence for finite concept classes and how convergence speed relates to learning-theory dimensions.

2 Oracle-Guided Inductive Synthesis: OGIS

  • Formal inductive synthesis seeks a concept from examples that satisfies an explicit specification, with the example domain and specification accessible only through an oracle interface.A specification may allow multiple correct concepts rather than a single one.Source: §2 · pp. 4–5

2.1 OGIS: A family of synthesizers

  • OGIS pairs a learner proposing concepts and queries with an oracle answering through an interface; convergence depends on query types, learner strategy and resources, and oracle design.The oracle can report when the learner has found a correct concept.Source: §2.1 · pp. 5, 6, 8

2.2 Examples of OGIS

  • OGIS instances include DFA learning with membership and equivalence queries, CEGIS with witness and counterexample queries, and distinguishing-input synthesis when specifications are unavailable or costly to verify.Generalized CEGIS can also use correctness, crafted-correctness, and membership queries.Source: §2.2 · pp. 8–9

2.3 Counterexample-Guided Inductive Synthesis (CEGIS)

  • For infinite recursive-language programs, CEGIS variants compare arbitrary, minimal, constant-bounded, and positive-history-bounded counterexamples under finite or infinite learner memory.The analysis asks whether synthesis converges to the correct program in the limit, not about computational complexity or convergence speed.Source: §2.3 · pp. 9–10
  • OGIS complexity for finite concept classes is related to Vapnik–Chervonenkis dimension [12] and teaching dimension [20].The paper presents an initial complexity analysis for this setting.Source: §2.3 · p. 10
  • For finite program classes, decidability is trivial because convergence is guaranteed when queries provide new examples or information about the target program.The speed of convergence remains relevant even when convergence is guaranteed.Source: §2.3 · p. 10

3 Background and Related Work

This section situates OGIS among formal synthesis and learning frameworks, contrasting what each formalizes and how it treats oracles, language learning, and teaching.

3.1 Formal Synthesis

  • The paper complements SyGuS: SyGuS formalizes the synthesis problem, while OGIS formalizes common solution techniques and analyzes CEGIS variants.The paper notes that many synthesis efforts use syntactic restrictions and inductive synthesis from examples.Source: §3.1 · pp. 10–11

3.2 Machine Learning Theory

  • Unlike query-based learning, OGIS treats designing or selecting the oracle as part of the synthesis procedure and proves results broadly for programs corresponding to recursive languages.Query-based learning typically specifies a black-box oracle as part of the problem and establishes results for particular concept classes.Source: §3.2 · p. 11

3.3 Learning of Formal Languages

  • Classical formal-language learning studies identification from an infinite stream of examples, distinguishing learning from positive-only text and from positive-and-negative informants.Gold's model assumes unbounded memory; none of the standard language classes cited, including regular and context-free languages, are identifiable in the limit from positive examples alone.Source: §3.3 · p. 11
  • Prior work relates query-based and Gold-style learning, while this paper uses OGIS to study how oracle and counterexample types affect learning programs or languages.The cited results include simulation of superset-query learners using positive data, but not subset-query learners in general.Source: §3.3 · pp. 11–12

3.4 Learning vs. Teaching

  • The paper relates finite-class OGIS sample bounds to teaching literature but assumes no particular inductive learning technique for the synthesis engine.Its aim is to bound how many oracle-provided examples are needed to synthesize the correct program.Source: §3.4 · p. 12

4 Theoretical Analysis of CEGIS: Preliminaries

The section formalizes CEGIS for recursive languages under partial trace-property specifications, then defines its oracle, learner, and convergence models. It distinguishes counterexample policies and learner memory bounds.

4 Theoretical Analysis of CEGIS: Preliminaries

  • The analysis specializes formal inductive synthesis to recursive languages and partial trace-property specifications, while noting that most results extend to more general specifications.Source: §4 · p. 12, §4.1 · p. 13

4.1 Basic Notation

  • Languages are identified by total Boolean programs, and syntactically different programs count as equivalent when they identify the same language.Source: §4.1 · p. 13
  • An indexed family encodes candidate languages with a recursive TEMPLATE, while a total order on behaviors models oracle preferences such as returning the smallest counterexample.Source: §4.1 · p. 13

4.2 CEGIS Definitions

  • CEGIS uses positive-witness and counterexample queries: the oracle supplies target-language examples and may return a counterexample refuting the current candidate.Source: §4.2 · pp. 14–15
  • The analysis compares arbitrary, minimal, constant-bounded, and positive-bounded counterexample policies.Source: §4.2 · pp. 15–16
  • Infinite-memory learners use response sequences, whereas finite-memory learners update candidates from the previous candidate and new responses.Source: §4.2 · p. 16
  • Identification requires convergence to the target after a finite transcript prefix for every valid transcript; under the specified partial trace setting, identifying the specification coincides with identifying its target language.Source: §4.2 · p. 17

5 Theoretical Analysis of CEGIS: Results

This section compares CEGIS variants for infinite language classes, varying counterexample type and learner memory. Its results characterize which variants identify the same or different language classes, under a focus on partial trace-property specifications.

5.1 Finite Memory Inductive Synthesis

5.1.1 Minimal vs. Arbitrary Counterexamples

  • With finite memory, minimal and arbitrary counterexamples yield equivalent synthesis power: mincegis = cegis.A finite-memory learner can recover the minimal counterexample through repeated calls to the arbitrary-counterexample verifier.Source: §5.1.1 · pp. 18–19

5.1.2 Bounded vs. Arbitrary Counterexamples

  • With finite memory, bounded-counterexample synthesis is strictly weaker than arbitrary-counterexample synthesis: cbcegis ⊂ cegis.Source: §5.1.2 · p. 19
  • With finite memory, positive-bounded and arbitrary-counterexample synthesis are incomparable: pbcegis ⊈ cegis and cegis ⊈ pbcegis.Source: §5.1.2 · p. 20

Language Family 3

5.1.3 Different Flavors of Bounded Counterexamples

  • With finite memory, bounded-counterexample and positive-bounded-counterexample synthesis are also incomparable: cbcegis ⊈ pbcegis and pbcegis ⊈ cbcegis.Source: §5.1.3 · p. 22

5.2 Infinite Memory Inductive Synthesis

  • With infinite memory, CBCEGIS ⊂ MINCEGIS = CEGIS and PBCEGIS ⊂ CEGIS = MINCEGIS; CBCEGIS and PBCEGIS remain incomparable.Source: §5.2 · p. 24

6 Analysis of OGIS for Finite Language Classes

For finite language classes, OGIS terminates when each nonterminal oracle response eliminates a candidate; this section analyzes minimum-query complexity through NP-hardness and teaching dimension.

6 Analysis of OGIS for Finite Language Classes

  • Finite-class OGIS terminates when each nonterminal response supplies a new example that rules out at least one candidate language.Enumerating languages until one satisfies the specification is one terminating procedure.Source: §6 · pp. 24–25

6.1 NP-hardness

  • Minimum-query synthesis is NP-hard for finite C and E with qcorr, including interfaces that also provide qposwit and qnegwit, via a reduction from minimum set cover.The reduction maps set-cover elements to competing languages and sets to examples; a minimum counterexample set corresponds to a minimum set cover.Source: §6.1 · p. 25

6.2 Relation to Teaching Dimension

  • Teaching dimension lower-bounds OGIS sample complexity, the number of examples needed to identify the correct language.The paper also identifies teaching dimension with the smallest number of examples required to identify the correct language.Source: §6.2 · pp. 26–27
  • For finite concept classes, cited bounds relate teaching dimension to VC dimension and class size, and an exhibited class makes the upper bound tight.Without restrictions on the concept class, the authors say strong sample-complexity bounds may not be provable.Source: §6.2 · p. 27

7 Conclusion

The paper formalizes OGIS as a framework for formal inductive synthesis and analyzes how CEGIS variants differ in synthesis power, especially under bounded memory. It presents this work as a first step, with several theoretical questions left open.

7 Conclusion

  • CEGIS variants can differ in synthesis power, especially when the learning engine can store only a bounded number of examples.The paper also compares finite and infinite memory and identifies teaching dimensions, learner time complexity, and learning strategies as open questions.Source: §7 · p. 27
  • The paper formalizes OGIS, illustrates how it generalizes concept learning and formal-methods synthesis, and analyzes CEGIS variants that use a verification engine as oracle.The paper identifies teaching dimensions for formal concept classes, time complexity, and learning strategies as directions for future work.Source: §7 · p. 27
  • The authors characterize their work as a first step toward a theory of formal inductive synthesis, with much left to understand.Source: §7 · p. 27
Loading 1505.03953v4…