Comment by westurner

If you train an LLM on only formally verified code, it should not be expected to generate formally verified code.

Similarly, if you train an LLM on only published ScholarlyArticles ['s abstracts], it should not be expected to generate publishable or true text.

Traceability for Retraction would be necessary to prevent lossy feedback.