3 ms·
I agree they'd be better for improving something human driven. I previously suggested plugging learning architectures provers to either spot opportunities to fe
by nickpsecurity 9y ago
I agree they'd be better for improving something human driven. I previously suggested plugging learning architectures provers to either spot opportunities to feed terms to automated solvers or create new tactics. Similarly, they could augment the automated solvers to improve their heuristics. Improving heuristics or models of data that changes quite a bit in different use cases seems to be the strong suite of these learning architectures. Whereas, there's already efficient algorithms for things like search or validating stuff. Might as well keep them in initial design attempts.
- zero_k 9y agoImproving heuristics... everybody has been doing that, but based on _very_ sparse information, mostly just running times and number of conflicts&decisions. I leads to poor understanding and slow improvement of heuristics. I think we ought to collect a lot more data, which would allow for better heuristics. But collecting data incurs running overhead, so it must be configurable -- collect when not in a "competition mode" and analyse, then during in the competition, only collect the data really needed for the computed prediction algorithm to correctly function.