3 ms·
Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...
by c-cube 4y ago
Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...
- zmgsabst 4y agoNope — research only I’m afraid; and currently just migrating to difference equations in numpy (with a focus on Numba GPU upgrades later). Currently moving shape types to digital image transforms; next up is Zn. https://www.zmgsabstract.com/whitepapers/shapes-as-digital-images https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i... https://www.zmgsabstract.com/whitepapers/shapes-have-operations https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
- raphlinus 4y agoDo not nerd snipe me! There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems. If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it. Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU. [1]: https://arxiv.org/abs/2205.11659 https://arxiv.org/abs/2205.11659 [2]: https://arxiv.org/abs/1608.02644 https://arxiv.org/abs/1608.02644 [3]: https://www.deepmind.com/publications/proving-theorems-using-incremental-learning-and-hindsight-experience-replay https://www.deepmind.com/publications/proving-theorems-using...
- zmgsabst 4y agoWould you be willing to elaborate on what you find to be strengths of Metamath Zero?