spolu

Yes you are perfectly right. Our product pushes users to be selective on the tables they give access to a given agent for a given use-case :+1:

The tricky part is correctly supporting multiple systems which each have their own specificity. All the way to Salesforce which is an entirely different beast in terms of query language. We're working on it right now and will likely follow-up with a blog post there :+1:

Hi, you are right that things can go sideways fast. In practice, the data that the typical employee needs is also quite simple. So there is definitely a very nice fit for this kind of product with a large number of use-case that we do see provide a lot of value internally for employees (self access to data) and data scientist (reducing loads).

For complex queries/use-cases, we generally instead push our users to create agents that assist them in shaping SQL directly, instead of going directly from text to result/graphs. Pushes them to think more about correctness while still saving them tone of time (the agent has access to the table schemas etc...), but not a good fit for non technical people of course.

Hi, this is a fair concern. We're super early and working on a proper privacy policy as we speak. But we also provided some color about how we handle your data on our Discord. Copying it here:

``` The privacy section on the landing README remains true. We just send your requests to OpenAI and store them for debugging purposes but we don't fetch or store anything else than what is required to process your requests of course. XP1 being opensource you can also look at the code if needed, but happy to answer any question In short: - Requests (including the text dump of tabs you select) go to the Dust main platform - They are processed as part of a Dust app whose Run object is stored - The LLM query is sent to OpenAI (retention policy 30 days, not used for training) - The response is tored as part of Dust's Run object - The response is streamed back to the client ```

Completely agreed with that. We'll revisit if needed but we don't expect it to be too much of an issue at this stage.

Our goal is to gather marginally more usage to learn more about productivity use-cases using LLMs.

Here's the email we sent to our users as we removed the paywall: https://twitter.com/dust4ai/status/1633484243228585988

Dust XP1 runs on a Dust app. You just need a "history" input parameter that gets injected at the right place. Does that make sense?

The real value will accrue as the assistant become more personalised as users use it.

Completely agreed! I believe I’ll open source the app in the coming days.

This is before anything else an exploration at this stage.

Some additional context here if interested: https://twitter.com/spolu/status/1602692992191676416

Copilot actually knows a bit of Lean and can be helpful when formalizing stuff. But it does not get the critical feedback we get from the formal systems (as it's not designed for formal systems).

It would be interesting to eval copilot on the same benchmark as I'm pretty sure it can close some of the proofs still.

It takes a lot of CPU (lean side) on top of GPU (neural side) indeed. But technically, when properly parallelized, it takes no more than 1-2h to crack the hardest problem we've cracked so far.

This is definitely something that we'll be looking into more closely in the future. Our old and busted `gptf` tactic was a good start but we can do much better!

Sorry, late reply. Indeed settle.network expired and is now owned by another party. Sorry for the ensued confusion.

Completely agreed.

(30k proofs to be precise, valid and test are each 1k)