Proof Extraction for Logical Neural Networks

Abstract

Automated Theorem Provers (ATPs) are widely used for the verification of logicalstatements. Explainability is one of the key advantages of ATPs: providing anexpert readable proof path which shows the inference steps taken to concludecorrectness. Conversely, Neuro-Symbolic Networks (NSNs) that perform theoremproving, do not have this capability. We propose a proof-tracing and filteringalgorithm to provide explainable reasoning in the case of Logical Neural Networks(LNNs), a special type of Neural-Theorem Prover (NTP).

Cite

Text

Lebese et al. "Proof Extraction for Logical Neural Networks." NeurIPS 2021 Workshops: AIPLANS, 2021.

Markdown

[Lebese et al. "Proof Extraction for Logical Neural Networks." NeurIPS 2021 Workshops: AIPLANS, 2021.](https://mlanthology.org/neuripsw/2021/lebese2021neuripsw-proof/)

BibTeX

@inproceedings{lebese2021neuripsw-proof,
  title     = {{Proof Extraction for Logical Neural Networks}},
  author    = {Lebese, Thabang and Makondo, Ndivhuwo and Cornelio, Cristina and Khan, Naweed},
  booktitle = {NeurIPS 2021 Workshops: AIPLANS},
  year      = {2021},
  url       = {https://mlanthology.org/neuripsw/2021/lebese2021neuripsw-proof/}
}