Specification-Guided Autoformalization with Source-Grounded Blueprints

Autoformalization translates informal mathematics into machine-checkable languages such as Lean~4. Large Language Models (LLMs) can generate plausible formal code, but successful elaboration establishes only that a declaration is well typed, not that it preserves the source meaning. Generated statements can instead omit, add, substitute, or structurally alter mathematical content while remaining valid Lean declarations. We present Specification-Guided Autoformalization (SGA), which separates semantic interpretation from Lean realization through a source-grounded, typed English specification called the Blueprint. Each Blueprint item cites the source spans that support it, enabling bidirectional review for omitted source content and unsupported specification items. SGA then translates the reviewed items into corresponding Lean fragments and assembles them in dependency order, preserving an audit trail from source evidence to generated code. In a small-scale study, SGA produces more semantically correct formalizations and shows stronger source sensitivity than direct and generic two-stage generation, although it accepts fewer outputs. Bidirectional review also improves the detection and localization of Blueprint mutations over holistic review.