DeepGrail Proof Net

This repository contains a Python implementation of Neural Proof Net using TLGbank data.

This code was designed to work with the DeepGrail Tagger and DeepGrail Linker.

In this version the tagger is not retrained with the linker. Meaning they are both trained separately in training phase but in inference phase, predictions of tagger feeds inputs of linker.

Usage

Installation

Python 3.9.10 (Warning don't use Python 3.10+)

Clone the project locally.

Libraries installation

Run the script init.sh

Optional : Upload the .pt files containing models weights in the models directory.

Structure

The structure should look like this :

.
.
├── Configuration                    # Configuration
│   ├── Configuration.py             # Contains the function to execute for config
│   └── config.ini                   # contains parameters
├── requirements.txt                 # librairies needed
├── Datasets                         # TLGbank data with links
├── SuperTagger                      # The Supertagger directory (that you need 
│    ├── Datasets                    # TLGbank data with supertags
│    └──  SuperTagger                # BertForTokenClassification
│       ├── SuperTagger.py           # Main class
│       ├── Tagging_bert_model.py # Bert model
│       ├── SymbolTokenizer       # Tags tokenizer
│       └── SentencesTokenizer    # Words tokenizer
├── Linker                           # The Linker directory (that you need to install)
│    ├── ...
│    └── Linker.py                   # Linker class containing the neural network
├── NeuralProofNet                   # The NeuralProofNet directory
│    ├── utils_proofnet              # utils for NeuralProofNet
│    └── NeuralProofNet.py           # NeuralProofNet class
├── models                           
│    ├── linker.pt                   # OPTIONAL : pretrained linker 
│    └── supertagger.pt              # pretrained supertagger 
├── Output                           # Directory with models backups while training
├── TensorBoard                      # Directory with stats
├── train_neuralproofnet.py          # train for linker with the pretrained supertager
├── train_supertagger.py             # train for the supertager
├── predict_supertags.py             # tags predictions
└── predict_links.py                 # links predictions

Dataset format

The sentences should be in a column "X", the links with '_x' postfix should be in a column "Y" and the categories in a column "Z". For the links each atom_x goes with the one and only other atom_x in the sentence.

Utils

In order to load m2_dataset.csv, you can use utils.read_csv_pgbar(...). This function return a pandas dataframe.

Training

Training of supertagger

df = read_csv_pgbar(file_path,1000)
texts = df['X'].tolist()
tags = df['Z'].tolist()

#Dict for convert ID to token (The dict is save with the model for prediction)
index_to_super = load_obj('Datasets/index_to_super') 

tagger = SuperTagger()

bert_name = 'camembert-base'

tagger.create_new_model(len(index_to_super), bert_name, index_to_super)
# You can load your model for re-train this
# tagger.load_weights("your/model/path")

tagger.train(texts, tags, checkpoint=True)

pred_without_argmax, pred_convert, bert_hidden_state = tagger.predict(texts[7])

In train, if you use checkpoint=True, the model is automatically saved in a folder: Training_XX-XX_XX-XX. It saves after each epoch. Use tensorboard=True for log in same folder. (tensorboard --logdir=logs for see logs)

bert_name can be any model available on Hugging Face

Training of linker

Launch train.py, if you look at it you can give another dataset file and another tagging model.

In train, if you use checkpoint=True, the model is automatically saved in a folder: Training_XX-XX_XX-XX. It saves after each epoch. Use tensorboard=True for log in same folder. (tensorboard --logdir=logs for see logs)

Predicting

Prediction of supertags

For predict on your data you need to load a model (save with this code).

df = read_csv_pgbar(file_path,20)
texts = df['X'].tolist()

tagger = SuperTagger()

tagger.load_weights("your/model/path")

pred_without_argmax, pred_convert, bert_hidden_state = tagger.predict(texts[7])

print(pred_convert)
#['let', 'dr(0,s,s)', 'let', 'dr(0,dr(0,s,s),np)', 'dr(0,np,n)', 'dr(0,n,n)', 'let', 'n', 'let', 'dl(0,n,n)', 'dr(0,dl(0,dl(0,n,n),dl(0,n,n)),dl(0,n,n))', 'dl(0,n,n)', 'let', 'dr(0,np,np)', 'np', 'dr(0,dl(0,np,np),np)', 'np', 'dr(0,dl(0,np,np),np)', 'np', 'dr(0,dl(0,np,s),dl(0,np,s))', 'dr(0,dl(0,np,s),np)', 'dl(1,s,s)', 'np', 'dr(0,dl(0,np,np),n)', 'n', 'dl(0,s,txt)']

Prediction of links

For predict on your data you need to load a model (save with this code).

linker = neuralproofnet.linker
links = linker.predict_without_categories("le chat est noir")
print(links)

The file postprocessing.py will allow you to draw the prediction with graphviz (you need to install it). Be careful to predict on limited sentence length otherwise the graph will not be helpful.

You can also use the function predict_without_categories which only needs the sentence (it uses the supertagger to predict the tags) or predict_with_categories so you can give directlythe categories (useful to check the links without bias from the supertager).

LICENSE

Copyright ou © ou Copr. CNRS, (18/07/2022)

Contributeurs : de Pourtales Caroline, Rabault Julien, Richard Moot

Ce logiciel est un programme informatique servant à établir un Proof Net depuis une phrase française.

Ce logiciel est régi par la licence CeCILL-C soumise au droit français et respectant les principes de diffusion des logiciels libres. Vous pouvez utiliser, modifier et/ou redistribuer ce programme sous les conditions de la licence CeCILL-C telle que diffusée par le CEA, le CNRS et l'INRIA sur le site "http://www.cecill.info".

En contrepartie de l'accessibilité au code source et des droits de copie, de modification et de redistribution accordés par cette licence, il n'est offert aux utilisateurs qu'une garantie limitée. Pour les mêmes raisons, seule une responsabilité restreinte pèse sur l'auteur du programme, le titulaire des droits patrimoniaux et les concédants successifs.

A cet égard l'attention de l'utilisateur est attirée sur les risques associés au chargement, à l'utilisation, à la modification et/ou au développement et à la reproduction du logiciel par l'utilisateur étant donné sa spécificité de logiciel libre, qui peut le rendre complexe à manipuler et qui le réserve donc à des développeurs et des professionnels avertis possédant des connaissances informatiques approfondies. Les utilisateurs sont donc invités à charger et tester l'adéquation du logiciel à leurs besoins dans des conditions permettant d'assurer la sécurité de leurs systèmes et ou de leurs données et, plus généralement, à l'utiliser et l'exploiter dans les mêmes conditions de sécurité.

Le fait que vous puissiez accéder à cet en-tête signifie que vous avez pris connaissance de la licence CeCILL-C, et que vous en avez accepté les termes.