Papers by Ruida Wang
Let’s Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM’s Math Capability (2025.emnlp-main)
Copied to clipboard
| Challenge: | Recent work has focused on improving the mathematical reasoning capabilities of Large Language Models (LLMs). |
| Approach: | They propose an end-to-end framework to integrate FL into NL math reasoning . they propose a problem alignment method that reformulates QA and existence problems . |
| Outcome: | The proposed framework achieves 89.80% and 84.34% accuracy rates on the MATH-500 and the AMC benchmarks. |
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts (2024.emnlp-main)
Copied to clipboard
| Challenge: | a framework for formal proof writing using formal languages like Lean4 is needed to prove mathematical theorems using formal language. |
| Approach: | They propose a framework that trains a general-purpose LLM to be a Lean4 expert. |
| Outcome: | The proposed framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets. |
GRAFF: GRaph-Augmented Fine-grained Fusion for Large Language Models (2026.findings-eacl)
Copied to clipboard
| Challenge: | Existing methods to integrate graphs into LLMs compress the graph's structural information into a single token, restricting their ability to capture deep semantic and structural information. |
| Approach: | They propose a method that integrates fine-grained node-level structural information with corresponding text entities to LLMs via a lightweight, structure adapter module. |
| Outcome: | The proposed method outperforms baseline models in graph-based question answering by 10.24%. |
FANS: Formal Answer Selection for LLM Natural Language Math Reasoning Using Lean4 (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing frameworks that use Lean4 to enhance LLMs' NL reasoning abilities have been controversial in the field of math reasoning. |
| Approach: | They propose a framework that utilizes Lean4 to enhance LLMs’ NL math reasoning ability by generating a Lean 4 theorem statement and a proof-generating LLM. |
| Outcome: | The proposed framework improves LLMs' NL math reasoning ability by 2% across several math benchmarks and higher further based on reward models or in subfields such as algebra and number theory. |
Let’s Synthesize Step by Step: Iterative Dataset Synthesis with Large Language Models by Extrapolating Errors from Small Models (2023.findings-emnlp)
Copied to clipboard
| Challenge: | *Data Synthesis* is a promising way to train a small model with very little labeled data. |
| Approach: | They propose a framework that iteratively extrapolates the errors of a small model trained on a real-world validation dataset using a large language model. |
| Outcome: | The proposed framework reduces the gap between the synthesized dataset and the real data . it improves on multiple NLP tasks and on large models with human-annotated data. |