@inproceedings{fatima-2025-firma,
    title = "{FIRMA}: Bidirectional Formal-Informal Mathematical Language Alignment with Proof-Theoretic Grounding",
    author = "Fatima, Maryam",
    editor = "Valentino, Marco  and
      Ferreira, Deborah  and
      Thayaparan, Mokanarangan  and
      Ranaldi, Leonardo  and
      Freitas, Andre",
    booktitle = "Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025)",
    month = nov,
    year = "2025",
    address = "Suzhou, China",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-emnlp/2025.mathnlp-main.5/",
    pages = "62--76",
    ISBN = "979-8-89176-348-7",
    abstract = "While large language models excel at gener- ating plausible mathematical text, they often produce subtly incorrect formal translations that violate proof-theoretic constraints. We present FIRMA (Formal-Informal Reasoning in Mathematical Alignment), a bidirectional translation system between formal and informal mathematical language that leverages proof-theoretic interpretability hierarchies and specialized architectural components for proof preservation. Unlike existing approaches that treat this as pure sequence-to-sequence translation, FIRMA introduces a hierarchical architecture with complexity-aware routing, proof-preserving attention mechanisms, and multi-objective training that balances formal correctness with natural readability. Through progressive complexity training on curated datasets from Lean 4 and formal mathematics repositories, we evaluate FIRMA on 200 translation samples across complexity levels and compare against two baseline systems. Our analysis shows statistically significant improvements of 277.8{\%} over BFS-Prover- V1-7B and 6307.5{\%} over REAL-Prover on overall translation quality metrics. Ablation studies on 50 samples demonstrate that each architectural component contributes substan- tially to performance, with removal of any component resulting in 83-85{\%} performance degradation. We release our code at https://github.com/smfatima3/FIRMA"
}