FIRMA : Bidirectional Formal-Informal Mathematical Language Alignment with Proof-Theoretic Grounding (2025)

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

## introduction mathematical communication exists on a spectrum from the highly formal languages of proof assistants like lean and coq to the intuitive explanations found in textbooks. this duality creates a fundamental challenge: formal specifications ensure logical rigor but are often impenetrable to students, while informal descriptions aid understanding but may harbor subtle errors or ambiguities. the ability to translate bidirectionally between these represen-tations would benefit both mathematical education and formal verification efforts. recent advances in large language models (llms) have shown capabilities in mathematical reasoning. the development of systems like al-phageometry @xcite and funsearch @xcite demonstrates that neural approaches can achieve results on challenging mathematical problems, including discovering new theorems and solving olympiad-level geometry problems. however, standard mathematical reasoning benchmarks like the math dataset @xcite reveal limitations when models attempt formal-informal translation tasks. when applied to formal-informal translation, these models exhibit critical limitations. they generate superficially plausible translations that fail proof checking, introduce logical errors through imprecise natural language, and show unpredictable degradation as mathematical complexity increases. early attempts at neural theorem proving like nat-uralprover @xcite and more recent work on whole-proof generation @xcite have made progress, but these failures stem from treating mathematical translation as a purely linguistic task, ignoring the underlying prooftheoretic structure that governs mathematical validity. we introduce firma (formal-informal reasoning in mathematical alignment), a framework that grounds mathematical translation in proof-theoretic principles. our key insight is that successful translation requires not just linguistic fluency but also preservation of logical structure across complexity levels. firma addresses this through three core innovations: first, we develop a hierarchical encoder-decoder architecture that explicitly models mathematical complexity through specialized routing mechanisms. unlike flat sequence models, firma processes mathematical statements at multiple levels of abstraction-symbols, syntax trees, and semantic structures-enabling it to maintain logical coherence while adapting linguistic style. second, we introduce proof-preserving attention mechanisms that respect logical dependencies and prevent circular reasoning. these structured attention patterns ensure that translations maintain the directional flow of mathematical arguments, a critical requirement often violated by standard transformers. this approach builds on insights from proof artifact co-training @xcite and hy-pertree proof search @xcite , which demonstrate the importance of structured reasoning in formal mathematics. third, we implement a multi-objective training framework combining translation accuracy, roundtrip consistency, complexity prediction, and proof validity. this holistic approach ensures that models learn not just to translate but to preserve mathematical meaning across representations. our contributions are as follows. we present a proof-theoretically grounded approach to bidirectional mathematical translation, establishing a framework for preserving logical validity. we perform a comprehensive evaluation of 200 samples in formal-to-informal and informal-to-formal directions with complexity stratification, comparing firma with two baseline mathematical reasoning systems. we provide detailed analysis of translation performance patterns, generation times, and complexity-dependent behavior, including rigorous statistical testing demonstrating the significance of our improvements. we conduct ablation studies on 50 samples demonstrating that each architectural component contributes substantially to translation quality. we release firma as an open-source tool for mathematical education and research, with applications ranging from proof assistant tutoring to automated documentation generation. ## conclusion we presented firma, an approach to bidirectional formal-informal mathematical translation that leverages proof-theoretic principles and complexity-aware processing. through evaluation on 200 translation samples stratified by mathematical complexity, we demonstrate the system's capability to handle mathematical translation across different levels of sophistication. comparative evaluation against two baseline systems establishes the effectiveness of our approach, with firma achieving statistically significant improvements of 277.8% over bfs-prover-v1-7b and 6307.5% over real-prover on overall translation quality metrics. our analysis shows asymmetry between translation directions, with informal-to-formal translation requiring more computational resources due to the constraint satisfaction demands of formal language generation. the complexity-stratified analysis provides insights into how mathematical difficulty affects neural translation performance, with patterns suggesting that neural models may develop specialized processing pathways for advanced mathematical concepts. future work will explore scaling to larger evaluation sets with more balanced complexity distributions, investigating the counter-intuitive complexity-time relationship through detailed computational analysis, and extending firma to interactive theorem proving applications. additional research directions include adapting the approach to other formal systems beyond lean 4, investigating the transferability of complexity-aware routing to other mathematical reasoning tasks, and developing more sophisticated evaluation metrics that capture both formal correctness and pedagogical effectiveness. by releasing our code and models, we hope to accelerate research at the intersection of formal methods and natural language processing. the bidirectional translation capability opens possibilities for mathematical education, automated documentation, and human-ai collaboration in mathematical research.