Kucie i wyszukiwanie, które zasługują na dowód
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 używa stosu weryfikacji, ponieważ żadna pojedyncza kontrola nie wystarcza dla każdej dziedziny. Szybkie przykłady są tanie i przydatne. Testy właściwości wykrywają szerokie klasy błędów i redukują kontrprzykłady do czegoś, co człowiek może przeczytać. Solwery SMT, takie jak Z3 i CVC5, potrafią dowodzić równoważności tam, gdzie kodowanie jest wykonalne. Wyczerpujące sprawdzanie jest praktyczne dla małych dziedzin. Nasycenie równościowe grafów e-grafów daje kolejną drogę przez równoważność algebraiczną.
Stos ma znaczenie, ponieważ jądra zawodzą w irytujący sposób. Kandydat może przejść wszystkie zwykłe benchmarki i nadal być błędny w przypadku brzegowym. Może być poprawny dla danych bez znaku i błędny dla danych ze znakiem. Może być poprawny w ciele matematycznym i błędny po przepełnieniu wybranej reprezentacji. Może być poprawny przed obniżeniem i subtelnie błędny po decyzji o wyborze instrukcji. Weryfikator istnieje, ponieważ optymizm nie jest strategią testowania. Sprawdziliśmy. Wielokrotnie. To nadal pozostaje prawdą.
Istnieje też praktyczny powód, aby utrzymywać kilka ścieżek dowodzenia. Metody formalne są potężne, ale nie są darmowe. Niektóre kodowania przekraczają limit czasu. Niektóre dziedziny są zbyt duże na wyczerpujące sprawdzanie. Niektóre właściwości łatwiej najpierw przetestować probabilistycznie, a potem udowodnić. Forge traktuje weryfikację jak lejek, a nie rytuał czystości. Tanie kontrole odrzucają oczywiste bzdury. Silniejsze kontrole chronią finalnego kandydata.
Szybkość to nie jedna liczba
Praca nad wydajnością staje się śmieszna, gdy jedna metryka może zdominować każdą rozmowę. Opóźnienie ma znaczenie. Liczba operacji ma znaczenie. Zużycie pamięci ma znaczenie. Presja rejestrów ma znaczenie. Czas kompilacji czasem ma znaczenie. Przenośność ma znaczenie, gdy to samo jądro ma działać na więcej niż jednym backendzie. Kandydat, który wygrywa na opóźnieniu, spalając rejestry jak małe ognisko, może być błędny dla rzeczywistego celu. Kandydat, który jest mały, ale wolny, może być przydatny gdzie indziej. Kontekst pozostaje niepokonany.
Forge dlatego ujmuje optymalizację jako problem Pareto. Silnik może przeszukiwać cele zamiast udawać, że istnieje jeden uniwersalny wynik przekazany przez bardzo pewny siebie arkusz kalkulacyjny. Przydatnym wynikiem nie zawsze jest pojedynczy najszybszy kandydat. Czasem jest to rodzina kandydatów z widocznymi kompromisami, aby inżynier mógł wybrać ten, który pasuje do ograniczeń wdrożenia.
To także powód, dla którego nie lubię nagich twierdzeń o przyspieszeniu w wpisach na blogu. Strona badawcza może opisywać wewnętrzne oczekiwania i cele eksperymentalne, ale publiczne twierdzenia wymagają świeżych przebiegów, aktualnego sprzętu, aktualnych flag kompilatora i dokładnego kontekstu obciążenia. W przeciwnym razie liczba staje się pamiątką. Pamiątki są miłe. Nie są architekturą.
Uczciwe twierdzenie jest zresztą silniejsze: Forge polega na tym, aby wyszukiwanie było powtarzalne, porównywalne i sprawdzalne. Gdy kandydat wygrywa, powinniśmy wiedzieć, który cel wygrał, których kandydatów pokonał, który weryfikator go zaakceptował i na który backend jest kierowany. To znacznie bardziej przydatne niż liczba pływająca po slajdach i wyglądająca na kosztowną.
Obniżanie to miejsce, gdzie dowody są testowane
Odkryta implementacja jest użyteczna tylko wtedy, gdy przetrwa podróż do rzeczywistych celów. Badania Forge obejmują obniżanie do backendów takich jak x86-64, RISC-V, WASM, ścieżki GPU Vulkan, C i Verilog. Ta lista celów nie jest ozdobnikiem. Każdy backend ma własne ograniczenia, kształty instrukcji, zachowanie pamięci i tryby awarii. Ta sama specyfikacja musi zachować swoje znaczenie, podczas gdy implementacja staje się czymś, co cel może faktycznie uruchomić.
W tym miejscu synteza łączy się z resztą stosu Dweve. Core chce wydajnych pętli wewnętrznych. Numerus dba o deterministyczne jądra numeryczne. BitWeave chce operacji na wektorach i macierzach binarnych, które nie marnują mocy CPU. Kera zajmuje się obniżaniem grafów obliczeniowych do rzeczywistego sprzętu. Forge może zasilać te warstwy tylko wtedy, gdy wygenerowana implementacja jest czymś więcej niż szybka. Musi być równoważna, wystarczająco przenośna dla wybranego celu i możliwa do sprawdzenia, gdy coś się zmieni.
Co to zmienia dla zespołów
Dla zespołu interesująca zmiana nie polega na tym, że maszyna może odkryć szybsze jądro. Chodzi o to, że praca nad jądrami staje się mniej zależna od folkloru. Zamiast jednego eksperta pamiętającego właściwą sztuczkę, proces wygląda tak: określ kontrakt, przeszukaj przestrzeń, zmierz kandydatów, udowodnij równoważność, zapisz kompromis i wygeneruj kod docelowy. Ludzie nadal podejmują decyzje. Po prostu przestają robić całe odkrywanie ręcznie.
To ma znaczenie dla operacji, ponieważ dług wydajnościowy jest kosztowny w sposób, który organizacje często ukrywają. Wolne jądro oznacza więcej serwerów. Więcej serwerów oznacza więcej kosztów, więcej energii, większą złożoność wdrożenia i więcej szumu w planowaniu. Błędna optymalizacja oznacza incydenty. Poprawna, ale nieudokumentowana sztuczka staje się przyszłym ryzykiem migracji. Forge to badania nad zmniejszeniem tej sterty możliwych do uniknięcia bzdur.
Jest też zmiana kulturowa. Ręczna praca nad wydajnością często nagradza bohaterstwo. Ktoś znika w jaskini i wraca ze sprytnym hackiem. Wszyscy biją brawo, nikt w pełni tego nie rozumie, a firma nabywa mały święty przedmiot. Forge przesuwa proces w stronę dowodów: oto specyfikacja, oto trasa poszukiwań, oto odrzuceni kandydaci, oto weryfikator, oto wybrany backend. Mniej mitologii. Więcej paragonów.
Gdzie praca wciąż jest trudna
Nic z tego nie czyni syntezy łatwą. Specyfikacje są trudne. Jeśli specyfikacja jest błędna, silnik może wiernie odkryć coś złego. Przestrzenie poszukiwań mogą eksplodować. Solvery mogą przekraczać limit czasu. Modele kosztów mogą mylić. Backendy mogą ujawniać szczegóły, które abstrakcyjne wyrażenie ignorowało. Weryfikacja może być silna w jednej dziedzinie, a niezręczna w innej. Każdy, kto sprzedaje syntezę programów jako automat z optymalnym kodem, albo pomija trudne części, albo pobiera dodatkową opłatę za rozczarowanie.
Forge jest interesujący właśnie dlatego, że mierzy się z tymi trudnymi częściami bezpośrednio. Łączy kilka strategii poszukiwań. Trzyma weryfikację blisko. Traktuje cele jako kompromisy. Celuje w prawdziwe backendy. Pozostaje programem badawczym, ponieważ wciąż uczymy się, gdzie przebiega granica między automatycznym odkrywaniem, ludzkim osądem, ograniczeniami solverów a rzeczywistością wdrożeń.
Tę granicę warto badać. Przemysł oprogramowania ma zbyt wiele małych gorących pętli, zbyt wiele powielonego folkloru wydajnościowego i zbyt wiele optymalizacji, których nikt nie chce ponownie dotykać. Jeśli Forge uda się zamienić choć część tej pracy w powtarzalny proces oparty na dowodach, wynikiem nie będzie tylko szybszy kod. To będzie spokojniejszy kod. Spokojniejszy kod jest niedoceniany, głównie przez ludzi, którzy nie byli wzywani o 02:17.
What a good Forge run needs
A serious Forge experiment starts before the engine runs. The team has to bring a real kernel, not a vague complaint about performance. It needs representative inputs, known edge cases, target hardware, current benchmarks, and the business reason this kernel matters. Otherwise the synthesis engine can spend a lot of time solving a problem nobody actually has. Research tools are not immune to garbage input. They merely make the garbage more expensive to inspect.
The most useful input is a small, sharp contract. What is the function supposed to compute? Which algebraic laws matter? Which overflow behaviour is intentional? Which ranges are impossible by construction, and which merely did not happen in the last test run? Which outputs can tolerate approximation, and which cannot? A team that cannot answer those questions probably does not have an optimization problem yet. It has a product clarification problem wearing a compiler hat.
A good run also needs a target posture. x86-64 and RISC-V are not the same. WASM has different constraints. Vulkan GPU paths care about shapes and memory movement. Verilog raises hardware questions that normal application teams rarely enjoy before coffee.Forge can explore target lowering, but it cannot decide organizational priorities. If portability matters more than one-target speed, say that. If latency beats memory, say that. If register pressure is the practical limit, say that too. The engine is powerful,not psychic.
The output should be treated like an evidence package. Candidate, objective, proof route, counterexamples rejected, backend, benchmark context, and open caveats. That package is what lets humans make a sane decision. Sometimes the winning move is to adopt the candidate. Sometimes it is to keep the old kernel because the portability tradeoff is not worth it. Sometimes the discovery is that the spec was too loose. All three outcomes are useful. Only one of them looks exciting in a demo, which is why demos are a poor substitute for engineering.
The lesson
The lesson of Forge is simple: performance should not outrun proof. Search is powerful, but a search engine without verification is just a very energetic way to create bugs. Verification is powerful, but without search it waits for humans to bring it candidates. Forge puts the two together and asks what kernels we can discover when the machine is allowed to explore, but not allowed to lie.
That is the research worth doing. Typed specs, candidatesearch, proof funnels, Pareto objectives, and backend lowering. Not magic. Not a product shortcut. A way to make better small code with evidence attached.