(le « très bien connus » pourrait être discuté, mais ça interroge quand-même)

(Si je puis me permettre, on ne sait pas très bien non plus pourquoi ~10^11 neurones biologiques connectés par ~10^15 synapses donnent une forme d'« intelligence » alors que les composants basiques sont très bien connus et bien modélisés individuellement depuis longtemps (cf Hodgkin-Huxley, etc.).)

(On imagine mal cet adage par exemple pour la vérification de logiciels embarqués en avionique ?)

Au passage, je me demande comment le domaine des méthodes formelles peut aller de pair avec le "Fake it till you make it" qui est parfois prôné dans l’entreprenariat "tech".

Oui oui, mais au-delà de l'IA (même si c'est lié), j'ai le sentiment qu'il y a une différence d'approche, car certains se veulent plus "business-oriented" que d'autres, et cela se ressent dans la communication.

N'est-ce pas surtout une conséquence de l'importance qu'a pris la communication autour de l'IA ces derniers temps et le positionnement de la FRO sur ce sujet ? (qui déteint avec une certaine forme de « sobriété » plus commune dans les milieux académiques)

Photographie de la couverture du livre https://press.princeton.edu/books/paperback/9780691281384/the-brain-in-theory

Prochaine lecture de vacances (par @romainbrette.bsky.social)

C'est-à-dire ?

Je ne m'y connais pas encore assez pour évaluer la part d'objectivité (e.g. on m'a mentionné la gestion de l'élimination sur les types inductifs, plus propre dans Lean) vs marketing dans ces affirmations.

Lean4Lean: Verifying a Typechecker for Lean, in Lean In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ ...

BTW, cela ne semble pas dater d'hier les références (négatives) à Rocq de la part des gens de Lean :

> This was in particular in formed by periodic news of unsoundnesses in Rocq due to complications of the many interacting features in the kernel.
arxiv.org/abs/2403.14064

Inconsistency due to uniform parameters in the guard condition · Issue #21797 · rocq-prover/rocq Description of the problem This issue was found using Claude and a little bit of guidance towards the suspect bits, but I had to write a test that wouldn't make the kernel loop myself. Small Rocq /...

J'imagine que @monniauxd.bsky.social fait référence à github.com/rocq-prover/...

Je me demande d'ailleurs si les sujets type IMO peuvent vraiment échapper aux GAFAM avant leur publication, et ce que ça signifie par rapport au fait qu'ils servent de benchmark pour les IA.

Trouvé la réponse ! (en passant au Marché du livre ancien et d'occasion, Paris 15ème)

Le chapitre 7 du livre *Deep Learning in Science* de Pierre Baldi discute de cette question, à mon sens trop peu abordée dans les débats intelligence naturelle vs artificielle.

www.igb.uci.edu/~pfbaldi/boo...

Le chapitre 7 du livre *Deep Learning in Science* de Pierre Baldi discute de cette question, à mon sens trop peu abordée dans les débats intelligence naturelle vs artificielle.

www.igb.uci.edu/~pfbaldi/boo...

Now that makes me curious... is there a path from type theory to your question or is it unrelated?

Est-ce une différence fondamentale (homme / machine) que la "backward propagation", contrairement à l'apprentissage Hebbien, ne respecte pas le principe de localité ?

Model Context Protocol - Wikipedia Earlier stop-gap approaches—such as OpenAI's 2023 "function-calling" API and the ChatGPT plug-in framework—solved similar problems but required vendor-specific connectors.[7] MCP re-uses the message-flow ideas of the Language Server Protocol (LSP) and is transported over JSON-RPC 2.0.[8]

Anthropic a standardisé un protocole (MCP, cf en.wikipedia.org/wiki/Model_C...) pour intégrer des outils appelables par un LLM "augmenté".

D'ailleurs, on parle beaucoup moins des modèles d'embeddings, mais il y en a plein, cf par exemple developers.openai.com/api/docs/gui...

Voir le schéma en.wikipedia.org/wiki/Retriev...

La notion d'"embedding" est importante aussi, en gros c'est ce qui permet d'encoder un bout de phrase dans une vecteur puis de faire des recherches par proximité sémantique.

J'en parlais il y a quelques temps, en gros tu fais exécuter des recherches par ton LLM, la recherche retourne { "clef1" -> "... extrait 1 ..." } puis il insère des balises <clef1> là où le passage doit être cité, c'est très classique.

bsky.app/profile/lips...

Cela marche aussi pour « L'IA invente des passages (de textes de loi, de roman, etc.) » dans une certaine mesure.

Quelles seraient, selon toi, les raisons principales expliquant ces écarts entre modèles théoriques et implémentations ?

Il y a aussi ceci semble-t-il :
bsky.app/profile/jean...

J'ai l'impression qu'il y a tellement de connaissances tribales dans ce petit monde...

BTW, j'ai commencé par Lean et j'envisage maintenant d'apprendre Coq : la littérature sur les aspects méta-théoriques etc. est tellement plus vaste.

Je serais intéressé d'ailleurs par un récapitulatif des principales différences entre les deux.

Oui voilà, avec le même ratio notes de bas de page / contenu que dans le poly :-p

(Personnellement, je trouve aussi le cours intéressant, c'est comme ça que j'ai appris ce que sont les nombres p-adiques. Pour l'aspect pédagogie à l'X en revanche on pourrait en discuter...)

Oui tout à fait, j'en ai encore le poly d'origine quelque part.

Ce cours avait rencontré un succès pour le moins mitigé, et ça s'est terminé par le départ du professeur en question de l'X (avec un long PDF d'explications qu'on doit encore pouvoir trouver sur les internets).

Je n'ai pas le contexte de votre message, mais je crois connaître le contexte de l'écriture de ce livre et je trouve amusant qu'on y trouve ce genre de choses.