Expected Work Search: Combining Win Rate and Proof Size Estimation
We propose Expected Work Search (EWS), a new game solving algorithm. EWS combines win rate estimation, as used in Monte Carlo Tree Search, with proof size estimation, as used in Proof Number Search. The search efficiency of EWS stems from minimizing a novel notion of Expected Work, which predicts the expected computation required to solve a position. EWS outperforms traditional solving algorithms on the games of Go and Hex. For Go, we present the first solution to the empty 5x5 board with the commonly used positional superko ruleset. For Hex, our algorithm solves the empty 8x8 board in under 4 minutes. Experiments show that EWS succeeds both with and without extensive domain-specific knowledge.
Code (0)
등록된 구현이 없습니다.
Tasks
PositionSimilar Papers 제목 키워드 기반
Combining Monte-Carlo Tree Search with Proof-Number Search
Proof-Number Search (PNS) and Monte-Carlo Tree Search (MCTS) have been successfully applied for decision making in a range of games. This paper proposes a new approach called PN-MCTS that combines these two tree-search m…
Decision MakingAn elementary proof of the dual representation of Expected Shortfall
We provide an elementary proof of the dual representation of Expected Shortfall on the space of integrable random variables over a general probability space. Unlike the results in the extant literature, our proof only ex…
Perspectives on neural proof nets
In this paper I will present a novel way of combining proof net proof search with neural networks. It contrasts with the 'standard' approach which has been applied to proof search in type-logical grammars in various diff…
Graph GenerationProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction
We propose ProofNet++, a neuro-symbolic framework that enhances automated theorem proving by combining large language models (LLMs) with formal proof verification and self-correction mechanisms. Current LLM-based systems…
Automated Theorem ProvingSimplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
The challenge of formal proof generation has a rich history, but with modern techniques, we may finally be at the stage of making actual progress in real-life mathematical problems. This paper explores the integration of…
Language ModelingLanguage ModellingLarge Language Model