activity
20242026
most citedFormalAlign: Automated Alignment Evaluation for Autoformalization

1 citations · 2 across the 10 of their papers we have counts for

collaborators

11 papers

cs.LG2026

Entropy Can Flow, or It Can Guide. Be Entropy. LEDFlow: Introducing Entropy-guided Generation Order into Uniform Discrete Flow

Tung Sum Thomas Kwok, Yidong Ouyang, Yingjia Wan +3

Uniform discrete flow permits repeated updates at every generation position. While continued revision supports correction of wrong tokens, it also exposes correct intermediate pred…

cs.CL2026

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

Eric Jiang, Xiao Liang, Yikai Zhang +19

Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for we…

cs.CL2026

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Haocheng Wang, Baiyu Huang, Yingjia Wan +4

The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar…

cs.CL2025

FaStfact: Faster, Stronger Long-Form Factuality Evaluations in LLMs

Yingjia Wan, Haochen Tan, Xiao Zhu +9

Evaluating the factuality of long-form generations from Large Language Models (LLMs) remains challenging due to efficiency bottlenecks and reliability concerns. Prior efforts attem…

cs.CL2025

InteractComp: Evaluating Search Agents With Ambiguous Queries

Mingyi Deng, Lijun Huang, Yani Fan +23

Language agents have demonstrated remarkable potential in web search and information retrieval. However, many search-agent benchmarks assume that user queries are complete and unam…

cs.LG2025

Meaningless Tokens, Meaningful Gains: How Activation Shifts Enhance LLM Reasoning

Zeru Shi, Yingjia Wan, Zhenting Wang +4

Motivated by the puzzling observation that inserting long sequences of meaningless tokens before the query prompt can consistently enhance LLM reasoning performance, this work anal…

cs.AI2025★ 1 cited

SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas

Anjiang Wei, Yuheng Wu, Yingjia Wan +6

We introduce SATBench, a benchmark for evaluating the logical reasoning capabilities of large language models (LLMs) through logical puzzles derived from Boolean satisfiability (SA…

cs.CL2024★ 1 cited

FormalAlign: Automated Alignment Evaluation for Autoformalization

Jianqiao Lu, Yingjia Wan, Yinya Huang +3

Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic al…

cs.CL2024

MR-Ben: A Meta-Reasoning Benchmark for Evaluating System-2 Thinking in LLMs

Zhongshen Zeng, Yinhong Liu, Yingjia Wan +16

Large language models (LLMs) have shown increasing capability in problem-solving and decision-making, largely based on the step-by-step chain-of-thought reasoning processes. Howeve…

cs.CL2024

Process-Driven Autoformalization in Lean 4

Jianqiao Lu, Yingjia Wan, Zhengying Liu +10

Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing effort…

cs.CL2024

AutoPSV: Automated Process-Supervised Verifier

Jianqiao Lu, Zhiyang Dou, Hongru Wang +4

In this work, we propose a novel method named \textbf{Auto}mated \textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier (\textbf{\textsc{AutoPSV}}) to enhance the reasoning capabil…