An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.
Self-Training with Direct Preference Optimization Improves Chain-of-Thought Reasoning
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
Effective training of language models (LMs) for mathematical reasoning tasks demands high-quality supervised fine-tuning data. Besides obtaining annotations from human experts, a common alternative is sampling from larger and more powerful LMs. However, this knowledge distillation approach can be costly and unstable, particularly when relying on closed-source, proprietary LMs like GPT-4, whose behaviors are often unpredictable. In this work, we demonstrate that the reasoning abilities of small-scale LMs can be enhanced through self-training, a process where models learn from their own outputs. We also show that the conventional self-training can be further augmented by a preference learning algorithm called Direct Preference Optimization (DPO). By integrating DPO into self-training, we leverage preference data to guide LMs towards more accurate and diverse chain-of-thought reasoning. We evaluate our method across various mathematical reasoning tasks using different base models. Our experiments show that this approach not only improves LMs' reasoning performance but also offers a more cost-effective and scalable solution compared to relying on large proprietary LMs.
citation-role summary
citation-polarity summary
fields
cs.AI 1years
2025 1verdicts
CONDITIONAL 1roles
background 1polarities
unclear 1representative citing papers
citing papers explorer
-
Mathesis: Towards Formal Theorem Proving from Natural Languages
An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.