Pith. sign in

REVIEW 3 major objections 5 minor 115 references

TreeThink packages modular asynchronous tree search so the same proof-search loop works across Lean, Rocq, Isabelle, and natural language.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-14 05:56 UTC pith:W2JEAO2C

load-bearing objection Solid systems library paper: multi-ITP async tree search with real code release; numbers are demos, not comparative science. the 3 major comments →

arxiv 2607.11258 v1 pith:W2JEAO2C submitted 2026-07-13 cs.CL

TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs

Burak S. Akbudak , Zeynel A. Ulu\c{s}an , Can S. Erer , G\"ozde G\"ul \c{S}ahin This is my paper
classification cs.CL
keywords neural theorem provingtree searchLean 4RocqIsabelle/HOLasynchronous inferenceLLM reasoningREPL verification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Researchers who want large language models to search for mathematical proofs usually rebuild the same scaffolding: how to expand partial proofs, score candidates, talk to a formal checker, and run everything without wasting GPU time. TreeThink claims to remove that duplication. It is an open Python library that plugs together standard tree-search methods, language-model policies, a range of node scorers, and live connections to the proof assistants Lean 4, Rocq, and Isabelle/HOL, while also supporting ordinary natural-language math problems. The same configuration can be pointed at different languages; asynchronous and batched execution is built in. On the miniF2F formal benchmark the library improves single-pass success rates, and on a small Isabelle subset concurrency yields up to a 6.3-times wall-clock speedup. On MATH500 it likewise lifts natural-language accuracy over single-pass and majority-vote baselines. The point is not a new state-of-the-art prover, but a reusable experimental chassis so later work can focus on better search or better evaluators instead of re-engineering infrastructure.

Core claim

A single modular, fully asynchronous tree-search library can host established search algorithms, vLLM-based policies, heterogeneous evaluators, and native REPL clients for Lean 4, Rocq, and Isabelle/HOL (plus natural language), and thereby support cross-language formal proof search and natural-language reasoning while delivering substantial wall-clock speedups from concurrency on the reported miniF2F and MATH500 setups.

What carries the argument

The interchangeable component stack—search methods (best-first, beam, MCTS and a rollout-free value-guided variant), policies, evaluators, and unified REPL clients—plus asynchronous batched execution and an LRU proof cache that together let the same search loop run against multiple formal languages and natural language.

Load-bearing premise

The reported accuracy gains and the 6.3-times speedup on a 32-problem Isabelle subset, obtained from single runs with different models per language and only a few evaluator choices, are taken as enough evidence that the library is a general reusable foundation rather than a narrow demonstration.

What would settle it

Re-run the same expansion budgets and concurrency settings on the full miniF2F test set for all three formal languages with fixed models and multi-seed averages; if pass-rate lifts disappear or the wall-clock speedup collapses under full load or different evaluators, the claim that the library is a reliable experimental chassis is falsified.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces TreeThink, an open-source modular Python library for fully asynchronous tree search in neural theorem proving. It decouples search algorithms (best-first, beam, traditional MCTS, and a rollout-free value-guided MCTS), vLLM-based policies, eight node evaluators (heuristic through neural/judge/tournament), and unified REPL clients for Lean 4, Rocq, and Isabelle/HOL, with natural-language support. The system is evaluated on miniF2F (cross-language formal search) and MATH500 (informal reasoning), reporting pass-rate lifts over pass@1 and up to 6.3× wall-clock speedup from asynchronous concurrency. Code is released under MIT on GitHub and as a PyPI package, with configuration via YAML/TOML and a CLI.

Significance. This is a practical systems contribution that fills a documented gap: general LLM tree-search libraries lack native formal-verifier integration, while NTP provers typically ship task-specific search stacks. The modular design, multi-ITP REPL clients, async/batched vLLM path, proof cache, and open MIT/PyPI release are concrete strengths that can reduce duplicated engineering in formal and informal mathematical reasoning research. The authors correctly scope the work as reusable infrastructure rather than a SOTA prover, include an explicit Limitations section, and provide reproducibility details (Appendix E). Those artifacts and the transparent capability-demo framing are the main reasons the contribution is valuable even with a narrow experimental suite.

major comments (3)
  1. [§4.1, Table 3] §4.1 and Table 3 present cross-language miniF2F pass rates, but each language uses a different policy model (DeepSeek-Prover-V2-7B for Lean, Qwen2.5-Coder-14B-Instruct for Isabelle, Qwen3.5-9B for Rocq). The text acknowledges model-availability constraints, yet the table and surrounding prose still read as a controlled cross-language comparison of search methods. Because language and model are confounded, the numbers support only per-language capability demos. The manuscript should state this limitation next to Table 3 and avoid any comparative language ranking based on these runs.
  2. [§4.2, Table 4] §4.2 and Table 4 report the headline 6.3× wall-clock speedup on a 32-problem random Isabelle subset, with single runs and no multi-seed averages (Table 8). Pass counts also move non-monotonically with concurrency (18→20→16). For a systems paper whose central performance claim is asynchronous throughput, either report variance over multiple subsets/seeds or more tightly qualify the 6.3× figure as illustrative of this specific setup rather than a general library property.
  3. [§4, Appendix D.2] Modularity of search methods and evaluators is a core claim (Table 1, §3, Appendix D.2), but main quantitative results use only BFTS/RF-MCTS with NormLenEvaluator (formal) and JudgeEvaluator (informal). Remaining methods and evaluators are covered only by unreported smoke tests. At least one additional evaluator or search method in the main tables—or concrete smoke-test outcomes on the held-out set—would better substantiate the modularity claim that the library is a reusable experimental foundation rather than a thin demo of a few configurations.
minor comments (5)
  1. [Abstract / title page] Abstract and opening: spacing glitches such as “TREETHINKon miniF2F” and the author-name character “Gözde Gül ¸ Sahin” should be cleaned.
  2. [Figure 1] Figure 1 caption is dense and mixes numbered steps with W-value notation; a short legend or clearer separation of Select/Expand/Evaluate/Verify would help readers new to NTP search loops.
  3. [Table 1] Table 1 uses “~” for evaluators/policies that “would not work in NTP out of the box”; a footnote defining “~” would make the comparison self-contained.
  4. [§3.1] §3.1 UCT formula is standard, but the rollout-free MCTS description should state explicitly how leaf values are initialized when the evaluator returns only a local score (no terminal reward), to avoid ambiguity for implementers.
  5. [Appendix E / Appendix A] Appendix E lists commit hash, package version, and hardware—excellent for reproducibility—but sampling temperature in the main formal runs (0.3 in Table 8 vs 1.0 in the YAML example) should be reconciled or explained.

Circularity Check

0 steps flagged

No circularity: systems library paper with empirical external-benchmark results, not a fitted or self-definitional derivation.

full rationale

TreeThink is an engineering/systems paper whose central claims are (i) a modular open-source library that composes established search algorithms, vLLM policies, heterogeneous evaluators, and unified REPL clients for Lean/Rocq/Isabelle/NL, and (ii) measured pass-rate lifts and wall-clock speedups on external benchmarks (miniF2F, MATH500) under stated configurations. There are no equations that define a quantity in terms of itself, no parameters fitted to data and then re-presented as predictions, no uniqueness theorems or ansätze imported from the authors’ own prior work, and no renaming of a known empirical pattern as a new derivation. Self-positioning against FETCH/LLM Reasoners/LiTS is comparative literature, not load-bearing self-citation. The reported 6.3× async speedup and pass@1 improvements are direct empirical measurements against external models and datasets (with Limitations already noting single runs and partial coverage). The derivation chain is therefore self-contained against external artifacts; circularity score is zero.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 1 invented entities

As a software-systems paper, load-bearing premises are tooling and experimental-setup assumptions rather than physical axioms or free parameters fitted to a scientific law. No invented particles or mediators. Free parameters are ordinary hyper-parameters of the search demos (budget, concurrency, length-norm exponent, model choice).

free parameters (4)
  • expansion_budget / max_children
    Default 512 expansions and 3 children per expansion control search cost and reported pass rates; chosen for the demos rather than derived.
  • async concurrency level
    Concurrency 1–16 is varied to produce the 6.3× wall-clock claim on a 32-problem subset; the peak speedup depends on this choice and hardware.
  • NormLenEvaluator length penalty alpha
    Length-normalization exponent (example 0.5 in config) shapes tree depth preference and is a tunable heuristic, not derived.
  • per-language policy model choice
    DeepSeek-Prover-V2-7B (Lean), Qwen2.5-Coder-14B (Isabelle), Qwen3.5-9B (Rocq), Llama3-8B (MATH500) are selected by availability/prior work; results are not model-agnostic.
axioms (4)
  • domain assumption External formal REPL servers correctly implement Lean 4 / Rocq / Isabelle type-checking and state extraction for the versions listed.
    All formal verification and several evaluators depend on Kimina Lean Server, isabelle-server, and rocq-ml-server behavior (§3.4).
  • domain assumption vLLM AsyncLLM sampling and pooling modes faithfully expose logprobs and reward-model scores used by evaluators.
    Policy and neural evaluators are built on vLLM interfaces (§3.2–3.3).
  • domain assumption miniF2F and MATH500 are appropriate capability benchmarks for the library demo (not SOTA claims).
    Evaluation design in §4 treats these datasets as sufficient to show cross-language and NL support.
  • standard math Standard tree-search algorithms (BFS, beam, UCT/MCTS) and cited evaluators behave as described in the literature when reimplemented modularly.
    Search and scoring components are adaptations of Pearl, Bisiani, Kocsis–Szepesvári, AlphaZero-style value backup, and prior NTP evaluators (§3.1–3.3).
invented entities (1)
  • TreeThink library (modular async NTP tree-search stack) independent evidence
    purpose: Provide reusable search, policy, evaluator, and multi-ITP REPL components so researchers avoid task-specific reimplementation.
    The library is the paper’s primary artifact; independent evidence is the public GitHub/PyPI release and reported runs, not an external physical prediction.

pith-pipeline@v1.1.0-grok45 · 18026 in / 3303 out tokens · 27799 ms · 2026-07-14T05:56:25.948527+00:00 · methodology

0 comments
read the original abstract

Tree search algorithms enable systematic exploration of the proof space in neural theorem proving. Existing LLM tree search libraries primarily target natural language reasoning and do not provide native integration with formal verifiers, while theorem proving systems often rely on task-specific search implementations. We introduce TreeThink, an open-source Python library for modular, fully asynchronous tree search in neural theorem proving. It integrates established tree search methods with vLLM-based inference pipelines and diverse node evaluation techniques, ranging from lightweight heuristics to neural evaluators. We support Lean~4, Rocq, and Isabelle/HOL alongside natural language. It connects directly to each language's Read-Eval-Print Loop (REPL) server for real-time verification and proof state extraction. We evaluate TreeThink on miniF2F and MATH500, demonstrating cross-language formal proof search, natural language reasoning support, and up to 6.3$\times$ wall-clock speedup from asynchronous execution. Source code is released under the MIT license at https://github.com/GGLAB-KU/treethink , and the library is accessible as a downloadable package at https://pypi.org/project/treethink/ .

Figures

Figures reproduced from arXiv: 2607.11258 by Burak S. Akbudak, Can S. Erer, G\"ozde G\"ul \c{S}ahin, Zeynel A. Ulu\c{s}an.

Figure 1
Figure 1. Figure 1: NTP tree search process. 1. Select: search method selects a node using a search algorithm. 2. Ex￾pand: the policy LLM generates child nodes. 3. Evalu￾ate: evaluator strategy scores the generated nodes. W stands for the value assigned to a node. 4. Verify: exter￾nal systems verify the correctness of the proof. Main op￾erations in individual sections are in red while batched processes are in blue. combines t… view at source ↗
Figure 2
Figure 2. Figure 2: Overview of the system. Our framework accepts search configuration as a YAML file and a dataset registry. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

115 extracted references · 3 canonical work pages

  1. [1]

    Dang Hoang Anh, Vu Tran, and Le Minh Nguyen. 2025. Analyzing logical fallacies in large language models: A study on hallucination in mathematical reasoning. In New Frontiers in Artificial Intelligence, pages 179--195, Singapore. Springer Nature Singapore

    2025

  2. [3]

    R. Bisiani. 1987. Beam search. In S. C. Shapiro, editor, Encyclopedia of Artificial Intelligence, pages 56--58. John Wiley and Sons

    1987

  3. [6]

    Guoxiong Gao, Zeming Sun, Jiedong Jiang, Yutong Wang, Jingda Xu, Peihao Wu, Bryan Dai, and Bin Dong. 2026. https://arxiv.org/abs/2605.13137 Leansearch v2: Global premise retrieval for lean 4 theorem proving . Preprint, arXiv:2605.13137

    Pith/arXiv arXiv 2026

  4. [7]

    Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshorn, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, and 542 others. 2024. https://arxiv.org/abs/2407.21783 The llama 3...

    Pith/arXiv arXiv 2024

  5. [9]

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the math dataset. NeurIPS

    2021

  6. [10]

    Jilin Hu, Jianyu Zhang, Yongwang Zhao, and Talia Ringer. 2025. https://arxiv.org/abs/2505.15740 Hybridprover: Augmenting theorem proving with llm-driven proof synthesis and refinement . Preprint, arXiv:2505.15740

    Pith/arXiv arXiv 2025

  7. [14]

    Peter Koepke, Anton Lorenzen, and Boris Shminke. 2022. Cicm'22 system entries. In Intelligent Computer Mathematics, pages 344--348, Cham. Springer International Publishing

    2022

  8. [15]

    Gonzalez, Hao Zhang, and Ion Stoica

    Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. 2023. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles

    2023

  9. [16]

    Xinzhe Li and Yaguang Tao. 2026. https://aclanthology.org/2026.acl-demo.5/ L i TS : A modular framework for LLM tree search . In Proceedings of the 64th Annual Meeting of the A ssociation for C omputational L inguistics (Volume 3: System Demonstrations) , pages 47--56, San Diego, California, United States. Association for Computational Linguistics

    2026

  10. [17]

    Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. 2025. https://arxiv.org/abs/2412.20735 Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving . Preprint, arXiv:2412.20735

    Pith/arXiv arXiv 2025

  11. [18]

    Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. 2024. https://openreview.net/forum?id=zlw6AHwukB A survey on deep learning for theorem proving . In First Conference on Language Modeling

    2024

  12. [19]

    Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. 2024. https://openreview.net/forum?id=v8L0pN6EOi Let's verify step by step . In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024 . OpenReview.net

    2024

  13. [20]

    Sadegh Mahdavi, Branislav Kisacanin, Shubham Toshniwal, Wei Du, Ivan Moshkov, George Armstrong, Renjie Liao, Christos Thrampoulidis, and Igor Gitman. 2026. https://openreview.net/forum?id=NsC3NFsavi Scaling generative verifiers for natural language mathematical proof verification and selection . In Forty-third International Conference on Machine Learning

    2026

  14. [21]

    Smith, Mateusz Paprocki, Ond r ej C ert\' i k, Sergey B

    Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ond r ej C ert\' i k, Sergey B. Kirpichev, Matthew Rocklin, Amit Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, and 8 others. 2017. https://doi.org/1...

    doi:10.7717/peerj-cs.103 2017

  15. [22]

    Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg

    2002

  16. [23]

    Judea Pearl. 1984. https://api.semanticscholar.org/CorpusID:59879760 Heuristics - intelligent search strategies for computer problem solving . In Addison-Wesley series in artificial intelligence

    1984

  17. [25]

    Tom Preston-Werner and 1 others. 2021. TOML : Tom's obvious, minimal language. https://toml.io/en/

    2021

  18. [26]

    Qwen Team . 2026. https://qwen.ai/blog?id=qwen3.5 Qwen3.5 : Towards native multimodal agents

    2026

  19. [27]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. 2025. https://arxiv.org/abs/2504.21801 Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for sub...

    Pith/arXiv arXiv 2025

  20. [28]

    Marco Dos Santos, Haiming Wang, Hugues de Saxcé, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu, and Jia Li. 2025. https://arxiv.org/abs/2504.21230 Kimina lean server: Technical report . Preprint, arXiv:2504.21230

    arXiv 2025

  21. [30]

    Sifre, Dharshan Kumaran, Thore Graepel, Timothy P

    David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, L. Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis. 2017. https://api.semanticscholar.org/CorpusID:33081038 Mastering chess and shogi by self-play with a general reinforcement learning algorithm . ...

    Pith/arXiv arXiv 2017

  22. [31]

    Théo Stoskopf. 2025. rocq-ml-toolbox. https://github.com/LLM4Rocq/rocq-ml-toolbox

    2025

  23. [32]

    The Coq Dev Team . 2024. The Coq reference manual -- release 8.19.0. https://coq.inria.fr/doc/V8.19.0/refman

    2024

  24. [33]

    Ante Wang, Linfeng Song, Ye Tian, Dian Yu, Haitao Mi, Xiangyu Duan, Zhaopeng Tu, Jinsong Su, and Dong Yu. 2025. https://arxiv.org/abs/2502.11183 Don't getlost in the trees: Streamlining llm reasoning by overcoming tree search exploration pitfalls . Preprint, arXiv:2502.11183

    Pith/arXiv arXiv 2025

  25. [36]

    Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. 2023 b . https://openreview.net/forum?id=1PL1NIMMrw Self-consistency improves chain of thought reasoning in language models . In The Eleventh International Conference on Learning Representations

    2023

  26. [37]

    Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin, and Kai Chen. 2025. https://openreview.net/forum?id=qwCqeIg5iI Intern LM 2.5-stepprover: Advancing automated theorem proving via critic-guided search . In 2nd AI for Math Workshop @ ICML 2025

    2025

  27. [40]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. Leandojo: theorem proving with retrieval-augmented language models. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS '23, Red Hook, NY, USA. Curran Associates Inc

    2023

  28. [41]

    Jiachen Yu, Shaoning Sun, Xiaohui Hu, Jiaxu Yan, Kaidong Yu, and Xuelong Li. 2025. https://arxiv.org/abs/2502.11689 Improve llm-as-a-judge ability as a general ability . Preprint, arXiv:2502.11689

    Pith/arXiv arXiv 2025

  29. [42]

    Dan Zhang, Sining Zhoubian, Ziniu Hu, Yisong Yue, Yuxiao Dong, and Jie Tang. 2024. https://openreview.net/forum?id=8rcFOqEud5 Re ST - MCTS *: LLM self-training via process reward guided tree search . In The Thirty-eighth Annual Conference on Neural Information Processing Systems

    2024

  30. [44]

    The Lean 4 Theorem Prover and Programming Language , booktitle =

    Leonardo de Moura and Sebastian Ullrich , editor =. The Lean 4 Theorem Prover and Programming Language , booktitle =. 2021 , url =. doi:10.1007/978-3-030-79876-5\_37 , timestamp =

    doi:10.1007/978-3-030-79876-5 2021

  31. [45]

    The Coq Reference Manual -- Release 8.19.0

    The Coq Dev Team. The Coq Reference Manual -- Release 8.19.0. 2024

    2024

  32. [46]

    , title =

    Nipkow, Tobias and Wenzel, Markus and Paulson, Lawrence C. , title =. 2002 , isbn =

    2002

  33. [47]

    and Hajishirzi, Hannaneh

    Lambert, Nathan and Pyatkin, Valentina and Morrison, Jacob and Miranda, LJ and Lin, Bill Yuchen and Chandu, Khyathi and Dziri, Nouha and Kumar, Sachin and Zick, Tom and Choi, Yejin and Smith, Noah A. and Hajishirzi, Hannaneh. R eward B ench: Evaluating Reward Models for Language Modeling. Findings of the Association for Computational Linguistics: NAACL 20...

    doi:10.18653/v1/2025.findings-naacl.96 2025

  34. [48]

    P rocess B ench: Identifying Process Errors in Mathematical Reasoning

    Zheng, Chujie and Zhang, Zhenru and Zhang, Beichen and Lin, Runji and Lu, Keming and Yu, Bowen and Liu, Dayiheng and Zhou, Jingren and Lin, Junyang. P rocess B ench: Identifying Process Errors in Mathematical Reasoning. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2025. doi:10.18653/v1/20...

    doi:10.18653/v1/2025.acl-long.50 2025

  35. [49]

    Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles , year=

    Efficient Memory Management for Large Language Model Serving with PagedAttention , author=. Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles , year=

  36. [50]

    2025 , eprint=

    Kimina Lean Server: Technical Report , author=. 2025 , eprint=

    2025

  37. [51]

    Proceedings of the 6th International Conference on Advanced Functional Programming , pages =

    Norell, Ulf , title =. Proceedings of the 6th International Conference on Advanced Functional Programming , pages =. 2008 , isbn =

    2008

  38. [52]

    Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics) , year =

    S. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics) , year =

  39. [53]

    Training language models to follow instructions with human feedback , url =

    Ouyang, Long and Wu, Jeffrey and Jiang, Xu and Almeida, Diogo and Wainwright, Carroll and Mishkin, Pamela and Zhang, Chong and Agarwal, Sandhini and Slama, Katarina and Ray, Alex and Schulman, John and Hilton, Jacob and Kelton, Fraser and Miller, Luke and Simens, Maddie and Askell, Amanda and Welinder, Peter and Christiano, Paul F and Leike, Jan and Lowe,...

  40. [54]

    ArXiv , year=

    Constitutional AI: Harmlessness from AI Feedback , author=. ArXiv , year=

  41. [55]

    2017 , eprint=

    Proximal Policy Optimization Algorithms , author=. 2017 , eprint=

    2017

  42. [56]

    , title =

    BRADLEY, RALPH ALLAN and TERRY, MILTON E. , title =. Biometrika , volume =. 1952 , month =. doi:10.1093/biomet/39.3-4.324 , url =

    doi:10.1093/biomet/39.3-4.324 1952

  43. [57]

    Francis Song and Noah Y

    Jonathan Uesato and Nate Kushman and Ramana Kumar and H. Francis Song and Noah Y. Siegel and Lisa Wang and Antonia Creswell and Geoffrey Irving and Irina Higgins , title =. CoRR , volume =. 2022 , url =. doi:10.48550/ARXIV.2211.14275 , eprinttype =. 2211.14275 , timestamp =

    Pith/arXiv arXiv doi:10.48550/arxiv.2211.14275 2022

  44. [58]

    The Twelfth International Conference on Learning Representations,

    Hunter Lightman and Vineet Kosaraju and Yuri Burda and Harrison Edwards and Bowen Baker and Teddy Lee and Jan Leike and John Schulman and Ilya Sutskever and Karl Cobbe , title =. The Twelfth International Conference on Learning Representations,. 2024 , url =

    2024

  45. [59]

    Policy Gradient Methods for Reinforcement Learning with Function Approximation , url =

    Sutton, Richard S and McAllester, David and Singh, Satinder and Mansour, Yishay , booktitle =. Policy Gradient Methods for Reinforcement Learning with Function Approximation , url =

  46. [60]

    , title =

    Williams, Ronald J. , title =. 1992 , issue_date =. doi:10.1007/BF00992696 , journal =

    doi:10.1007/bf00992696 1992

  47. [61]

    Jordan and Pieter Abbeel , editor =

    John Schulman and Philipp Moritz and Sergey Levine and Michael I. Jordan and Pieter Abbeel , editor =. High-Dimensional Continuous Control Using Generalized Advantage Estimation , booktitle =. 2016 , url =

    2016

  48. [62]

    Zhihong Shao and Peiyi Wang and Qihao Zhu and Runxin Xu and Junxiao Song and Mingchuan Zhang and Y. K. Li and Y. Wu and Daya Guo , title =. CoRR , volume =. 2024 , url =. doi:10.48550/ARXIV.2402.03300 , eprinttype =. 2402.03300 , timestamp =

    Pith/arXiv arXiv doi:10.48550/arxiv.2402.03300 2024

  49. [63]

    1984 , isbn =

    Pearl, Judea , title =. 1984 , isbn =

    1984

  50. [64]

    1976 , school=

    The Harpy Speech Recognition System , author=. 1976 , school=

    1976

  51. [65]

    and Powley, Edward and Whitehouse, Daniel and Lucas, Simon M

    Browne, Cameron B. and Powley, Edward and Whitehouse, Daniel and Lucas, Simon M. and Cowling, Peter I. and Rohlfshagen, Philipp and Tavener, Stephen and Perez, Diego and Samothrakis, Spyridon and Colton, Simon , journal=. A Survey of Monte Carlo Tree Search Methods , year=

  52. [66]

    ArXiv , year=

    Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm , author=. ArXiv , year=

  53. [67]

    CoRR , volume =

    Stanislas Polu and Ilya Sutskever , title =. CoRR , volume =. 2020 , url =. 2009.03393 , timestamp =

    Pith/arXiv arXiv 2020

  54. [68]

    and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , title =

    Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , title =. Proceedings of the 37th International Conference on Neural Information Processing Systems , articleno =. 2023 , publisher =

    2023

  55. [69]

    and Ringer, Talia and Brun, Yuriy , title =

    First, Emily and Rabe, Markus N. and Ringer, Talia and Brun, Yuriy , title =. 2023 , isbn =. doi:10.1145/3611643.3616243 , booktitle =

    doi:10.1145/3611643.3616243 2023

  56. [70]

    CoRR , volume =

    Kunhao Zheng and Jesse Michael Han and Stanislas Polu , title =. CoRR , volume =. 2021 , url =. 2109.00110 , timestamp =

    Pith/arXiv arXiv 2021

  57. [71]

    2025 , eprint=

    HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving , author=. 2025 , eprint=

    2025

  58. [72]

    2023 , eprint=

    ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics , author=. 2023 , eprint=

    2023

  59. [73]

    Proceedings of the 38th International Conference on Neural Information Processing Systems , articleno =

    Tsoukalas, George and Lee, Jasper and Jennings, John and Xin, Jimmy and Ding, Michelle and Jennings, Michael and Thakur, Amitayush and Chaudhuri, Swarat , title =. Proceedings of the 38th International Conference on Neural Information Processing Systems , articleno =. 2024 , isbn =

    2024

  60. [74]

    BFS -Prover: Scalable Best-First Tree Search for LLM -based Automatic Theorem Proving

    Xin, Ran and Xi, Chenguang and Yang, Jie and Chen, Feng and Wu, Hang and Xiao, Xia and Sun, Yifan and Zheng, Shen and Ding, Ming. BFS -Prover: Scalable Best-First Tree Search for LLM -based Automatic Theorem Proving. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2025. doi:10.18653/v1/2025....

    doi:10.18653/v1/2025.acl-long.1565 2025

  61. [75]

    HyperTree Proof Search for Neural Theorem Proving , booktitle =

    Guillaume Lample and Timoth. HyperTree Proof Search for Neural Theorem Proving , booktitle =. 2022 , url =

    2022

  62. [76]

    Proceedings of the 35th International Conference on Neural Information Processing Systems , articleno =

    Wu, Minchao and Norrish, Michael and Walder, Christian and Dezfouli, Amir , title =. Proceedings of the 35th International Conference on Neural Information Processing Systems , articleno =. 2021 , isbn =

    2021

  63. [77]

    DT -Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function

    Wang, Haiming and Yuan, Ye and Liu, Zhengying and Shen, Jianhao and Yin, Yichun and Xiong, Jing and Xie, Enze and Shi, Han and Li, Yujun and Li, Lin and Yin, Jian and Li, Zhenguo and Liang, Xiaodan. DT -Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. Proceedings of the 61st Annual Meeting of the Associati...

    doi:10.18653/v1/2023.acl-long.706 2023

  64. [78]

    Ren and Qihao Zhu and Bo Liu and Chong Ruan and Wenda Li and Xiaodan Liang , booktitle=

    Huajian Xin and Daya Guo and Zhihong Shao and Z.Z. Ren and Qihao Zhu and Bo Liu and Chong Ruan and Wenda Li and Xiaodan Liang , booktitle=. Advancing Theorem Proving in. 2024 , url=

    2024

  65. [79]

    Huajian Xin and Z. Z. Ren and Junxiao Song and Zhihong Shao and Wanjia Zhao and Haocheng Wang and Bo Liu and Liyue Zhang and Xuan Lu and Qiushi Du and Wenjun Gao and Qihao Zhu and Dejian Yang and Zhibin Gou and Z. F. Wu and Fuli Luo and Chong Ruan , title =. CoRR , volume =. 2024 , url =. doi:10.48550/ARXIV.2408.08152 , eprinttype =. 2408.08152 , timestamp =

    Pith/arXiv arXiv doi:10.48550/arxiv.2408.08152 2024

  66. [80]

    2025 , eprint=

    DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition , author=. 2025 , eprint=

    2025

  67. [81]

    2024 , eprint=

    Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters , author=. 2024 , eprint=

    2024

  68. [82]

    2024 , eprint=

    Generative Reward Models , author=. 2024 , eprint=

    2024

  69. [83]

    2025 , eprint=

    GenPRM: Scaling Test-Time Compute of Process Reward Models via Generative Reasoning , author=. 2025 , eprint=

    2025

  70. [84]

    2025 , eprint=

    Inference-Time Scaling for Generalist Reward Modeling , author=. 2025 , eprint=

    2025

  71. [85]

    and Zhang, Hao and Gonzalez, Joseph E

    Zheng, Lianmin and Chiang, Wei-Lin and Sheng, Ying and Zhuang, Siyuan and Wu, Zhanghao and Zhuang, Yonghao and Lin, Zi and Li, Zhuohan and Li, Dacheng and Xing, Eric P. and Zhang, Hao and Gonzalez, Joseph E. and Stoica, Ion , title =. Proceedings of the 37th International Conference on Neural Information Processing Systems , articleno =. 2023 , publisher =

    2023

  72. [86]

    and Feng, Shi , title =

    Panickssery, Arjun and Bowman, Samuel R. and Feng, Shi , title =. Proceedings of the 38th International Conference on Neural Information Processing Systems , articleno =. 2024 , isbn =

    2024

  73. [87]

    and Yilmaz, Emine and Shi, Shuming and Tu, Zhaopeng , booktitle =

    Ye, Fanghua and Yang, Mingming and Pang, Jianhui and Wang, Longyue and Wong, Derek F. and Yilmaz, Emine and Shi, Shuming and Tu, Zhaopeng , booktitle =. Benchmarking LLMs via Uncertainty Quantification , url =. doi:10.52202/079017-0491 , editor =

    doi:10.52202/079017-0491

  74. [88]

    2025 , eprint=

    Reasoning Through Execution: Unifying Process and Outcome Rewards for Code Generation , author=. 2025 , eprint=

    2025

  75. [89]

    2024 , eprint=

    Lessons from Formally Verified Deployed Software Systems (Extended version) , author=. 2024 , eprint=

    2024

  76. [90]

    , title =

    Gauthier, Thibault and Brown, Chad E. , title =. 15th International Conference on Interactive Theorem Proving (ITP 2024) , pages =. 2024 , volume =. doi:10.4230/LIPIcs.ITP.2024.16 , annote =

    work page doi:10.4230/lipics.itp.2024.16 2024

  77. [91]

    Manning and Stefano Ermon and Chelsea Finn , editor =

    Rafael Rafailov and Archit Sharma and Eric Mitchell and Christopher D. Manning and Stefano Ermon and Chelsea Finn , editor =. Direct Preference Optimization: Your Language Model is Secretly a Reward Model , booktitle =. 2023 , url =

    2023

  78. [92]

    PRMBench:

    Mingyang Song and Zhaochen Su and Xiaoye Qu and Jiawei Zhou and Yu Cheng , editor =. PRMBench:. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers),. 2025 , url =

    2025

  79. [93]

    2025 , url=

    RewardCode: Training Generalist Code Reward Model via Pairwise Reinforcement Learning , author=. 2025 , url=

    2025

  80. [94]

    Chi and Quoc V

    Jason Wei and Xuezhi Wang and Dale Schuurmans and Maarten Bosma and Brian Ichter and Fei Xia and Ed H. Chi and Quoc V. Le and Denny Zhou , editor =. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models , booktitle =. 2022 , url =

    2022

Showing first 80 references.