{"list":"other","total":70,"rows":[{"id":"2203.02155","title":"Training language models to follow instructions with human feedback","created":"2022-03-04","cited_by_count":15971},{"id":"2402.03300","title":"DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models","created":"2024-02-05","cited_by_count":9379},{"id":"2210.03629","title":"ReAct: Synergizing Reasoning and Acting in Language Models","created":"2022-10-06","cited_by_count":8695},{"id":"2303.11366","title":"Reflexion: Language Agents with Verbal Reinforcement Learning","created":"2023-03-20","cited_by_count":4276},{"id":"2303.17651","title":"Self-Refine: Iterative Refinement with Self-Feedback","created":"2023-03-30","cited_by_count":3442},{"id":"2409.19256","title":"HybridFlow: A Flexible and Efficient RLHF Framework","created":"2024-09-28","cited_by_count":2057},{"id":"2408.03314","title":"Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters","created":"2024-08-06","cited_by_count":1986},{"id":"2405.15793","title":"SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering","created":"2024-05-06","cited_by_count":1737},{"id":"2304.05128","title":"Teaching Large Language Models to Self-Debug","created":"2023-04-11","cited_by_count":988},{"id":"2203.14465","title":"STaR: Bootstrapping Reasoning With Reasoning","created":"2022-03-28","cited_by_count":940},{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427},{"id":"2109.00110","title":"MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics","created":"2021-08-31","cited_by_count":391},{"id":"2009.03393","title":"Generative Language Modeling for Automated Theorem Proving","created":"2020-09-07","cited_by_count":388},{"id":"2310.10631","title":"Llemma: An Open Language Model For Mathematics","created":"2023-10-16","cited_by_count":388},{"id":"2210.12283","title":"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs","created":"2022-10-21","cited_by_count":291},{"id":"2504.21801","title":"DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition","created":"2025-04-30","cited_by_count":287},{"id":"2205.12615","title":"Autoformalization with Large Language Models","created":"2022-05-25","cited_by_count":263},{"id":"2405.14333","title":"DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data","created":"2024-05-23","cited_by_count":234},{"id":"1707.00183","title":"Teacher-Student Curriculum Learning","created":"2017-07-01","cited_by_count":210},{"id":"2205.11491","title":"HyperTree Proof Search for Neural Theorem Proving","created":"2022-05-23","cited_by_count":197},{"id":"2408.08152","title":"DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search","created":"2024-08-15","cited_by_count":197},{"id":"2302.12433","title":"ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics","created":"2023-02-24","cited_by_count":192},{"id":"2504.11354","title":"Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning","created":"2025-04-15","cited_by_count":180},{"id":"2407.11214","title":"PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition","created":"2024-07-15","cited_by_count":165},{"id":"2508.03613","title":"Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction","created":"2025-08-05","cited_by_count":154},{"id":"2202.01344","title":"Formal Mathematics Statement Curriculum Learning","created":"2022-02-03","cited_by_count":142},{"id":"2502.07640","title":"Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving","created":"2025-02-11","cited_by_count":133},{"id":"2102.06203","title":"Proof Artifact Co-training for Theorem Proving with Language Models","created":"2021-02-11","cited_by_count":132},{"id":"2406.03847","title":"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems","created":"2024-06-06","cited_by_count":122},{"id":"1905.09381","title":"Learning to Prove Theorems via Interacting with Proof Assistants","created":"2019-05-21","cited_by_count":109},{"id":"2401.08500","title":"Code Generation with AlphaCodium: From Prompt Engineering to Flow Engineering","created":"2024-01-16","cited_by_count":103},{"id":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101},{"id":"2310.04353","title":"An In-Context Learning Agent for Formal Theorem-Proving","created":"2023-10-06","cited_by_count":82},{"id":"2407.10040","title":"Lean-STaR: Learning to Interleave Thinking and Proving","created":"2024-07-14","cited_by_count":68},{"id":"2310.17807","title":"Clover: Closed-Loop Verifiable Code Generation","created":"2023-10-26","cited_by_count":67},{"id":"2509.22819","title":"Hilbert: Recursively Building Formal Proofs with Informal Reasoning","created":"2025-09-26","cited_by_count":60},{"id":"2404.00762","title":"Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification","created":"2024-03-31","cited_by_count":58},{"id":"2404.12534","title":"Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean","created":"2024-04-18","cited_by_count":58},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58},{"id":"2406.08467","title":"DafnyBench: A Benchmark for Formal Software Verification","created":"2024-06-12","cited_by_count":57},{"id":"2403.18120","title":"Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization","created":"2024-03-26","cited_by_count":55},{"id":"2303.05491","title":"Verus: Verifying Rust Programs using Linear Ghost Types (extended version)","created":"2023-03-09","cited_by_count":53},{"id":"2601.14027","title":"Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics","created":"2026-01-20","cited_by_count":50},{"id":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49},{"id":"1804.00596","title":"TacticToe: Learning to Prove with Tactics","created":"2018-04-02","cited_by_count":44},{"id":"2311.07948","title":"Finding Inductive Loop Invariants using Large Language Models","created":"2023-11-14","cited_by_count":36},{"id":"2403.04651","title":"Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)","created":"2024-03-07","cited_by_count":34},{"id":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","cited_by_count":34},{"id":"2410.15756","title":"Automated Proof Generation for Rust Code via Self-Evolution","created":"2024-10-21","cited_by_count":33},{"id":"2510.12787","title":"Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics","created":"2025-10-14","cited_by_count":31},{"id":"2008.00120","title":"The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq","created":"2020-07-31","cited_by_count":24},{"id":"2409.14274","title":"Proof Automation with Large Language Models","created":"2024-09-22","cited_by_count":22},{"id":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","cited_by_count":20},{"id":"2509.22908","title":"A benchmark for vericoding: formally verified program synthesis","created":"2025-09-26","cited_by_count":20},{"id":"2510.24592","title":"ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization","created":"2025-10-28","cited_by_count":20},{"id":"2410.16429","title":"Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4","created":"2024-10-21","cited_by_count":18},{"id":"2504.21230","title":"Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification","created":"2025-04-29","cited_by_count":17},{"id":"2511.03108","title":"miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward","created":"2025-11-05","cited_by_count":14},{"id":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","cited_by_count":11},{"id":"2510.15700","title":"ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations","created":"2025-10-17","cited_by_count":11},{"id":"2603.19329","title":"Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification","created":"2026-03-18","cited_by_count":11},{"id":"2502.17925","title":"LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction","created":"2025-02-25","cited_by_count":10},{"id":"2507.16331","title":"Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny","created":"2025-07-22","cited_by_count":10},{"id":"2510.25015","title":"VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus","created":"2025-10-28","cited_by_count":9},{"id":"2510.25427","title":"RLMEval: Evaluating Research-Level Neural Theorem Proving","created":"2025-10-29","cited_by_count":8},{"id":"2511.00125","title":"Inferring multiple helper Dafny assertions with LLMs","created":"2025-10-31","cited_by_count":4},{"id":"2601.12845","title":"Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles","created":"2026-01-19","cited_by_count":3},{"id":"2603.25810","title":"ExVerus: Verus Proof Repair via Counterexample Reasoning","created":"2026-03-26","cited_by_count":3},{"id":"1412.4395","title":"Dafny: Statically Verifying Functional Correctness","created":"2014-12-14","cited_by_count":2},{"id":"2508.02733","title":"What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus","created":"2025-08-01","cited_by_count":2}],"next_cursor":null}