Forge et recherche qui font leurs preuves
The old trick problem
Every serious software system has a few pieces of code that matter far more than their size suggests. A loop that runs millions of times. A bit operation in a compression path. A small matrix routine. A modular arithmetic kernel. The sort of thing that looks harmless in code review and then quietly decides the energy bill, the latency budget, or the number of machines you need to buy. Very democratic, software. One tiny function can ruin the meeting for everyone.
Historically, those kernels are improved by people. A senior engineer remembers a trick from a paper. Someone digs through an old forum post. A benchmark suite is written. A few candidates are tried. The fastest one wins if it still appears correct. Then the organization freezes it, because touching it again feels like poking a sleeping transformer with a fork.
Forge is research into a better version of that process. It is a program synthesis engine for small, critical implementations: give it a typed specificationand properties, let it search candidate programs, measure and compare tradeoffs, verify equivalence, then lower the discovered implementation to targets that matter. The important word is not search. The important word is still. It still has to be correct.
This is why Forge lives in research. It is not a public product button where someone types make faster and receives a miracle. It is a synthesis workbench for partner experiments, kernel discovery, and research on how far automated search can go when it is tied to verification instead of benchmark theatre.
A specification is the starting line
Optimization without a specification is just gambling with nicer variable names. The moment a clever candidate appears, the team needs to know what it is meant to preserve. Does it handle every input or only the friendly ones from the benchmark? Does itrespect overflow behaviour? Is the algebraic identity valid under the representation actually used? Does it keep the same semantics when lowered to a different backend?
Forge starts from typed expressions and properties because the search needs a boundary. The boundary says what counts as equivalent. Without it, the engine can find something astonishingly fast by deleting half the work. Computers are excellent at malicious compliance when the contract is vague.
The search side is deliberately plural. Enumerative search is useful when the space is small enough to cover. CEGIS is useful when counterexamples can guide refinement. Genetic programming and MCTS explore differently. ML-guided search can learn cost models and prioritize promising regions. None of these is universally best. That is not a weakness. It is how search behaves in the real world. If one hammer solved every kernel, toolboxes would be very boring and hardware vendors would be unemployed.
The research question is how to combine those engines with enough proof pressure that the result is not merely clever. A synthesized kernel has to survive both the happy-path benchmark and the unhappy-path verifier. Otherwise the improvement is not engineering. It is a magic trick with a maintenance cost.
The verifier is the adult in the room
Forge utilise une pile de vérification, car aucun contrôle unique ne suffit pour tous les domaines. Les exemples rapides sont peu coûteux et utiles. Les tests de propriétés détectent de larges catégories d'erreurs et réduisent les contre-exemples à quelque chose de lisible par un humain. Les solveurs SMT tels que Z3 et CVC5 peuvent prouver l'équivalence lorsque l'encodage est traitable. La vérification exhaustive est pratique pour les petits domaines. La saturation d'égalité par e-graphes offre une autre voie vers l'équivalence algébrique.
La pile est importante parce que les noyaux échouent de manière agaçante. Un candidat peut réussir tous les benchmarks ordinaires et être tout de même faux sur un cas limite. Il peut être correct pour des entrées non signées et faux pour des entrées signées. Il peut être correct dans un corps mathématique et faux après que la représentation choisie déborde. Il peut être correct avant l'abaissement et subtilement faux après une décision de sélection d'instructions. Le vérificateur existe parce que l'optimisme n'est pas une stratégie de test. Nous avons vérifié. À plusieurs reprises. Cela reste vrai.
Il y a aussi une raison pratique de conserver plusieurs voies de preuve. Les méthodes formelles sont puissantes, mais elles ne sont pas gratuites. Certains encodages expirent. Certains domaines sont trop vastes pour une vérification exhaustive. Certaines propriétés sont plus faciles à tester d'abord de manière probabiliste et à prouver ensuite. Forge traite la vérification comme un entonnoir, non comme un rituel de pureté. Les contrôles peu coûteux rejettent les absurdités évidentes. Les contrôles plus forts protègent le candidat final.
Rapide n'est pas un seul nombre
Le travail sur les performances devient absurde lorsqu'une seule métrique est autorisée à dominer chaque conversation. La latence compte. Le nombre d'opérations compte. L'utilisation de la mémoire compte. La pression sur les registres compte. Le temps de compilation compte parfois. La portabilité compte lorsque le même noyau doit vivre sur plus d'un backend. Un candidat qui gagne en latence en brûlant des registres comme un petit feu de joie peut être faux pour la cible réelle. Un candidat minuscule mais lent peut être utile ailleurs. Le contexte reste invaincu.
Forge cadre donc l'optimisation comme un problème de Pareto. Le moteur peut rechercher parmi plusieurs objectifs plutôt que de prétendre qu'il existe un score universel dicté par un tableur très confiant. La sortie utile n'est pas toujours le candidat le plus rapide. C'est parfois une famille de candidats avec des compromis visibles, afin qu'un ingénieur puisse choisir celui qui correspond à la contrainte de déploiement.
C'est aussi pourquoi je n'aime pas les affirmations nues d'accélération dans les articles de blog. La page de recherche peut décrire les attentes internes et les objectifs expérimentaux, mais les affirmations publiques nécessitent des exécutions récentes, du matériel actuel, des drapeaux de compilateur actuels et un contexte de charge de travail exact. Sinon, le nombre devient un souvenir. Les souvenirs sont agréables. Ils ne sont pas de l'architecture.
L'affirmation honnête est plus forte de toute façon : Forge consiste à rendre la recherche reproductible, comparable et vérifiable. Lorsqu'un candidat gagne, nous devrions savoir quel objectif il a remporté, quels candidats il a battus, quel vérificateur l'a accepté et quel backend il cible. C'est bien plus utile qu'un nombre flottant dans un deck de présentation en ayant l'air coûteux.
L'abaissement est là où les preuves vont être testées
Une implémentation découverte n'est utile que si elle survit au voyage jusqu'aux cibles réelles. La recherche Forge couvre l'abaissement vers des backends tels que x86-64, RISC-V, WASM, les chemins GPU Vulkan, C et Verilog. Cette liste de cibles n'est pas une décoration. Chaque backend a ses propres contraintes, formes d'instructions, comportements mémoire et modes de défaillance. La même spécification doit conserver son sens pendant que l'implémentation devient quelque chose que la cible peut réellement exécuter.
C'est ici que la synthèse se connecte au reste de la pile Dweve. Core veut des boucles internes efficaces. Numerus se soucie des noyaux numériques déterministes. BitWeave veut des opérations binaires sur vecteurs et matrices qui ne gaspillent pas le CPU. Kera se préoccupe d'abaisser les graphes de calcul vers du matériel réel. Forge ne peut alimenter ces couches que si l'implémentation générée est plus que rapide. Elle doit être équivalente, assez portable pour la cible choisie, et inspectable quand quelque chose change.
Ce que cela change pour les équipes
Pour une équipe, le changement intéressant n'est pas qu'une machine puisse découvrir un noyau plus rapide. C'est que le travail sur les noyaux dépend moins du folklore. Au lieu d'un expert qui se souvient de la bonne astuce, le processus devient : énoncer le contrat, explorer l'espace, mesurer les candidats, prouver l'équivalence, consigner le compromis, et générer le code cible. Les humains décident toujours. Ils arrêtent simplement de tout découvrir à la main.
Cela compte pour les opérations, car la dette de performance est coûteuse d'une manière que les organisations cachent souvent. Un noyau lent signifie plus de serveurs. Plus de serveurs signifie plus de coûts, plus d'énergie, plus de complexité de déploiement et plus de bruit dans la planification. Une optimisation erronée devient des incidents. Une astuce correcte mais non documentée devient un risque de migration futur. Forge est une recherche pour réduire ce tas d'absurdités évitables.
Il y a aussi un changement culturel. Le travail de performance manuel récompense souvent l'héroïsme. Quelqu'un disparaît dans la caverne et revient avec une astuce astucieuse. Tout le monde applaudit, personne ne comprend vraiment, et l'entreprise a acquis un petit objet sacré. Forge pousse le processus vers les preuves : voici la spécification, voici la route de recherche, voici les candidats rejetés, voici le vérificateur, voici le backend sélectionné. Moins de mythologie. Plus de reçus.
Où le travail reste difficile
Rien de tout cela ne rend la synthèse facile. Les spécifications sont difficiles. Si la spécification est fausse, le moteur peut découvrir fidèlement la mauvaise chose. Les espaces de recherche peuvent exploser. Les solveurs peuvent expirer. Les modèles de coût peuvent induire en erreur. Les backends peuvent exposer des détails que l'expression abstraite ignorait. La vérification peut être forte dans un domaine et maladroite dans un autre. Quiconque vend la synthèse de programmes comme un distributeur automatique de code optimal saute soit les parties difficiles, soit facture un supplément pour la déception.
Forge est intéressant précisément parce qu'il fait face directement à ces parties difficiles. Il combine plusieurs stratégies de recherche. Il garde la vérification proche. Il traite les objectifs comme des compromis. Il cible de vrais backends. Il reste un programme de recherche parce que nous apprenons encore où se situe la frontière entre la découverte automatisée, le jugement humain, les limites des solveurs et la réalité du déploiement.
Cette frontière vaut la peine d'être explorée. L'industrie du logiciel a trop de petites boucles chaudes, trop de folklore de performance dupliqué, et trop d'optimisations que personne ne veut retoucher. Si Forge peut transformer ne serait-ce qu'une partie de ce travail en un processus de preuve reproductible, le résultat n'est pas seulement du code plus rapide. C'est du code plus calme. Le code plus calme est sous-estimé, surtout par ceux qui n'ont pas été réveillés à 02:17.
Ce qu’exige un bon passage sur Forge
Une expérience sérieuse avec Forge commence avant que le moteur ne s’exécute. L’équipe doit apporter un vrai noyau, pas une vague plainte sur les performances. Il faut des entrées représentatives, des cas limites connus, le matériel cible, des benchmarks actuels et la raison métier pour laquelle ce noyau compte. Sinon, le moteur de synthèse peut passer beaucoup de temps à résoudre un problème que personne n’a réellement. Les outils de recherche ne sont pas à l’abri des entrées médiocres. Ils rendent simplement l’inspection de ces déchets plus coûteuse.
L’entrée la plus utile est un contrat petit et précis. Que doit calculer la fonction ? Quelles lois algébriques importent ? Quel comportement de débordement est intentionnel ? Quelles plages sont impossibles par construction, et lesquelles ne se sont simplement pas produites lors du dernier test ? Quelles sorties tolèrent une approximation, et lesquelles non ? Une équipe qui ne peut pas répondre à ces questions n’a probablement pas encore un problème d’optimisation. Elle a un problème de clarification produit déguisé en problème de compilateur.
Un bon passage exige aussi une posture cible. x86-64 et RISC-V ne sont pas identiques. WASM a des contraintes différentes. Les chemins GPU Vulkan se soucient des formes et des mouvements de mémoire. Verilog soulève des questions matérielles que les équipes applicatives normales n’aiment rarement aborder avant le café. Forge peut explorer l’abaissement vers la cible, mais il ne peut pas décider des priorités organisationnelles. Si la portabilité compte plus que la vitesse sur une seule cible, dites-le. Si la latence prime sur la mémoire, dites-le. Si la pression sur les registres est la limite pratique, dites-le aussi. Le moteur est puissant, pas télépathe.
La sortie doit être traitée comme un dossier de preuves. Candidat, objectif, voie de preuve, contre-exemples rejetés, backend, contexte de benchmark et réserves ouvertes. Ce dossier est ce qui permet aux humains de prendre une décision sensée. Parfois, la meilleure décision est d’adopter le candidat. Parfois, c’est de garder l’ancien noyau parce que le compromis de portabilité n’en vaut pas la peine. Parfois, la découverte est que la spécification était trop lâche. Ces trois résultats sont utiles. Un seul d’entre eux semble impressionnant dans une démo, ce qui explique pourquoi les démos remplacent mal l’ingénierie.
La leçon
La leçon de Forge est simple : la performance ne doit pas dépasser la preuve. La recherche est puissante, mais un moteur de recherche sans vérification n’est qu’une manière très énergique de créer des bogues. La vérification est puissante, mais sans recherche, elle attend que les humains lui apportent des candidats. Forge réunit les deux et demande quels noyaux nous pouvons découvrir lorsque la machine est autorisée à explorer, mais pas autorisée à mentir.
C’est la recherche qui vaut la peine. Spécifications typées, recherche de candidats, entonnoirs de preuve, objectifs de Pareto et abaissement vers le backend. Pas de magie. Pas de raccourci produit. Une manière de produire un meilleur petit code avec des preuves à l’appui.