Guide avancé de Rethlas : comment exécuter Rethlas manuellement

Ce guide plus avancé sur Rethlas s'adresse aux mathématiciens ayant des connaissances minimales en informatique. Je vais présenter Rethlas plus en détail et expliquer comment je l'utiliserais.

Prérequis

1. Connaître les bases de l'utilisation d'un terminal. Consultez mon guide du terminal.
2. Avoir terminé la configuration de base de Rethlas. Consultez mon article précédent, Guide de Rethlas : comment exécuter Rethlas avec l'aide de l'IA (aucune connaissance en informatique requise).

Vue d'ensemble du dépôt Rethlas

├── agents
│   ├── generation
│   │   ├── AGENTS.md
│   │   ├── data
│   │   ├── downloads
│   │   ├── logs
│   │   ├── mcp
│   │   ├── memory
│   │   ├── results
│   │   ├── scripts
│   │   ├── site
│   │   └── tests
│   └── verification
│       ├── AGENTS.md
│       ├── api
│       ├── mcp
│       ├── memory
│       ├── requirements.txt
│       ├── results
│       ├── schemas
│       └── scripts

Rethlas comporte deux agents : un agent de génération et un agent de vérification. La philosophie de base est très simple : si l'agent de vérification peut rejeter de manière fiable les preuves erronées et si l'agent de génération est suffisamment puissant pour explorer l'espace des solutions à la recherche de preuves candidates, alors, en répétant la boucle de génération–vérification, l'agent de génération finira par trouver une preuve en comblant de petites lacunes et en évitant de répéter ses erreurs.

Vous pouvez consulter le code de l'une des deux manières suivantes :

1. Pour les adeptes des interfaces graphiques : ouvrez les dossiers et cliquez sur les fichiers ou sous-dossiers qui vous intéressent.
2. Pour les adeptes du terminal : utilisez cd pour vous déplacer dans les répertoires, ls pour afficher les fichiers visibles, ls -alh pour inclure les fichiers masqués, et less <filename> pour parcourir le contenu d'un fichier page par page.

Si vous vous intéressez uniquement à l'utilisation de Rethlas, il vous suffit de connaître les éléments suivants :

1. agents/generation/data est le dossier dans lequel vous placez vos problèmes et vos références.
2. agents/generation/results est le dossier dans lequel vous consultez les solutions produites (des fichiers Markdown).
3. agents/generation/logs est le dossier dans lequel vous pouvez consulter les journaux de Rethlas et étudier ses trajectoires d'exploration. Ces journaux peuvent toutefois être trop longs pour être lus en entier.
4. agents/generation/memory vous aide également à comprendre les points clés des trajectoires de raisonnement, notamment les décisions majeures, les états des branches, les contre-exemples, les événements, les voies infructueuses, les conclusions immédiates, les étapes de preuve, les sous-objectifs, les exemples-jouets et les rapports de vérification.

Je vais présenter ces éléments plus en détail. Je prendrai comme exemple la conjecture selon laquelle les polynômes de Kazhdan–Lusztig des matroïdes n'ont que des racines réelles.

Problèmes et références

Rédiger un énoncé et fournir les références

Puisqu'il est généralement plus pratique de tout faire dans un terminal, je vais d'abord présenter cette méthode canonique. Pour les personnes qui n'aiment vraiment pas le terminal, je montrerai comment procéder avec une interface graphique (GUI).

Commencez par utiliser cd pour entrer dans le dossier rethlas.

cd ~/Desktop
git clone https://github.com/frenzymath/Rethlas.git rethlas
cd rethlas

Créez ensuite un nouveau dossier de projet pour votre problème :

cd agents/generation/data
mkdir real_root_kl
cd real_root_kl

Voici maintenant l'essentiel :

• touch real_root_kl.md. Cette commande crée un fichier Markdown dans lequel vous pouvez écrire votre problème.
• mkdir real_root_kl.refs. Cette commande crée un dossier dans lequel vous pouvez placer des références.

Le nom que vous donnez au problème n'a pas d'importance. Il est toutefois important que les noms de base de x.md et de x.refs soient identiques.

Utilisez maintenant votre éditeur préféré pour modifier le fichier Markdown et énoncer votre problème de manière claire et rigoureuse (sinon, les agents risquent de vous donner des exemples triviaux !). Comme expliqué dans le guide du terminal, vous pouvez utiliser open -e <filename.md> sous macOS pour ouvrir le fichier dans TextEdit. Si vous avez installé Visual Studio Code — avec Homebrew ou depuis un navigateur — et rendu sa commande code accessible depuis le terminal, vous pouvez utiliser code <filename> pour modifier le fichier avec VS Code. Vous pouvez également utiliser vim <filename>.

Conseils sur les énoncés de problèmes et les références

Comme vous le savez, l'IA générative est essentiellement un système de prédiction du prochain jeton ; le prompt et le contexte comptent donc beaucoup. Voici quelques conseils sur lesquels je souhaite insister :

1. Assurez-vous que l'énoncé de votre problème est rigoureux et contient toutes les conditions nécessaires ; sinon, les agents risquent de vous donner des exemples triviaux. Évitez les ambiguïtés et les abus de notation. Faites en sorte que tout soit parfaitement explicite.
2. Pour fournir des références, placez simplement les fichiers dans real_root_kl.refs. Je recommande vivement d'utiliser Markdown, LaTeX ou du texte brut. Pour les articles disponibles sur arXiv, vous pouvez télécharger le code source LaTeX. Pour les PDF, vous pouvez utiliser la reconnaissance optique de caractères (OCR) ou un autre outil d'IA — par exemple, l'interface web de ChatGPT — afin de les convertir en Markdown.
3. Vous n'avez pas besoin de fournir toutes les références disponibles sur arXiv, car les agents peuvent utiliser des outils de recherche pour les trouver eux-mêmes. Il peut toutefois être très utile de fournir des livres protégés par le droit d'auteur que vous jugez pertinents.
4. Les références détourneront l'attention des agents si elles ne sont pas utiles. Ne fournissez donc que les références nécessaires que vous jugez étroitement liées au problème, ou des documents protégés par le droit d'auteur qu'il est difficile de télécharger librement sur Internet.
5. Dans l'énoncé du problème, vous pouvez fournir les définitions nécessaires à sa compréhension. Cela est particulièrement utile lorsque les termes employés ont d'autres sens dans d'autres domaines.

Voici quelques astuces plus avancées :

Dans le guide du terminal, j'ai montré comment utiliser Git avec Overleaf. Vous pouvez donc cloner votre projet d'article sur Overleaf dans ce dossier de références. Si vous répartissez clairement les sections de votre article dans différents fichiers .tex et utilisez \input dans main.tex, vous pouvez ainsi fournir aux agents le contexte de votre travail en cours ou de vos notes personnelles.

Si le problème fait appel à des définitions tirées de votre article, je vous recommande de répéter ces définitions dans l'énoncé du problème et d'ajouter une indication telle que as defined in 1introduction.tex in refs. Voici un modèle de prompt :

A monodromic crystalline D-module is defined to be ..., as in
3monodromic.tex. Prove ..., i.e., the unproved lemma lem:unproved in
3monodromic.tex.

Ensuite, après avoir révisé le résultat, si vous le jugez correct, vous pouvez rédiger vous-même la preuve dans votre article à partir de ce que vous avez compris, ou demander à Codex ou à Claude de l'intégrer à votre article. Veillez à vérifier soigneusement que le résultat est correct et à le réécrire avec soin. Vous pouvez utiliser git add, git commit et git push pour mettre votre projet Overleaf à jour. Vous pouvez également utiliser git restore . pour abandonner les modifications apportées aux fichiers suivis qui n'ont pas encore été ajoutées à la zone de préparation.

Exécuter Rethlas

Maintenant que vous avez énoncé le problème et fourni les références, lançons Rethlas. Bien entendu, vous pouvez toujours utiliser une IA pour vous aider à le lancer et à l'exécuter, comme expliqué dans le guide de Rethlas. Je souhaite ici montrer comment piloter les expériences manuellement.

Utilisez de nouveau cd pour entrer dans le répertoire rethlas, puis poursuivez depuis ce répertoire : cd ~/rethlas ou cd ~/Desktop/rethlas, selon l'emplacement du dossier Rethlas.

Utilisez ensuite tmux pour gérer plusieurs fenêtres de terminal au sein d'une même session. Pour en savoir plus sur tmux et ses avantages, consultez le guide du terminal.

tmux

Nous allons maintenant réserver une fenêtre à l'agent de génération et une autre au service de vérification.

Configurer le service de vérification

Appuyez sur ctrl+b, relâchez les deux touches, puis appuyez sur , pour renommer la fenêtre actuelle. Saisissez verify, puis appuyez sur enter.

Exécutez ensuite :

cd agents/verification

Si vous avez déjà configuré l'environnement virtuel comme expliqué dans le guide de Rethlas, exécutez simplement :

source .venv/bin/activate

Sinon, exécutez :

uv venv
source .venv/bin/activate
uv pip install -r requirements.txt

Exécutez ensuite :

uvicorn api.server:app --host 0.0.0.0 --port 8091

Vous devriez voir ceci :

Passons maintenant au lancement de l'agent de génération.

Configurer l'agent de génération

Commencez par appuyer sur ctrl+b, relâchez les deux touches, puis appuyez sur c pour créer une nouvelle fenêtre. Utilisez de nouveau ctrl+b, puis ,, pour renommer cette fenêtre gen1.

Assurez-vous de vous trouver dans le répertoire Rethlas, puis exécutez :

cd agents/generation

Si la nouvelle fenêtre tmux a plutôt hérité du répertoire agents/verification, exécutez cd ../generation.

Si vous avez déjà configuré l'environnement virtuel de l'agent de génération, exécutez :

source .venv/bin/activate

Sinon, exécutez :

uv venv
source .venv/bin/activate
uv pip install -r mcp/requirements.txt

Exécutez maintenant :

MODEL=gpt-5.6-sol REASONING_EFFORT=max PROBLEM_FILE=data/real_root_kl/real_root_kl.md ./tests/run_example.sh

Vous verrez alors ceci :

Le chronomètre indiquera depuis combien de temps l'expérience s'exécute.

Il ne vous reste plus qu'à laisser l'expérience tourner pendant des heures et, avec un peu de chance, à en récolter le résultat. Vous pouvez l'arrêter en appuyant sur ctrl+c.

Consulter le résultat dans un navigateur

Une fois l'expérience terminée, vous pouvez consulter le résultat en exécutant la commande suivante :

./site/serve.sh

Exécutez cette commande depuis le répertoire agents/generation.

Ouvrez ensuite http://localhost:3264 dans votre navigateur pour consulter les résultats. Si certaines formules présentent des erreurs de mise en forme, vous pouvez bien entendu demander à Codex de les corriger.

Exécutions en parallèle

Vous pouvez exécuter plusieurs agents de génération afin de vous attaquer à plusieurs problèmes en parallèle, à condition de disposer d'un quota d'utilisation de GPT suffisant.

1. Utilisez ctrl+b, puis c, pour ouvrir une nouvelle fenêtre. Utilisez ctrl+b, puis ,, pour la renommer gen2.
2. Utilisez cd pour entrer dans agents/generation.
3. Exécutez MODEL=gpt-5.6-sol REASONING_EFFORT=max PROBLEM_FILE=data/real_root_z/real_root_z.md ./tests/run_example.sh.

Vous pouvez utiliser ctrl+b, puis w, pour choisir la fenêtre que vous souhaitez afficher. Vous pouvez vérifier de temps en temps que le service de vérification fonctionne correctement.

Analyser la trajectoire d'exploration

Si vous souhaitez comprendre pourquoi Rethlas réussit ou échoue sur un problème donné, vous devez examiner les journaux et les fichiers de mémoire. Les fichiers de mémoire sont généralement courts et instructifs. Les journaux sont habituellement très longs et verbeux, mais contiennent davantage d'informations utiles au débogage et à la compréhension des échecs.

En examinant les journaux, j'ai découvert les éléments suivants :

1. Rethlas a commis une erreur de substitution de référence bibliographique dans le problème de Brian Conrad sur les groupes algébriques [1, Section 5.1.1] en raison d'un problème de droit d'auteur : l'ouvrage CGP [3] n'était pas accessible à Codex, et le modèle refusait de reproduire le contenu de ce livre protégé par le droit d'auteur.
2. J'ai également reconstitué la trajectoire de raisonnement de Rethlas dans l'article sur les polynômes de Kazhdan–Lusztig [2].

Bien entendu, vous pouvez utiliser Codex ou Claude pour vous aider à comprendre les journaux, mais vous ne pouvez pas trop compter sur leur aide, car les journaux sont très longs et les agents risquent de passer à côté de certains éléments.

Références

[1] Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai et Bin Dong. Automated Conjecture Resolution with Formal Verification. arXiv:2604.03789.

[2] Ronnie Cheng et Shurui Liu. Kazhdan–Lusztig Polynomials of Matroids Need Not Be Unimodal. arXiv:2607.24186.

[3] Brian Conrad, Ofer Gabber et Gopal Prasad. Pseudo-reductive Groups. 2e éd., New Mathematical Monographs 26, Cambridge University Press, 2015. DOI: 10.1017/CBO9781316092439.