Fil de Ben Goertzel (@bengoertzel)

À propos de l'utilisation des LLM pour aider à démontrer des problèmes mathématiques difficiles (existence et unicité dreddit.com/r/singularity/… etc.) En lisant ceci https://t.co/tOvR1LbfZ6 Le fait que certains membres de DeepMind utilisent l'IA pour aider à prouver le théorème d'existence et d'unicité de Navier-Stokes me motive à souligner qu'il y a quelques mois, j'ai tenté de prouver ce théorème avec l'aide de quelques étudiants en droit (LLM) pour certains détails. https://t.co/uPCZ9GRnz5 L'idée de la démonstration était de moi : utiliser la correspondance entre l'équation HJB (que j'ai beaucoup utilisée dans mes travaux récents en IA) et l'équation de Navier-Stokes, afin d'appliquer les résultats d'existence et d'unicité de HJB à NS. Cependant, les détails sont assez complexes et je n'avais pas le temps de les approfondir moi-même ; les masters en droit m'ont été d'une grande aide. Cela dit, ce sont des questions épineuses et je ne peux pas affirmer avec certitude qu'il n'y ait aucune lacune… J'avais mis ce projet de côté car travailler sur l'AGI me semblait plus prioritaire. J'ai envisagé d'en faire une solution Lean complète, mais je n'ai pas encore eu le temps de m'en occuper. À peu près à la même époque, j'ai également bénéficié de l'aide de quelques étudiants en droit (LLM) pour préciser les détails d'une idée que j'avais sur la façon de prouver P/=NP en utilisant une variante de la faiblesse quantale (un outil conceptuel/mathématique que j'ai développé dans le cadre de mon travail sur l'AGI, généralisant la notion de faiblesse de Michael Timothy Bennett comme alternative au rasoir d'Occam traditionnel). https://t.co/vKP3grPtbV Travailler à l'avènement de l'AGI est une tâche chronophage et je n'ai pas eu le temps de la formaliser entièrement (même si les LLM y contribuent évidemment...). De plus, comme pour toute preuve aussi complexe, il pourrait y avoir une lacune qui m'échappe... Je n'ai pas fait de bruit autour de ces efforts car je voulais attendre de tout formaliser et de vérifier les choses, mais maintenant que d'autres en parlent, je me dis : bon, pourquoi pas… L'un de mes objectifs en travaillant sur ces problèmes mathématiques complexes [mon doctorat était en mathématiques, même si je me suis rapidement orienté vers l'IA] était de réfléchir à la manière d'utiliser efficacement notre système proto-AGI Hyperon comme « contrôleur » pour les LLM dans ce type de travail. Autrement dit, dans ce type de travail, un esprit créatif et ouvert est nécessaire pour concevoir des idées de démonstration, un LLM pour en travailler les détails, et enfin Lean ou un autre cadre ITP pour effectuer une vérification formelle complète. Le rôle que j'espère qu'Hyperon pourra jouer ici est celui de « l'esprit créatif et ouvert »… Mais dans les tentatives de démonstration que je viens de publier, c'est moi, et non Hyperon, qui ai essayé de jouer ce rôle ;)