llwu

5 ms·

1.
by llwu 2y ago
Yeah, the progress has to be quite significant, no points are awarded for trivial observations. Thus scores are usually bimodal around 0 and 7. In the linked stats you can see that 1 point for P3/P5 was less common than full score on o
2.
by llwu 2y ago
Partial credit is quite challenging to earn, per: https://www.imo-official.org/year_statistics.aspx?year=2024
3.
by llwu 2y ago
nlinarith is a proof automation that attempts to finish a proof using the simplex method to find a linear combination of hypotheses and things that have already been proven, as well as some quadratic terms of them. Docs: https://
4.
by llwu 2y ago
> We don't have a way to verify formalizations the same way. While there is no perfect method, it is possible to use the agent to determine if the statement is false, has contradictory hypotheses, or a suspiciously short proof.
5.
by llwu 3y ago
I contributed a few trivial proofs to this project, and I tried enlisting GPT-4, Copilot, Moogle, and Morph Prover to help out (I did not try LLMStep or ReProver). Out of these: - GPT-4 answered maybe one or two questions about syntax - Cop
6.
by llwu 3y ago
Even if eprint.iacr.org did include the analogue of viXra's content (which I've heard it mostly doesn't, other than one time that famous cryptographer whose name I forgot got old and published a crank paper, which IIRC was qu
7.
by llwu 3y ago
Adding to what other commenters said, ESLint also works like this. However in an IDE setting it's not exactly "auto"; you have to click the light bulb and accept the fix (idk about VSCode, but in Neovim you can even get a pre
8.
by llwu 3y ago
Question on the "Batching memory-bound processes on a GPU" section - it says "This enables us to reuse parts of the model that we’ve already loaded into the GPU’s SRAM", but the 10 GB we are loading is into the HBM, righ
9.
by llwu 3y ago
There is a niche use-case for the reverse order `(foo min map filter baz bar)`, which is, solving typed holes (you could refine the hole as like `_.foo()` although that wouldn't be interoperable with things like next token prediction).
10.
by llwu 3y ago
This is a cool idea - it could be tested it by seeing whether W_V tends to map <bot> to 0, and whether <bot> tends to get attended to. There are interesting things to said whether or not this turns out to be the case.
11.
by llwu 3y ago
This is probably what the author meant to say but elided. I can see why it looks off though.
12.
by llwu 3y ago
Aren't CRDTs the logical conclusion of automatic merging? I feel like with source control you want to be more intentional about what gets merged, right? Maybe CRDT can be good for trunk-based development with a merge queue. Definitely
13.
Is server component default always a performance win? Or should it be opt-in?(github.com)
1 points by llwu 3y ago|0 comments