LEMMA: Learned Guidance for Evidence-Carrying Long-Horizon Symbolic Rewriting

LEMMA is a neuro-symbolic system for long-horizon symbolic mathematical rewriting. It combines a symbolic rule engine, guardrail-filtered action generation, evidence-typed verification, and learned policy guidance to transform a starting expression into a specified goal through individually validated rewrite steps.The accompanying study evaluates six search and decoding procedures on a frozen 120-problem benchmark with reference derivations of depths 64, 96, and 128. On the 89 problems containing genuine branching decisions, learned local action ranking substantially improves fixed-budget search efficiency.