In other words - say you have a model that is semi-smart, often makes mistakes in logic, but sometimes gives valid answers. You use it to “brainstorm” physical equations and then use formal provers to weed out the correct answer.
Even if the llm is correct 0.001% of the time, it’s still better than the current algorithms which are essentially brute forcing.