paper-with-me

홈 › Papers

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs

2026-05-08 · Viresh Pati, Zhengyu Li, Piyush Jha, Rahul Garg, Yatharth Sejpal, Vijay Ganesh arxiv

We introduce MathConstraint, a hard, adaptive benchmark for evaluating the combinatorial reasoning capabilities of LLMs. We combine constraint satisfaction problems with rigorous solver-based verification and design an adaptive generator to create instances that remain challenging as the LLMs improve in their reasoning capabilities. Unlike existing benchmarks that quickly saturate on fixed datasets or use LLM-as-a-judge for checking solutions,MathConstraint uses parameterized problem types that enable scalable generation of arbitrarily difficult and automatically verifiable instances. We release MathConstraint-Easy ($266$ instances), on which frontier models achieve between $72.6\%$ (gemini-3.1-flash-lite) and $87.6\%$ (gpt-5.5) accuracy, and MathConstraint ($329$ instances) on which the same models drop to between $18.5\%$ (claude-4.6-sonnet) and $66.9\%$ (gpt-5.5) accuracy, demonstrating the resilience of our benchmark generator against rapid progress in LLM reasoning capabilities. We evaluate 12 frontier and open-weight models with and without access to a sandboxed Python environment that includes generic SAT/SMT solvers. Tool access roughly doubles frontier accuracy on MathConstraint (mean $+28$pp; up to $+52$pp for claude-4.6-sonnet). Further, halving the tool-call budget from $8$ to $4$ rounds erases up to $37$ points -- a sensitivity that most single-budget benchmarks miss. We release the generator, dataset, and evaluation harness as a robust environment for studying combinatorial reasoning and tool-use behavior under adversarially-tunable difficulty.

📄 PDF Abstract BibTeX arXiv:2605.08498

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

CombEval: A Framework for Evaluating Combinatorial Counting in Large Language Models

2026-06-18 · Yuxu Zhou, Ondřej Kuželka, Yuyi Wang, Yuanhong Wang 외 arxiv

We present CombEval, a dynamic benchmark for evaluating combinatorial counting in large language models. CombEval represents each problem as a typed Cofola specification over entities, combinatorial objects, object depen…

Using Reasoning Models to Generate Search Heuristics that Solve Open Instances of Combinatorial Design Problems

2025-05-29 · Christopher D. Rosin

Large Language Models (LLMs) with reasoning are trained to iteratively generate and refine their answers before finalizing them, which can help with applications to mathematics and code generation. We apply code generati…

Code Generation

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

2025-08-21 · Terry Jingchen Zhang, Wenyuan Jiang, Rongchuan Liu, Yisong Wang 외 arxiv

Formal theorem proving (FTP) has emerged as a critical foundation for evaluating the reasoning capabilities of large language models, enabling automated verification of mathematical proofs at scale. However, progress has…

Automated Theorem ProvingArithmetic Reasoning

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs

2026-05-06 · Beibei Xiong, Hangyu Lv, Junqi Liu, Yisen Wang 외 arxiv

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberge…

VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generation

2025-12-12 · Adewale Akinfaderin, Shreyas Subramanian arxiv

Financial AI systems suffer from a critical blind spot: while Retrieval-Augmented Generation (RAG) excels at finding relevant documents, language models still generate calculation errors and regulatory violations during …