Reproduce “Bridging Formal Language with Chain-of-Thought Reasoning to Geometry Problem Solving” on OpenResearch

About this paper

Tianyun Yang, Yunwen Li, Ziniu Li, Zhihang Lin, Ruoyu Sun, Tian Ding

The GF-Reasoner framework enables Large Vision Language Models (LVLMs) to effectively solve complex geometry problems by bridging natural language Chain-of-Thought with formal language and a geometry solver. It achieved state-of-the-art accuracy, with gains of +16 points on PGPS9K and +18.3 points on UniGEO, while nearly eliminating computational errors.

Key insights

• Hybrid reasoning, combining flexible natural language CoT with the precision of formal language and solvers, significantly enhances LVLM capabilities in mathematically rigorous domains like geometry problem-solving.
• Scalable bidirectional data synthesis, particularly leveraging existing formal program annotations through customized backward synthesis, is crucial for efficiently creating high-quality formal-integrated CoT datasets.
• A two-stage training approach (SFT followed by RL) effectively instills tool-use capabilities; moderate SFT is essential for preserving a diverse policy space that unlocks greater reasoning potential during subsequent RL post-training.

Summary by alphaXiv.