txhwind

4 ms·

1.
by txhwind 8d ago
I'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?
2.
by txhwind 9d ago
It looks like a Transformer encoder post-trained on classification and regression tasks. The encoder-only model is less noticed in recent years, but this product finds a nice application for it.
3.
by txhwind 10d ago
In imperative languages, it's a leaky abstraction not reducing the cognition overhead, compared with the plain loop.
4.
by txhwind 10d ago
If the contraint is not in the signature, and cannot trigger a test failure with typical implementation, it doesn't exist.
5.
by txhwind 11d ago
other questions: - can it be used to relax timing order requirement in pipeline parallelism? Each node update lambda on communication, and optimize weights at other time. - given that BP is using SGD, can batches and T share the same timeli
6.
by txhwind 11d ago
Backprop can also be viewed L local signal passing, but it requires global timing coordination. The Lagrangian enables out-of-order update.
7.
by txhwind 11d ago
Nice introduction to a simple but useful idea! The Lagrangian works like a time-smoothed optimizing direction state, but it can be placed on any wire, even at non-differentiable boundary! Can it be better than existing training methods for
8.
by txhwind 13d ago
Human hackers would be put into jail. LLM hackers would be rewarded.
9.
by txhwind 26d ago
Funded positions are much less than PhD number. However, people can fund themselves with a job. In a country, if it's easy to to get a part-time job with enough payment, mathematicians can continue work.
10.
by txhwind 1mo ago
With agent asssistance, we don't need writing annoying formal spec and proof anymore. Then formal verification can be a practical and useful tool in daily programming, especially for "deep module" whose spec is much simpler t
11.
by txhwind 2mo ago
I also wrote a Monkey script to save clicks when reading papers: just embed PDF webview into the Arxiv abstract page. https://github.com/OneMoreSecond/FileSave/blob/master/arxiv_... It seems the software
12.
by txhwind 4mo ago
This is the first shoelace knot my parents taught me. We call it "butterfly knot". It's always my default choice with muscle memory, unless the shoelace is not long enough to create the "bufferfly wings". It's
13.
by txhwind 4mo ago
Does the official relay server cost a lot on network?
14.
by txhwind 4mo ago
Very nice! an open-sourced alternative of Codex Remote Control, allowing full customization
15.
by txhwind 4mo ago
I prefer synthetic dataset since the first day hearing distillation. The engineering friction is much lower than soft logits, and I have not observed or heard performance loss (in Speech and language area).
16.
by txhwind 4mo ago
Could you share some latest articles or papers comparing both methods, especially on lanuage modelling case? I was not conviced by this claim when reading the original Knowledge Distillation paper. ChatGPT said there are some later works sh
17.
by txhwind 4mo ago
How is the water animation implemented?
18.
by txhwind 4mo ago
I'm curious on the use of rsync in version control. What's the source and destination?
19.
by txhwind 4mo ago
now we may have a more powerful "Prolog" - LLM Agent, though not precise and correct somtimes.
20.
by txhwind 4mo ago
I really hate modern time schedule. It's nightmare to be forced to get up 6am or 7am every workday since childhood. The only relief is natural wakeup on weekend.
21.
by txhwind 4mo ago
another "obscurity": I'm not valuable enough to be attacked, compared with the cost. But what if cost has been reduced a lot?
22.
by txhwind 4mo ago
Fucking abbreviations. Who knows it's DeepSeek, Dark Souls or DualShock? All possible on HN.
23.
by txhwind 6mo ago
The proof will be more friendly to nowadays programmers if we treat all "Gödel numbers" as bytecode of a programming language. It's trivial that functions like "prove" and "subst" can be implemented based