Autonomous Agents

Stream: Formal conjectures

[Franz Huschenbeth]

Now we have autonomous agents, posting to the repo. Great...

image.png
this is in FC#2246

I wonder how sloppy their PRs might be, also I wonder what the Prompts were; "Search for Github Repos, where you can open PRs", "Search in the Github Repo of Formal Conjectures and see if you can help with formalizing a Problem"

Maybe their PRs are even better compared to people using AI blindly, because the autonomous agent can decide how much information / iterations it wants to use. But even if that is the case, it would be kind of uncanny to merge such PR.

[Franz Huschenbeth]

I dont think they are at such level yet, but they will likely get to such level. It always requires scaffolding in the beginning and then they get progressively more autonomous over time and need less and less scaffolding.

[Yaël Dillies]

The future is old now

[Michael Rothgang]

I'm not sure if a comment like "this can be resolved by addressing the core issue" carries much value. But your mileage may vary!

[Franz Huschenbeth]

I think that is boilarplate of the software scaffold around this kind of agent.

Its probably some software, which people can install and then auto manages the Github Account by setting up Hooks, which are triggered when a new issue is opened. It ingests the issue content and then makes a suggested solution. The Thing is that this pipeline seems to be bugged, it commented in less than a second on the issue, far less than it would need for the inference and we can also deduce this because the "proposed Solution" is actually empty.

So in a nutshell, we now have AI Slop Software used to distribute / annoy people with more AI Slop.

[Franz Huschenbeth]

If something like that becomes too big of a problem, one could think about introducing something along these lines:

Vouch

By Mitchell Hashimoto.

[Felix Pernegger]

Franz Huschenbeth said:

Now we have autonomous agents, posting to the repo. Great...

image.png
this is in FC#2246

I wonder how sloppy their PRs might be, also I wonder what the Prompts were; "Search for Github Repos, where you can open PRs", "Search in the Github Repo of Formal Conjectures and see if you can help with formalizing a Problem"

Maybe their PRs are even better compared to people using AI blindly, because the autonomous agent can decide how much information / iterations it wants to use. But even if that is the case, it would be kind of uncanny to merge such PR.

Nevertheless if such an agent is applied to the formalconjectures repo this is/will likely be a Github-wide issue, in which case it seems better to let them figure out anti bot measures rather than to (try to) apply something ourselves

[Franz Huschenbeth]

I agree.

It was just a possible option, of how a solution might look like. It certainly is not a impossible problem to solve :)