Generation Is Not Selection: Neuro-Symbolic Natural Language Formalization of Temporal Logic

Natural-language-to-temporal-logic translation is challenging because a requirement can admit multiple plausible formalizations. We study whether neuro-symbolic systems can select the intended formalization when a correct candidate is already present. We present Pendulum, a pipeline separating neural candidate synthesis from symbolic analysis and final selection. Symbolic analysis provides solver-backed equivalence and behavioral evidence, which a downstream judge uses before deterministic finalization. We evaluate Pendulum on ${\mathrm{DS}}_1^{tricky}$, a 306-instance future-time LTL dataset derived from the Little Tricky Logic benchmark. An audit of all 306 references identifies 55 confirmed reference errors and 48 ambiguous specifications, leaving 258 determinate cases for primary evaluation. A correct candidate is present for 92.2% of these cases, but the final system selects one correctly for 87.2%, yielding a 5.0-percentage-point coverage-to-selection gap. Controlled changes to synthesis, semantic analysis, and selection do not consistently eliminate this gap. Solver-backed behavioral evidence likewise does not reliably resolve selection when multiple semantically distinct candidates remain plausible given the natural-language requirement.