Viewing profile — karelpeeters

In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.

Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL and verified parts of it? I have no doubt that mode…

Degate is even a bit overkill, it is meant for when you only have images of the physical chip. This challenge has the full GDS files, which are the files that are sent to the fab f…

Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway! I'm…

Congrats on solving the challenge! I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations…

Text watermarking has no effect on output quality, it just works by changing the explicit source of randomness that is in practice always present in LLM output sampling. See for ex…

No, I think the comment you're responding to is actually correct. Look at this quote from the Anthropic blog post again: > The design should have been simple: if a session has been…

What would be the point of embedding Redis into an application? What's the advantage of using Redis over using the builtin (or third party) data structures of the language the appl…

Using this sampling-based approach you get correct covariance modeling for free. You have to only sample leaf values that are used in multiple places once per evaluation, but it lo…

Yes, the `regex` crate is also the regex engine used by ripgrep, both were developed by https://github.com/burntsushi .

Out of curiosity, why are you still using 32-bit architectures?

That switch-case gets optimized and compiled down to logic gates by the synthesis tools. It'll be a different set of gates from the original netlist (which might also have used a m…

Matlab is one language that chooses the second. Every assignment a=b where b is a matrix creates a distinct copy of the matrix. The interpreter is slightly more clever and instead …

Look like this was generated by an LLM.

It means that instead of (only) doing convolution in spatial dimensions, it also(/instead) happens in the temporal dimension. A good resource for the "instead" case: https://unit8.…

Could you share the paper(s) about "backdoors" in physical constants? That doesn't make much sense at first sight.

Sure, it's all slightly fuzzy. I don't think that detracts much from the my point though.

For all emails sent to/from any Seattle owned email address in 2017, please provide the following information: 1. From address 2. To address 3. bcc addresses 4. cc addresses 5. Tim…

Interesting, what could power companies use this for? Checking for overgrown power lines? Checking for roofs to place solar panels one?

Could you share the repo? I've been curious what nontrivial parsers look like woth nom, I always lose the overview pretty quickly.

It's important to note that these probe models are very simple - they're "trained" by just doing a linear regression between the hidden activations and the desired output. This mea…

What value does this label have for English localization?

That sounds interesting, can you give some examples? Is this limited to classical RL Q-learning type stuff for turn based games, or full AlphaStar-level agents for RTS games?

I'm not an expert, but some thoughts: * The problem with large vectors is that they have large dot products with every other vector, which would imply that they are more similar to…