[truculent]

If you use a formal system with a checker/compiler, there are certain properties that you can guarantee with essentially total certainty. I’m not sure a stochastic system like ML can ever do that.

Perhaps there is research on providing mathematical guarantees and constraints on complex models like neural networks? If not, it feels like it would be harder to give a model a high degree of control. Although embedding the model in a system that did provide guarantees (e.g. using a compiler) might be a pragmatic solution?

[flooo]

Stochastic methods may not be able to do so in isolation, but they can be used in tandem with other approaches such as in “A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving” https://ojs.aaai.org/index.php/AAAI/article/view/16780/16587

[matijash]

yep that would be really interesting! If e.g. the target generated code was some language with high type safety or a DSL whose compilation already guarantees certain properties.