VCSearch studies a failure mode that standard math benchmarks largely ignore: real-world mathematical problems with missing or contradictory conditions. It introduces a new benchmark, PMC, and a training-free formal-search framework that improves rejection of unsolvable problems without giving up performance on well-defined ones.
VCSearch starts from a practical observation: LLMs often produce fluent but wrong answers when a math word problem is missing key conditions or contains internal contradictions.
PMC is built by mutating four common math reasoning datasets and validating the resulting
problems as truly unsolvable. The public Hugging Face release exposes missing_test
and contra_test splits.
PMC is constructed from GSM8K, SVAMP,
AddSub, and MultiArith by turning standard solvable
questions into unsolvable ones through incompleteness or contradiction. Candidate instances
are validated by multiple LLMs, with disputed cases reviewed by humans, and the released
benchmark exposes missing_test and contra_test splits together with
R-Rate and R-Score for evaluation.
PMC makes the core tension visible: once a system must both solve normal problems and detect unsolvable ones, prompt-only strategies run into a trade-off. That points to a deeper bottleneck, namely reliable formalization of variables and constraints before solving.
Mixed prompting weakens robustness on unsolvable cases, especially for smaller models.
The same prompting strategy also harms ordinary problem solving, showing that the issue is structural rather than cosmetic.
Instead of forcing an LLM to formalize the whole problem in one pass, VCSearch treats formalization itself as the hard part and decomposes it into a neuro-symbolic search over variables and constraints.
VCSearch first builds a draft formal state and, when full constraints are still unstable, falls back to a variable-centered anchor. This gives the search a reliable starting point instead of forcing brittle one-shot formalization.
Select one unexplored head variable and its related constraints so the next search step stays localized.
Use the LLM to polish constraints, recover implicit variables, and expand the current formal state.
Use Z3 and an LLM judge to compare candidate states and keep the branch with better formal consistency.
We highlight the main downstream gains on well-defined reasoning and mixed realistic settings, then summarize robustness across model scales.
Average improvement over SatLM on well-defined tasks.
Average well-defined accuracy of VCSearch vs. 61.51% for SatLM.
Qwen 1.5B rises from 15.10% to 35.30% on well-defined tasks.
VCSearch + PAL improves Qwen2.5 1.5B from 32.85 to 62.28.
Average accuracy distilled from the main paper table over AddSub, MultiArith, SVAMP, GSM8K, RobustMath, and GSM-IC.
| Model | SatLM | VCSearch | Delta |
|---|---|---|---|
| DeepSeek-Coder 6.7B | 43.97% | 50.87% | +6.90 |
| Qwen2.5 7B | 61.51% | 77.76% | +16.25 |
| Qwen2.5 3B | 37.58% | 54.64% | +17.06 |
| Qwen2.5 1.5B | 15.10% | 35.30% | +20.20 |
VCSearch acts as a solvability filter for downstream reasoning methods such as CoT and PAL.
VCSearch remains strongest from 1.5B to 7B when models must recognize unsolvable inputs.
The method also improves formal modeling quality on well-defined benchmarks.
The BibTeX below follows the ACL Anthology entry for EMNLP 2025.
@inproceedings{tian-etal-2025-vcsearch,
title = "{VCS}earch: Bridging the Gap Between Well-Defined and Ill-Defined Problems in Mathematical Reasoning",
author = "Tian, Shi-Yu and
Zhou, Zhi and
Yu, Kun-Yang and
Yang, Ming and
Jia, Lin-Han and
Guo, Lan-Zhe and
Li, Yu-Feng",
editor = "Christodoulopoulos, Christos and
Chakraborty, Tanmoy and
Rose, Carolyn and
Peng, Violet",
booktitle = "Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing",
month = nov,
year = "2025",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2025.emnlp-main.642/",
doi = "10.18653/v1/2025.emnlp-main.642",
pages = "12710--12731",
ISBN = "979-8-89176-332-6"
}