| ▲ | TorchLean: Formalizing Neural Networks in Lean(leandojo.org) | |||||||
| 28 points by matt_d 3 days ago | 3 comments | ||||||||
| ▲ | westurner 21 minutes ago | parent | next [-] | |||||||
How could this lend insight into why Fast Fourier Transform approximates self-attention? > Because self-attention can be replaced with FFT for a loss in accuracy and a reduction in kWh [1], I suspect that the Quantum Fourier Transform can also be substituted for attention in LLMs. [1] "Fnet: Mixing tokens with fourier transforms" (2021) https://arxiv.org/abs/2105.03824 .. "Google Replaces BERT Self-Attention with Fourier Transform: 92% Accuracy, 7 Times Faster on GPUs" https://syncedreview.com/2021/05/14/deepmind-podracer-tpu-ba... "Why formalize mathematics – more than catching errors" (2025) https://news.ycombinator.com/item?id=45695541 Can the QFT Quantum Fourier Transform (and IQFT Inverse Quantum Fourier Transform) also be substituted for self-attention in LLMs, and do Lean formalisms provide any insight into how or why? | ||||||||
| ▲ | measurablefunc 2 hours ago | parent | prev [-] | |||||||
I guess the next step would be adding support for quantized arithmetic. | ||||||||
| ||||||||