ReExp: From Autoformalization Corrections to Transferable Repair Experience

Autoformalization enables solver-based reasoning by translating natural-language problems into executable symbolic representations, while feedback-driven refinement can correct faulty formalizations. Such refinement also produces correction histories, but a successful correction does not by itself reveal which local changes can be safely reused on new problems. We introduce ReExp, a framework that transforms failure-to-success correction histories into transferable repair experience. ReExp replays recorded corrections to isolate sufficient edits, abstracts them into typed and rebindable repair programs, and retains only repairs that demonstrate positive utility on held-out states. At inference, selected repairs are rebound and executed on compatible formalizations before standard refinement resumes. Across five logical reasoning benchmarks and four backbones, ReExp improves over within-instance solver-feedback refinement in all 20 settings, with per-backbone mean gains of 6.78–14.67 percentage points. It also outperforms retrieval-based experience reuse in most settings, with corresponding improvements in semantic faithfulness.