We introduce FormalMATH, a large-scale Lean4 benchmark for formal mathematical reasoning, comprising 5,560 semantically validated Lean4 statements spanning competition-level and undergraduate mathematics. To improve reliability, FormalMATH is constructed through a human-in-the-loop pipeline that combines type checking, LLM-based semantic verification against the informal–formal statements alignment, negation-based disproving, and expert review. We conduct a systematic evaluation of frontier theorem provers under test-time scaling on FormalMATH. Results show that current provers remain far from solving the benchmark: the strongest model, DeepSeek-Prover-V2 (671B), achieves only 28.31% Pass@32. We further observe substantial domain imbalance across provers, with stronger performance in applied mathematics and algebra but weaker results in discrete mathematics. We identify common failure modes in current provers, including incomplete proofs, weak handling of inequalities, misuse of automation tactics, and redundant hypothesis introduction. Extreme test-time scaling (e.g., Pass@3200) yields only modest gains on a subset of FormalMATH, suggesting that current training paradigms do not equip provers to effectively exploit additional sampling budget. We also observe a counterintuitive negative effect when provers are given human-written natural-language solution references: such references can measurably degrade formal proof generation rather than aid it. Overall, FormalMATH provides a challenging and reliable testbed for measuring progress in formal mathematical reasoning.

Evaluating multimodal large language models (MLLMs) on long-form scientific papers requires measuring not only answer correctness, but also whether answers are supported by traceable cross-modal evidence. Existing answer-only metrics and synthetic “Needle-In-A-Haystack” tests mainly assess answer matching or isolated retrieval, leaving evidence-grounded support under-examined. We introduce “Fish-in-the-Ocean” (FITO), an evidence-chain evaluation lens for native scientific documents, and instantiate it with SIN-Data, a scientific interleaved corpus that preserves text–figure coupling. Built on SIN-Data, SIN-Bench comprises four evidence-auditing tasks: evidence discovery, hypothesis verification, grounded QA, and evidence-anchored synthesis. We further propose “No Evidence, No Score”, which credits predictions only when linked to verifiable anchors and diagnoses evidence quality through matching, relevance, and logic. Experiments on 10 MLLMs show a clear correctness–grounding gap: Gemini-3-pro obtains the best average overall score (0.566), while GPT-5 reaches the highest SIN-QA answer accuracy (0.767) but lower evidence-aligned scores. Code and data are available at https://github.com/IIGROUP/sin-bench .

Existing Chinese preference datasets suffer from limited scale, restricted domain coverage, and insufficiently rigorous data validation. Human annotation significantly limits the scalability of human preference datasets. As a result, Chinese Alignment and Chinese Reward Models (CRM) have not yet been thoroughly explored. To address these challenges, we design an LLM-based data annotation pipeline with no human intervention. Based on this pipeline, we curate COIG-P (Chinese Open Instruction Generalist - Preference), a high-quality, large-scale Chinese preference dataset consisting of 1M Chinese preference pairs and 92k carefully curated Chinese queries across diverse domains, including Chat, Coding, Maths, and others. We conduct experiments to verify the quality of COIG-P from two perspectives. (1) COIG-P brings significant performance improvements for the Qwen2/2.5 and Infinity-Instruct model series on AlignBench through DPO, with gains ranging from 2% to 12%. Furthermore, it significantly outperforms other existing Chinese preference datasets. (2) We train an 8B-sized CRM and manually annotate a Chinese Reward Benchmark (CRBench). Our CRM demonstrates robust scoring ability on CRBench. In addition, in practical data construction experiments, the quality of the data constructed by our CRM is comparable to that produced by GPT-4o.

Large language models are increasingly deployed as interactive coding agents for end-to-end web development, yet existing benchmarks evaluate narrow slices of this workflow—typically text-conditioned generation with static correctness metrics—overlooking visual fidelity, interactivity, and codebase-level reasoning. We introduce WebCompass, a benchmark that covers the full web development lifecycle by spanning three input modalities (text, image, video) and three task types (generation, editing, repair). To match the diverse nature of these tasks, we pair checklist-guided LLM-as-a-Judge for patch-based evaluation with a novel Agent-as-a-Judge protocol that executes generated websites in a real browser and synthesizes targeted test cases. Experiments on ten models reveal a 25-point gap between the best closed- and open-source models, persistent weaknesses in visual aesthetics even among frontier systems, and divergent performance profiles across task types that challenge the notion of a single "best" web coding agent.

Deep Research Agents have shown strong capability in multi-step information retrieval, reasoning, and long-form report generation, but existing benchmarks and systems remain predominantly text-centric, with limited evaluation of whether visual elements are factually reliable and well aligned with the surrounding analysis. To address this gap, we introduce TVIR (Text–Visual Interleaved Report Generation), which includes TVIR-Bench, a benchmark of 100 expert-curated multimodal deep research tasks that require visual elements to serve specific analytical sub-goals, and TVIR-Agent, a hierarchical multi-agent framework for constructing structured outlines, retrieving images, generating charts with traceable sources, and composing reports through context-aware sequential writing. We further develop a dual-path evaluation framework that combines Textual Assessment and Visual Assessment. Experiments across nine deep research systems show that TVIR-Agent achieves strong overall performance, underscoring the importance of explicit multimodal design and evaluation for evidence-driven report generation.

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 formalizations truly capture the semantic intent of the original problem. In this paper, we introduce CriticLean, a novel critic-guided reinforcement learning framework that elevates the role of the critic from a passive validator to an active learning component. Specifically, first, we propose the CriticLeanGPT, trained via supervised fine-tuning and reinforcement learning, to rigorously assess the semantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench, a benchmark designed to measure models’ ability to distinguish semantically correct from incorrect formalizations, and demonstrate that our trained CriticLeanGPT models can significantly outperform strong open- and closed-source baselines. Building on the CriticLean framework, we construct FineLeanCorpus, a dataset comprising over 509K problems that exhibits rich domain diversity, broad difficulty coverage, and high correctness based on human evaluation.Overall, our findings highlight that optimizing the critic phase is essential for producing reliable formalizations and we hope our CriticLean will provide valuable insights for future advances in formal mathematical reasoning.