Papers by Wotao Yin
BC-Prover: Backward Chaining Prover for Formal Theorem Proving (2024.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for interactive theorem proving in formal logic lack robustness and robustness. |
| Approach: | They propose a backward chaining framework guided by pseudo steps for proofstep generation that prioritizes pseudo steps. |
| Outcome: | The proposed framework improves on the miniF2F benchmark. |
Scale Down to Speed Up: Dynamic Data Selection for Reinforcement Learning (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Current approaches to Reinforcement Learning (RL) rely on massive static datasets, leading to computational inefficiency and redundant gradient updates. |
| Approach: | They propose a data-centric RL framework that dynamically selects the most informative training samples to optimize RL for mathematical reasoning. |
| Outcome: | The proposed framework achieves comparable performance to full-data training methods while requiring only 1.5K samples instead of 220K, reducing training time from 13 days to just 4 hours on 8A800 GPUs. |
AdapThink: Adaptive Thinking Preferences for Reasoning Language Models (2026.findings-acl)
Copied to clipboard
| Challenge: | Recent research has highlighted a significant inefficiency associated with the slow thinking paradigm . models often overthink simple tasks while underthinking complex challenges . |
| Approach: | They propose a framework for adaptive reasoning preference control that dynamically adjusts reflection preferences based on group-level distributional statistics of reasoning length and reflection intensity. |
| Outcome: | The proposed framework reduces average response length by 17.1%-21.4% while improving performance by 6.12-6.59 points under 32K token budgets. |