Like most other chess programmers, I dislike Search Instability. Perhaps even more than others in that I would rather "write a program that's perfect rather than one that's strong." to paraphrase Bruce Moreland. (but ideally both.)
This inability to let go may stem from my background in theoretical computer science, or maybe just because I originally chose MTD-bi for my sunfish engine, rather than PV-search, and MTD is extraordinarily sensitive to search instability.
For many years I introduced changes to sunfish to guarantee stability: I key my TT be keyed by (pos, depth) so low depth values don't get "contaminated" by high depth search; and I clear it after each move, since values are path dependent through three-fold repetition.
Even with all those precautions, I was always worried that my search was not 100% correct. Enough that I have up working on it for many years. However, with the advent of Lean formal verification I eyed a chance to finally achieve peace of mind.
Like many others here, I'm not a fan of AI written chess engines. Engines that copy my code and ideas, without ever a human reading the code and appreciating the work/art that went into it. However, I don't actually know how to prove things in Lean, and the Claude does.
So what did I do? I first ported my engine to lean and formalized what it means for the engine to be consistent. Basically just my existing docstring formalized. Later I switched to using https://github.com/thomasnormal/lean-surfaces which defines the python semantics in lean, so I can work directly on the AST. That removes the risk that the port is not truthful.
The exercise led me to restructure how I do futility pruning. It is now done via a hard static cap, V(m) = min(pos.eval + move.value + margin, -search(child)). This was we can still skip searching the child if the cap fails to exceed gamma (alpha in PV) but we also have to cap the actual value if we do the search.
I also had to fix my LMR. In sunfish LMR is only basic on intrinsic move value, not sorted order. This is because the killer/TT move is tested before the move generation in the node runs, so we wouldn't know whether to prune the killer move.
Emboldened I also decided to also prove that the search always finds a mate if it's there. If given enough time/resources/depth... As expected this didn't play well with null-move pruning, and I had to replace it with null-move reductions at higher depth.
Null move pruning is now replaced by null move reduction (verification search) at least for higher depths (this is more standard.)
A (partially) unexpected benefit of this exercise was that it emboldened me to refactor some other parts of the engine, knowing that I wouædn thave to spend weeks worrying about search inconsistency edge cases. All in all I gained around 100 Elo, so that's nice.
formally verified sunfish
Moderator: Ras