Bridging Formal Language with Chain-of-Thought Reasoning to Geometry Problem Solving

• URL: http://arxiv.org/abs/2508.09099v1
• Date: Tue, 12 Aug 2025 17:26:23 GMT
• Title: Bridging Formal Language with Chain-of-Thought Reasoning to Geometry Problem Solving
• Abstract summary: We present a new approach that integrates Chain-of-Thought (CoT) with formal language.<n>The model interleaves natural language reasoning with incremental emission of solver-executable code.<n>Built on Qwen2.5-VL-7B, our new model, GF-Reasoner, achieves up to 15% accuracy improvements on standard GPS benchmarks.
• Score: 9.550050299909184
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large vision language models exhibit notable limitations on Geometry Problem Solving (GPS) because of their unreliable diagram interpretation and pure natural-language reasoning. A recent line of work mitigates this by using symbolic solvers: the model directly generates a formal program that a geometry solver can execute. However, this direct program generation lacks intermediate reasoning, making the decision process opaque and prone to errors. In this work, we explore a new approach that integrates Chain-of-Thought (CoT) with formal language. The model interleaves natural language reasoning with incremental emission of solver-executable code, producing a hybrid reasoning trace in which critical derivations are expressed in formal language. To teach this behavior at scale, we combine (1) supervised fine-tuning on an 11K newly developed synthetic dataset with interleaved natural language reasoning and automatic formalization, and (2) solver-in-the-loop reinforcement learning that jointly optimizes both the CoT narrative and the resulting program through outcome-based rewards. Built on Qwen2.5-VL-7B, our new model, named GF-Reasoner, achieves up to 15% accuracy improvements on standard GPS benchmarks, surpassing both 7B-scale peers and the much larger model Qwen2.5-VL-72B. By exploiting high-order geometric knowledge and offloading symbolic computation to the solver, the generated reasoning traces are noticeably shorter and cleaner. Furthermore, we present a comprehensive analysis of method design choices (e.g., reasoning paradigms, data synthesis, training epochs, etc.), providing actionable insights for future research.

Related papers

• Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing [27.961458371130018]
  We propose SD-GPS, a solver-driven framework that treats the symbolic solver as an execution oracle throughout both formalization and deduction.<n>We show that SD-GPS consistently outperforms existing MLLM, neural, and neuro-symbolic methods across standard completion, multiple-choice, and cross-modal reference regimes.
  arXiv  Detail & Related papers  (2026-06-26T10:20:09Z)
• Knowledge Graphs are Implicit Reward Models: Path-Derived Signals Enable Compositional Reasoning [4.464939140209426]
  We propose a bottom-up learning paradigm in which models are grounded in axiomatic domain facts and compose them to solve complex, unseen tasks.<n>By deriving novel reward signals from knowledge graph paths, we provide verifiable, scalable, and grounded supervision.<n>Our experiments show that path-derived rewards act as a "compositional bridge", enabling our model to significantly outperform larger models.
  arXiv  Detail & Related papers  (2026-01-21T16:38:59Z)
• AgentMath: Empowering Mathematical Reasoning for Large Language Models via Tool-Augmented Agent [80.83250816918861]
  Large Reasoning Models (LRMs) like o3 and DeepSeek-R1 have achieved remarkable progress in natural language reasoning with long chain-of-thought.<n>However, they remain computationally inefficient and struggle with accuracy when solving problems requiring complex mathematical operations.<n>We present AgentMath, an agent framework that seamlessly integrates language models' reasoning capabilities with code interpreters' computational precision.
  arXiv  Detail & Related papers  (2025-12-23T19:57:49Z)
• Geometrically-Constrained Agent for Spatial Reasoning [53.93718394870856]
  Vision Language Models exhibit a fundamental semantic-to-geometric gap in spatial reasoning.<n>Current paradigms fail to bridge this gap.<n>We propose a training-free agentic paradigm that resolves this gap by introducing a formal task constraint.
  arXiv  Detail & Related papers  (2025-11-27T17:50:37Z)
• Learning to Reason: Training LLMs with GPT-OSS or DeepSeek R1 Reasoning Traces [2.0789230137053014]
  Test-time scaling has enabled a new class of Large Language Models (LLMs) that are able to reason through complex problems.<n>We compare the performance of medium-sized LLMs on Math problems after post-training on two kinds of reasoning traces.
  arXiv  Detail & Related papers  (2025-11-24T17:26:58Z)
• Teaching Language Models to Reason with Tools [73.21700643314917]
  We present emphHint-Engineering, a new data synthesis strategy that strategically injects diverse hints at optimal points within reasoning paths.<n>CoRT significantly enhances efficiency, reducing token usage by approximately 30% for the 32B model and 50% for the 1.5B model.
  arXiv  Detail & Related papers  (2025-10-23T08:41:44Z)
• Reasoning Distillation and Structural Alignment for Improved Code Generation [0.6933020649563103]
  This work distills the reasoning capabilities of a large language model into a smaller, more efficient model that is faster and cheaper to deploy.<n>Our approach trains the model to emulate the reasoning and problem-solving abilities of the VLLM by learning to identify correct solution pathways.<n> Experimental results show that our fine-tuned model, developed through a cheap and simple to implement process, significantly outperforms our baseline model in terms of pass@1, average data flow, and average syntax match metrics.
  arXiv  Detail & Related papers  (2025-10-20T14:47:47Z)
• RV-Syn: Rational and Verifiable Mathematical Reasoning Data Synthesis based on Structured Function Library [58.404895570822184]
  RV-Syn is a novel mathematical Synthesis approach.<n>It generates graphs as solutions by combining Python-formatted functions from this library.<n>Based on the constructed graph, we achieve solution-guided logic-aware problem generation.
  arXiv  Detail & Related papers  (2025-04-29T04:42:02Z)
• Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment [21.12989936864145]
  Chain-of-Thought (CoT) prompting has shown promise in enhancing the reasoning capabilities of large language models (LLMs)<n>We propose Reasoning-as-Logic-Units (RaLU), which constructs a more reliable reasoning path by aligning logical units between the generated program and their corresponding NL descriptions.
  arXiv  Detail & Related papers  (2025-02-05T08:23:18Z)
• SRA-MCTS: Self-driven Reasoning Augmentation with Monte Carlo Tree Search for Code Generation [14.786100203787194]
  Large language models demonstrate exceptional performance in simple code generation tasks but face challenges in tackling complex problems.<n>We propose a reasoning-augmented data generation process, SRA-MCTS, which guides the model to autonomously generate high-quality intermediate reasoning paths.<n>Our method operates entirely through the model itself without requiring additional supervision.
  arXiv  Detail & Related papers  (2024-11-17T12:31:04Z)
• Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
  We propose a neural-symbolic model for plane geometry problem solving (PGPS) with three key steps: modal fusion, reasoning process and knowledge verification. For reasoning, we design an explicable solution program to describe the geometric reasoning process, and employ a self-limited decoder to generate solution program autoregressively. We also construct a large-scale geometry problem dataset called PGPS9K, containing fine-grained annotations of textual clauses, solution program and involved knowledge solvers.
  arXiv  Detail & Related papers  (2024-07-10T02:45:22Z)
• How Do Humans Write Code? Large Models Do It the Same Way Too [14.954886191356342]
  Program-of-Thought (PoT) replaces natural language-based Chain-of-Thought (CoT) as the most popular method in Large Language Models. Using PoT introduces more reasoning errors, such as incorrect formulas or flawed logic, compared to CoT. We propose Human-Think Language (HTL), which leverages a suite of strategies that help integrate PoT and CoT.
  arXiv  Detail & Related papers  (2024-02-24T05:40:01Z)
• Large Language Models as Analogical Reasoners [155.9617224350088]
  Chain-of-thought (CoT) prompting for language models demonstrates impressive performance across reasoning tasks. We introduce a new prompting approach, analogical prompting, designed to automatically guide the reasoning process of large language models.
  arXiv  Detail & Related papers  (2023-10-03T00:57:26Z)
• Neural-Symbolic Solver for Math Word Problems with Auxiliary Tasks [130.70449023574537]
  Our NS-r consists of a problem reader to encode problems, a programmer to generate symbolic equations, and a symbolic executor to obtain answers. Along with target expression supervision, our solver is also optimized via 4 new auxiliary objectives to enforce different symbolic reasoning.
  arXiv  Detail & Related papers  (2021-07-03T13:14:58Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  We construct a new large-scale benchmark, Geometry3K, consisting of 3,002 geometry problems with dense annotation in formal language. We propose a novel geometry solving approach with formal language and symbolic reasoning, called Interpretable Geometry Problem solver (Inter-GPS) Inter-GPS incorporates theorem knowledge as conditional rules and performs symbolic reasoning step by step.
  arXiv  Detail & Related papers  (2021-05-10T07:46:55Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.