6 citations · 6 across the 3 of their papers we have counts for
3 papers
cs.AI2021
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Minchao Wu, Takeshi Tsukada, Hiroshi Unno +2
Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Desp…
cs.LG2021★ 6 cited
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Minchao Wu, Michael Norrish, Christian Walder +1
We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tacti…
cs.LO2021
A bi-directional extensible interface between Lean and Mathematica
Robert Y. Lewis, Minchao Wu
We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other…