Neuro-Symbolic Machine-Code Synthesis: Untrusted Palettes, Checked Answers

The system combines three mechanisms. First, four checker-aware reductions eliminate deadinstructions, independent reorderings, solver-proved duplicate forms, and prefixes that losesemantically required inputs; under stated premises, they preserve the optimum within a boundedpalette. Second, realize applies cost-bounded counterexample-guided solving to determine when nocheaper admitted program exists in that palette, producing records that can be replayed with thesame encoding and solver. Third, an LLM revises instruction palettes using checked kernels andper-length unrealizability or inconclusive answers.