Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2603.24372

Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

Arsen Shebzukhov
View original source ↗Read source document ↗Export metadata ↓

Abstract

Autoformalization - automatically translating natural language mathematical texts into formal proof language such as Lean4 - can help accelerate AI-assisted mathematical research, be it via proof verification or proof search. I fine-tune Qwen3.5-2B with LoRA for natural language to Lean4 formalization on FineLeanCorpus and consider three training regimes: supervised fine-tuning (SFT) with curriculum learning (difficulty 1 to 10), SFT without curriculum ordering, and reinforcement learning using group relative policy optimization (GRPO) with a cycle consistency reward. Cycle consistency measures how well the meaning of a statement is preserved through a NL to Lean4 to NL' loop, computed as cosine similarity of off-the-shelf sentence embeddings. On an unseen subset of FineLeanCorpus (FLC) and on PutnamBench, RL substantially outperforms both SFT variants (mean cycle consistency 0.669 vs. 0.513 on FLC; 0.561 vs. 0.422 on PutnamBench), while increasing cross-entropy loss by only 0.011 nats, with minimal impact on formalization quality. Curriculum ordering provides no measurable benefit over shuffled training.

Explore related subjects

cs.CL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Arsen Shebzukhov. 2026-03-25. Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning. https://arxiv.org/abs/2603.24372

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

What is the Role of Small Models in the LLM Era: A Survey

Large Language Models (LLMs) have demonstrated remarkable capabilities in various reasoning tasks, which leads to the development of increasingly large models. However, scaling up model sizes results in significantly higher computational costs and energy consumption, which makes these models impractical for academic researchers and businesses with limited resources. At the same time, Small Models (SMs) are frequently used in practical settings, although their significance is currently underestimated. This raises important questions about the role of small models in the era of LLMs, a topic that has received limited attention in prior surveys. In this work, we systematically examine the relationship between LLMs and SMs from two key perspectives: Collaboration and Competition (or Complementarity). We hope this survey provides valuable insights for practitioners, fostering a deeper understanding of the contribution of small models and promoting more efficient use of computational resources.

cs.CL↗
arXiv2026

SG-FSM: A Self-Guiding Zero-Shot Prompting Paradigm for Multi-Hop Question Answering Based on Finite State Machine

Large Language Models with chain-of-thought prompting, such as OpenAI-o1, have shown impressive capabilities in natural language inference tasks. However, Multi-hop Question Answering (MHQA) remains challenging for many existing models due to issues like hallucination, error propagation, and limited context length. To address these challenges and enhance LLMs' performance on MHQA, we propose the Self-Guiding prompting Finite State Machine (SG-FSM), designed to strengthen multi-hop reasoning abilities. Unlike traditional chain-of-thought methods, SG-FSM tackles MHQA by iteratively breaking down complex questions into sub-questions, correcting itself to improve accuracy. It processes one sub-question at a time, dynamically deciding the next step based on the current context and results, functioning much like an automaton. Experiments across various benchmarks demonstrate the effectiveness of our approach, outperforming strong baselines on challenging datasets such as Musique. SG-FSM reduces hallucination, enabling recovery of the correct final answer despite intermediate errors. It also improves adherence to specified output formats, simplifying evaluation significantly.

cs.CL↗
arXiv2026

A Course Intelligence Platform for Higher Education: Lessons from AI-Assisted Course Evaluation

The rapid adoption of generative AI has created new opportunities for teaching, learning, and quality assurance. Existing applications, however, remain largely student-facing, with comparatively limited attention to institution-level needs. This paper presents a course intelligence platform deployed across more than 100 universities and serving over 10,000 instructors in China. By linking competency requirements, knowledge structures, teaching activities, and assessment evidence, it establishes a shared foundation for knowledge organization, instructional design, learning assessment, and quality evaluation. The course evaluation module is examined as a representative institution-facing application of the platform, which integrates national evaluation standards, structured educational evidence, customized prompting strategies, and domain-adapted LLMs to generate quantitative scores and qualitative feedback. A case study involving 100 authentic university courses is conducted to evaluate its alignment with expert judgments and the interpretability of its outputs. Statistical analyses show substantial agreement between AI-generated assessments and expert ratings, while qualitative results highlight the credibility of the feedback. The findings further suggest that AI-assisted evaluation requires not only capable models but also structured domain knowledge and transparent criteria. In this context, human ratings should be treated as an informative reference rather than an error-free gold standard, and the objective is to achieve consistent, interpretable, and defensible judgments instead of merely replicating expert scores.

cs.CL↗