A peephole optimization rewrites a specific instruction sequence into a faster equivalent. The compiler engineer discovers that x * 2 can become x << 1. The hard part is generalization: when does this rewrite apply? For which bit widths? Under what constraints on x?
Pure synthesis — deriving general rules from concrete instances via formal methods alone — succeeds on 35 of 81 LLVM optimization cases. LPG, which combines LLM reasoning with formal verification, succeeds on 74 of 81. On the broader set including floating-point and vector operations: 90 of 102.
The division of labor is precise. The LLM handles semantic abstraction — recognizing that a concrete optimization over 32-bit integers might generalize to arbitrary bit widths, or that a specific constant can be replaced by a symbolic variable under certain constraints. Formal verification ensures the generalized rule is sound and profitable. The LLM proposes; the verifier disposes.
Neither component alone achieves this. The LLM without verification produces plausible but sometimes unsound generalizations. The synthesizer without the LLM gets stuck on the search space — the number of possible generalizations is too large for exhaustive enumeration. The combination works because the two capabilities are complementary, not redundant: exploration is easy for the LLM and hard for the synthesizer; verification is easy for the synthesizer and impossible for the LLM.
The structural pattern: systems where the search space is too large for formal methods but the correctness criterion is too strict for heuristics are natural territory for hybrid approaches. The LLM narrows the search; the verifier validates the result. Neither trusts the other, and that mutual distrust is what makes the combination reliable.