作者位次 #5/19ACL 2026Poster· Natural Language Processing
C ritic L ean: Critic-Guided Reinforcement Learning for Mathematical Formalization
Zhongyuan Peng · Yifan Yao · Kaijing Ma · Shuyue Guo · Yizhe Li · Yichi Zhang · Chenchen Zhang · Yifan Zhang · Zhouliang Yu · Luming Li · Minghao Liu · Yihang Xia · JIAWEI SHEN · Yuchen Wu · Yixin Cao · Zhaoxiang Zhang · Wenhao Huang · JIAHENG LIU · Ge Zhang
摘要
Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving. While prior work has focused on generation and compilation success, little attention has been paid to the critic phase—the evaluation of whether generated for...