ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems

Zeyu Zheng; Yiyang Liu; Yuyang Zhao; Congmin Zheng; Jiachen Zhu; Jianian Chen; Kangning Zhang; Kayue Daniel Wong; Lingyu Yang; Rong Shan; Shihao Chen; Thomas Zhu; Wentao Zhang; Xiaopeng Li; Yan Hu; Yongxi Lin; Yuxiang Chen; Zhuoying Ou; Jianghao Lin; Jeremy Avigad; Prasad Tetali; Jingbang Chen; Sean Welleck

arXiv · 2610.27046

ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems

View original source ↗Read source document ↗Export metadata ↓

Abstract

As AI systems begin to resolve open research problems, reliable verification becomes increasingly important. Formal mathematics provides a trusted framework for mathematical reasoning, enabling agents to produce machine-checkable proofs while conducting mathematical exploration. Existing formal mathematics benchmarks often focus on known results or a small set of prominent open problems, which can become difficult to evaluate reliably once solutions are discovered and widely disseminated. Existing evaluation protocols are also not always aligned with how modern coding agents operate. We therefore introduce ReuF2F, a Lean 4 benchmark of 244 formalized open problems drawn from Research Experiences for Undergraduates (REU), spanning entry-level open research problems across a broad range of mathematical subfields. We expect these less prominent open problems, which tend to attract less attention and may remain unsolved for longer, to be better suited for held-out evaluation of end-to-end open problem resolution in Lean. We adopt a standard coding-agent evaluation setting, placing each problem and its logical negation into a Lean project in a Docker container. We also build Leanimum-agent on mini-SWE-agent to provide a unified harness for fair comparisons across models. Our evaluation finds that even the best-performing model resolves only ~40% of the problems, leaving substantial room for improvement on formalized open research problems.

Explore related subjects

cs.AI cs.CL cs.LG

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Zeyu Zheng, Yiyang Liu, Yuyang Zhao, Congmin Zheng, Jiachen Zhu, Jianian Chen, Kangning Zhang, Kayue Daniel Wong, Lingyu Yang, Rong Shan, Shihao Chen, Thomas Zhu, Wentao Zhang, Xiaopeng Li, Yan Hu, Yongxi Lin, Yuxiang Chen, Zhuoying Ou, Jianghao Lin, Jeremy Avigad, Prasad Tetali, Jingbang Chen, Sean Welleck. 2026-10-19. ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems. https://arxiv.org/abs/2610.27046

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

RoSeViT: Role-Separated Vision Transformers for ARC Visual Reasoning

ARC tasks can be formulated as visual transformation problems, where a model must infer a high-level transformation rule from a small set of demonstrations and apply it consistently across a grid. While dense Vision Transformers (ViTs) perform well in this setting, they entangle local visual state and global transformation logic within a shared token representation, which can hinder consistent reasoning. In this paper, we introduce RoSeViT, a role-separated Vision Transformer that explicitly decouples high-level instruction inference from visual workspace computation. RoSeViT uses controller tokens to aggregate transformation-level information and workspace tokens to represent the visual grid, with a structured attention pass in which nonlocal workspace interactions are routed through the controller. This design is motivated by our formal analysis showing that enforcing a shared instruction representation can reduce the effective complexity of visual transformation modeling. RoSeViT outperforms dense ViT baselines under the standard VARC training and evaluation protocol for ARC. In a controlled backbone replacement setting, it improves ARC-1 accuracy from 54.5 to 56.6, and with recurrent refinement reaches 58.8. When integrated into the full system, RoSeViT-Ensemble improves performance from 60.4 to 62.6 on ARC-1. These results demonstrate that explicitly separating instruction and workspace representations leads to more effective visual reasoning on ARC tasks. GitHub repository: https://github.com/lz7fd/RoSeViT.

cs.AI↗

arXiv2026

Learning to Model Optimization Problems from Solver Outcomes

Automating optimization modeling with LLMs is a promising path toward scalable decision intelligence, but existing approaches either rely on agentic pipelines built on closed-source LLMs with high inference latency or fine-tune smaller LLMs using costly process supervision that often overfits to a single solver API. We study how reinforcement learning from inexpensive outcome labels can improve optimization modeling and support reuse across heterogeneous solver environments. To this end, we propose Optimization Modeling from Solver Outcomes (OMSO), which uses reinforcement learning (RL) with a mathematical programming solver as a deterministic, interactive environment. Given a natural-language problem and a target solver, OMSO generates solver-specific code, executes it in a sandboxed harness, and converts execution outcomes into scalar rewards in a closed-loop generate-execute-feedback-update process. This RL formulation learns optimization modeling without process-level supervision and supports cross-solver generalization by switching the solver environment rather than reconstructing solver-specific datasets. Experiments on NL4OPT, MAMO, IndustryOR, and OptiBench across Gurobi, OR-Tools, and COPT show that OMSO matches or outperforms process-supervised SFT, supports zero-shot training-free transfer, direct RL training, and SFT-cold-started RL, and improves modeling reasoning and semantic correctness beyond solver API usage.

cs.AI↗

arXiv2026

Forget Attention: Importance-Aware Attention Is All You Need

Attention retrieves content precisely, but its scores depend only on query--key products, leaving order and recency to positional encodings. Conversely, state-space models (SSMs) such as Mamba-3 track order and recency through input-dependent state transitions that decay and rotate, yet compressing context into a fixed-size state hampers precise retrieval. Hybrids like Samba and Hymba exploit this complementarity only across layers or heads, so SSM transitions never shape attention scores directly. The closest prior work, the Forgetting Transformer (FoX), adds an input-dependent forget gate to the scores but reweights attention by recency alone. We propose SSM-Informed Softmax Attention (SISA), which builds Mamba-3-style state transitions, rotation included, directly into the scores alongside FoX's gate. Each logit receives the weight such an SSM would give that token pair: a decayed match between rotated SSM projections. This rotation already encodes relative position, so SISA drops RoPE; restoring it raises loss. SISA outperforms parameter-matched Transformer and FoX in language modeling and length extrapolation. Among the attention models we compare, hybrids included, only SISA benefits from context beyond the training window. Building SSM transitions into the scores yields stronger attention, and our kernels make it faster and leaner than baselines on their official or standard kernels.

cs.AI↗