Cover Image

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Peng, Zhongyuan, Yao, Yifan, Ma, Kaijing, Guo, Shuyue, Li, Yizhe, Zhang, Yichi, Zhang, Chenchen, Zhang, Yifan, Yu, Zhouliang, Li, Luming, Liu, Minghao, Xia, Yihang, Shen, Jiawei, Wu, Yuchen, Cao, Yixin, Zhang, Zhaoxiang, Huang, Wenhao, Liu, Jiaheng, Zhang, Ge
Format:	Preprint
Published:	2025
Subjects:	Computation and Language
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
by: Yu, Zhouliang, et al.
Published: (2025)

CodeCriticBench: A Holistic Code Critique Benchmark for Large Language Models
by: Zhang, Alexander, et al.
Published: (2025)

OProver: A Unified Framework for Agentic Formal Theorem Proving
by: Ma, David, et al.
Published: (2026)

ReLook: Vision-Grounded RL with a Multimodal LLM Critic for Agentic Web Coding
by: Li, Yuhang, et al.
Published: (2025)

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
by: Liu, Junqi, et al.
Published: (2026)

ING-VP: MLLMs cannot Play Easy Vision-based Games Yet
by: Zhang, Haoran, et al.
Published: (2024)

DeepMF: Deep Motion Factorization for Closed-Loop Safety-Critical Driving Scenario Simulation
by: Li, Yizhe, et al.
Published: (2024)

InfoCons: Identifying Interpretable Critical Concepts in Point Clouds via Information Theory
by: Li, Feifei, et al.
Published: (2025)

A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4
by: Liu, Junqi, et al.
Published: (2025)

UMOEA/D: A Multiobjective Evolutionary Algorithm for Uniform Pareto Objectives based on Decomposition
by: Zhang, Xiaoyuan, et al.
Published: (2024)

KOR-Bench: Benchmarking Language Models on Knowledge-Orthogonal Reasoning Tasks
by: Ma, Kaijing, et al.
Published: (2024)

Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries
by: Chen, Luoxin, et al.
Published: (2026)

ChatScene: Knowledge-Enabled Safety-Critical Scenario Generation for Autonomous Vehicles
by: Zhang, Jiawei, et al.
Published: (2024)

Autonomous Data Selection with Zero-shot Generative Classifiers for Mathematical Texts
by: Zhang, Yifan, et al.
Published: (2024)

CodeEditorBench: Evaluating Code Editing Capability of Large Language Models
by: Guo, Jiawei, et al.
Published: (2024)

Artificial Intelligence‐Driven Platform: Unveiling Critical Hepatic Molecular Alterations in Hepatocellular Carcinoma Development
by: Miao Jiang, et al.
Published: (2024)

LeanGeo: Formalizing Competitional Geometry problems in Lean
by: Song, Chendong, et al.
Published: (2025)

Feature‐Driven DEM Generation With Enhanced Detail Preservation and Noise Mitigation Using Conditional GANs
by: Chenhui Wu, et al.
Published: (2026)

GeoMapGAN: Remote Sensing Image to Map via Two‐Stream Network and Adaptive Noise
by: Xiaochi Ma, et al.
Published: (2025)

SVIP: Towards Verifiable Inference of Open-source Large Language Models
by: Sun, Yifan, et al.
Published: (2024)

Contingency Planning for Safety-Critical Autonomous Vehicles: A Review and Perspectives
by: Zheng, Lei, et al.
Published: (2026)

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
by: Long, Wentao, et al.
Published: (2026)

Safety-Critical Control with Uncertainty Quantification using Adaptive Conformal Prediction
by: Zhou, Hao, et al.
Published: (2024)

Can Large Language Models Detect Errors in Long Chain-of-Thought Reasoning?
by: He, Yancheng, et al.
Published: (2025)

WebCompass: Towards Multimodal Web Coding Evaluation for Code Language Models
by: Lei, Xinping, et al.
Published: (2026)

A Conditional Generative Framework for Synthetic Data Augmentation in Segmenting Thin and Elongated Structures in Biological Images
by: Liu, Yi, et al.
Published: (2025)

FMC: Formalization of Natural Language Mathematical Competition Problems
by: Xie, Jiaxuan, et al.
Published: (2025)

Induced Traffic Volume Prediction of a New Highway Based on the ESE Gravity Model
by: Yifan Li, et al.
Published: (2025)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
by: Yang, Bowen, et al.
Published: (2026)

Datasets and Supporting Scripts for Landmark Recentering and Lazy Witness Complex Experiments
by: Zhang, Yifan
Published: (2026)

Persuasion in Networks: Can the Sender Do Better than Using Public Signals?
by: Zhang, Yifan
Published: (2024)

Training and Evaluating Language Models with Template-based Data Generation
by: Zhang, Yifan
Published: (2024)

Deep Tensor Network
by: Zhang, Yifan
Published: (2023)

Residual Stream Duality in Modern Transformer Architectures
by: Zhang, Yifan
Published: (2026)

A Markov Categorical Framework for Language Modeling
by: Zhang, Yifan
Published: (2025)

Single Agent Robust Deep Reinforcement Learning for Bus Fleet Control
by: Zhang, Yifan
Published: (2025)

Local Depth-Based Corrections to Maxmin Landmark Selection for Lazy Witness Persistence
by: Zhang, Yifan
Published: (2026)

Exact Coset Sampling for Quantum Lattice Algorithms
by: Zhang, Yifan
Published: (2025)

MTU-Bench: A Multi-granularity Tool-Use Benchmark for Large Language Models
by: Wang, Pei, et al.
Published: (2024)

Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
by: Li, Yuxin, et al.
Published: (2025)