What about real symbolics in neuro-symbolics approach: natural language semantics

[alexandre-emmanuel]

I have checked both preprints "2406.18532v1 Symbolic Learning Enables Self-Evolving Agents" and "2410.02823v1 Domain-Aware Neurosymbolic Agents" and I see that people are using natural language as a symbolic part. Although such approch can be good and it is certainly doable with LLMs, there is still one more step in the direction of symbolics: natural language has formal semantics, that allows to translate it into more or less expressive logics automatically - https://www.grammaticalframework.org/. And there are papers that translate natural language into type theories https://ncatlab.org/nlab/show/dependent+type+theoretic+methods+in+natural+language+semantics - and the practical languge for the type theories is the one that is used by one or another proof assistant, e.g. Coq. And so - natural language translations can directly benefit for any reasoning mechanisms that are or will be implemented in Coq of other assitant. Even more, the translations are being made even in the most advanced formalisms https://www.researchgate.net/publication/320704539_Copredication_in_homotopy_type_theory

One may argue, that natural language is too rich. But it is not so. Natural language has grammar of mildly sensitive context free grammar (if I am not mistake, I have no reference at hand for this, but there was paper which considered it - it is certainly just mildly more expressive than the usual programming languages, this is clear, because language is used by the people of all sorts). And type theories are ever evolving - e.g. there is modal HoTT.

So - maybe - for doing legal reasoning, engineering, mathematical reasoning in the agents - one should really go to the full symbolism? I have looked some time ago on OpenCog and they have this translation of natural language, but they are translating in very non-expressive formalism in which little can be done (Aristotelian fragment of FOL).

So - what about this kind of symbolism? Are there thoughts about implementing it?