{"aixiv_id":"2608.00004","url":"https://aixiv.online/abs/2608.00004","pdf_url":"https://arxiv.org/pdf/2205.11491","title":"HyperTree Proof Search for Neural Theorem Proving","abstract":"We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by the recent success of AlphaZero. Our model learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.","authors":["Guillaume Lample","Marie-Anne Lachaux","Thibaut Lavril","Xavier Martinet","Amaury Hayat","Gabriel Ebner","Aurélien Rodriguez","Timothée Lacroix"],"primary_category":"cs.AI","categories":["cs.AI","cs.LO"],"published":"2022-05-23","updated_at":"2026-08-27T09:54:17.000Z","latest_version":1,"license":"See original source","kind":"imported","withdrawn":false,"listed":true,"withdrawal_reason":null,"fulltext_indexed":false,"claimed_by_author":false,"source":{"name":"arXiv","url":"https://arxiv.org/abs/2205.11491"},"repository":null,"ai_process":{"models":null,"contribution_level":null,"has_process_summary":false,"has_prompts_harness":false,"has_verification_notes":false,"has_negative_results":false,"trace_url":null},"reproduction_status":"unverified","editors_pick":false,"editorial_summary":"HyperTree Proof Search: online MCTS-style search over tactics with a learned critic, trained on Lean and Metamath — a clean design for the search half of neural theorem proving.","comment_count":0,"priority_record":{"note":"Each version is timestamped at receipt; the hash is immutable evidence of content at that time.","versions":[{"version":1,"submitted_utc":"2026-08-27T09:54:17.000Z","content_hash":"sha256:863534de44aaa16c8ad6c105d33709d2f93cb4fb82e1c98ffef49cf8efb83fbf","hash_covers":"metadata-record","has_pdf":false,"source_url":null,"changelog":"Imported from arXiv by aiXiv editors"}]},"process_summary":null,"prompts_harness":null,"verification_notes":null,"negative_results":null,"reproduction_reports":[],"bibtex_url":"https://aixiv.online/bibtex/2608.00004"}