Technical Report for AI4Math-2026 Track 1: Automated Semantic Alignment Verification and Error Categorization of Lean 4 Formalizations via Decomposition-Guided Auditing

We present a semantic alignment verification pipeline for Lean 4 autoformalization developed for the AI4Math @ ICML 2026 FormalRx Challenge. Given an informal mathematical statement and a candidate Lean formalization, the system predicts semantic alignment, generates corrected formal statements, localizes erroneous segments, and classifies errors using the 28-category SCI taxonomy. Our approach combines structured decomposition of informal mathematics, LLM-based semantic auditing, correction generation, and a hybrid SCI classifier integrating deterministic token substitution rules with model-based classification. Experiments on the official FormalRx benchmark show that our best system achieves an Overall score of $0.3397$, with strong Verdict F1 ($0.7327$) and Correction accuracy ($0.7671$). Results indicate that tightly coupled semantic reasoning and correction generation outperform heavily decomposed multi-stage pipelines, while symbolic heuristics provide effective complementary signals for SCI categorization.