groar

I guess if you tell codex to build a transpiler from a subset of python to brainfuck, then solve in that subset of python, it would work much better. Would that be cheating?

It would have been fun to see how AI generated voice (like https://www.enginn.tech ) could be integrated as well (and have an estimate of how much time it saves)

The author shows that any neural network having piece-wise linear activation functions can be represented as a decision tree

You're right, it seems to be "LaMDA" (see https://arxiv.org/abs/2201.08239 ). The three first authors are part of the Character.ai team.

I guess it's probably something along the lines of "LaMDA: Language Models for Dialog Applications" (see https://arxiv.org/abs/2201.08239 ). Given that the three first authors are part of the team at Character.ai (see https://beta.character.ai/help)

It is actually "Godard", not Goddard.

Although they should not dismiss it at all as it can lead to extremely successful companies. I have Dataiku or UIPath (they did it for years) as good examples. They leveraged their existing customers to test their first product, with success.

Agreed, my initial title is not accurate. It should say "finds errors in 20% of annotations".

That is true up to a certain point (for instance, in my experience, having bounding boxes that are not pixel-perfect acts as a regularizer), but there is also a good chance that you are mislabelling edge cases, situations that happen rarely, and that definitely hurts the performance of the neural network to make a correct prediction on these difficult / uncommon scenarios.

Yes agreed with that ! I can't change the title unfortunately

If I understand correctly they actually did not change the test set.

Using simple techniques, they found out that popular open source datasets like VOC or COCO contain up to 20% annotation errors in. By manually correcting those errors, they got an average error reduction of 5% for state-of-the-art computer vision models.

Sure, in terms of expressivity, you can obtain much better results with a CNN. But very often, it is done at the cost of computational efficiency: SIFT descriptors are "easy" to compute.

This paper titled "Backpropagation in the Simply Typed Lambda-calculus with Linear Negation" describes how to generalize the backpropagation algorithm used for computational graphs (like in PyTorch or TF) to the simply-typed lambda calculus augmented with a notion of linear negation.

By relying on conceptual tools originating from Linear Logic, the authors prove the correctness of the transformation and its time efficiency.

We started using Slite http://slite.com/ 6 months ago with great success. We previously used Atlassian Confluence for our internal knowledge database, and it resulted in very static content and poor adoption. Slite is a much better choice: we use it for "static" company knowledge (like onboarding, processes, etc.), but also for most of our dynamic content (meeting notes, document drafting, sales support documentation, etc.).

Many people (including dev) use it on a daily basis, and most people on a weekly basis.

Definitely recommend.

This is the result of using deepomatic.com fashion detection API on each frame of a streetstyle fashion week video.

Deepomatic just released four specialized image detection APIs: fashion items, furniture and decoration, street scene and weapon.

https://vimeo.com/194022746 to see in action

Basically trying to achieve a certain level of plasticity in deep neural nets by getting inspiration from https://en.wikipedia.org/wiki/Adult_neurogenesis

For those who never heard about Tierra. I bumped into it today, and it reminded me of the times I was fascinated by this experiment and was playing with similar ideas. Old school.

Yeah but it's still misleading as we are talking about approximating continuous functions here, not any function. Those examples are not clearly computable, or even just continuous..

For those who want to dive further in automata theory, transducers and the non-commutative algebraic view of the theory, the following one by J. Sakarovitch is a fantastic book : http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=978...

Clearly, when I think about the hardest thing I ever coded, I have the following story in mind.

Back in 2002 I was writing a floppy disk driver for the little OS we were writing with a friend. It turned out finding anything else than very sparse documentation was really hard, plus for some unknown reason the floppy drive behavior seemed to be of non-deterministic nature. Maybe the fact that I was 15 didn't help.

At some point, after many nights spent on debugging it, it just worked. I still don't know why. I never changed any line of the code after that moment, by fear of breaking it.

I attended the 2011 edition, and this was one of the best experiences I had during my PhD. Lots of brilliant people, amazing lectures, blue grass music, a rafting session, great beers and so much more. You have to go.

There are many reasons for the name: apart from being one of France's emblems, one of the people who initiated the project is Thierry Coquand and the original type system underlying it is called Calculus Of Construction (CoC).

But I know for a fact that they thought it would be good joke as well.

  Or at least a very [...] formal one

That's a good one ;)

  The problem with memory models is not some much verifying it in a mechanised way, but inventing something suitable at all.

Agreed.

I'm aware of some work done a few years ago by people working on weak memory models and extending CompCert with some concurrency primitives: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/

    What you probably mean is something like nice abstract accounts of memory models for C that at the same time capture all the optimisations modern C-compilers want to do, while still being implementable on existing CPUs. That is indeed an open problem [1].

True. Although CompCert [1] is a nice effort toward that goal: a proved C compiler that covers almost all C99 with many optimizations implemented and proved sound.

[1] http://compcert.inria.fr/compcert-C.html

In a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.