Without analytical thinking how else would you come to conviction that two functions are identical, for a computationally unfeasible number of possible inputs?

Formal logic / formal proofs. We have good systems for verifying that.

The proper flow is that you use LLM to generate decompilation steps, along with potential proofs, and then use old algorithms from 1970s that verify that the steps are correct.

Source: I built a decompiler for EVM, arguably the best one on the market, and to some extent it was how it worked (and others comparable in class).

The issue was always the exploration of possible transformations of code, once you manage to find the right ones (which LLMs can propose way better than old hard coded rules and SMT solvers), it's simple to verify that the transformations are correct.