Limitations of program synthesis#

Problems#

• General non-continuity of discrete solutions
  • Property of highly compressed representations
• Lack of correlation between syntatic and semantic program space
• Undecidability (and thus difficulty in comparing) semantic space: Rice’s Theorem
• Applies even to highly constrained (templated DSL) search spaces.

Potential approach#

Dual latent space:

• What it does
• The form it takes

Implications:

• Semantic space can be continuous: amenable to gradient methods, diffusion
• Structural space is discrete but constrained by semantic intent: smaller search space
• Mapping from structural to concrete is deterministic: no search needed

┌─────────────────────────────────────────────────────────────────┐
│                    Semantic Latent Space                        │
│                         (continuous)                            │
│                                                                 │
│    Captures "what the program does" at high level               │
│    e.g., "maps positive inputs to 1, negative to 0"             │
│                                                                 │
│         z_semantic ∈ ℝᵈ                                         │
└─────────────────────────┬───────────────────────────────────────┘
                          │
                    decode (learned)
                          │
                          ▼
┌─────────────────────────────────────────────────────────────────┐
│                  Structural Latent Space                        │
│                    (discrete, combinatorial)                    │
│                                                                 │
│    Captures "how the program is organized"                      │
│    e.g., "uses if-then-else at root, comparison at condition"   │
│                                                                 │
│         z_structural ∈ Grammar Derivations                      │
└─────────────────────────┬───────────────────────────────────────┘
                          │
                    deterministic expansion
                          │
                          ▼
┌─────────────────────────────────────────────────────────────────┐
│                      Concrete Program                           │
│                                                                 │
│    if x > 0:                                                    │
│        return 1                                                 │
│    return 0                                                     │
└─────────────────────────────────────────────────────────────────┘