{"total":20,"rows":[{"id":"2510.24592","title":"ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization","created":"2025-10-28","cited_by_count":20,"area":"lr"},{"id":"2507.06181","title":"CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization","created":"2025-07-08","cited_by_count":16,"area":"lr"},{"id":"2508.04440","title":"StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion","created":"2025-08-06","cited_by_count":16,"area":"lr"},{"id":"2505.12680","title":"Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities","created":"2025-05-19","cited_by_count":8,"area":"lr"},{"id":"2508.14644","title":"LeanGeo: Formalizing Competitional Geometry problems in Lean","created":"2025-08-20","cited_by_count":7,"area":"lr"},{"id":"2506.10903","title":"Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning","created":"2025-06-12","cited_by_count":6,"area":"lr"},{"id":"2510.09517","title":"StatEval: A Comprehensive Benchmark for Large Language Models in Statistics","created":"2025-10-10","cited_by_count":6,"area":"lr"},{"id":"2601.23135","title":"Why GRPO Needs Normalization: A Local-Curvature Perspective on Adaptive Gradients","created":"2026-01-30","cited_by_count":5,"area":"lr"},{"id":"2603.19514","title":"Learning to Disprove: Formal Counterexample Generation with Large Language Models","created":"2026-03-19","cited_by_count":5,"area":"lr"},{"id":"2602.02561","title":"MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics","created":"2026-01-30","cited_by_count":4,"area":"lr"},{"id":"2607.04655","title":"FormalRx: Rectify and eXamine Semantic Failures in Autoformalization","created":"2026-07-06","cited_by_count":4,"area":"lr"},{"id":"2605.28365","title":"Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning","created":"2026-05-27","cited_by_count":3,"area":"lr"},{"id":"2607.13248","title":"GSM-Plus-BN: A Perturbation-Based Benchmark for Bangla Mathematical Reasoning in Large Language Models","created":"2026-07-14","cited_by_count":2,"area":"lr"},{"id":"2602.07992","title":"When Is Compositional Reasoning Learnable from Verifiable Rewards?","created":"2026-02-08","cited_by_count":1,"area":"lr"},{"id":"2604.06505","title":"MedConclusion: A Benchmark for Biomedical Conclusion Generation from Structured Abstracts","created":"2026-04-07","cited_by_count":1,"area":"lr"},{"id":"2605.07147","title":"MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries","created":"2026-05-08","cited_by_count":1,"area":"lr"},{"id":"2606.28841","title":"LAMP: Lean-based Agentic framework with MCP and Proof Repair","created":"2026-06-27","cited_by_count":1,"area":"lr"},{"id":"2605.17255","title":"CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean","created":"2026-05-17","cited_by_count":0,"area":"lr"},{"id":"2607.12733","title":"LLMs Can See the Smoke but not the Fire: Evaluating Abductive Reasoning with Elenchos","created":"2026-07-14","cited_by_count":0,"area":"lr"},{"id":"2608.25449","title":"MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize","created":"2026-08-26","cited_by_count":0,"area":"lr"}],"next_cursor":null}