botbaki

Stream: general

[Kim Morrison]

Joseph Myers said:

There should be lots of ways for AI to accelerate stating things other than building a sloplib. For example, AI could probably help with many of the more mechanical parts of PR review for mathlib (that aren't mechanical enough to turn into linters) and so reduce the amount of time maintainers need to spend on those when doing reviews for mathlib. People have written extremely detailed instructions to AIs on Linux kernel patch review, why shouldn't we have similarly detailed instructions on reviewing mathlib changes and a service that does such reviews on PRs (automatically, or when requested)?

Oh, and we have this too! See https://github.com/kim-em/botbaki. You can actually use it today on mathlib, try @botbaki review on a PR to request a review, and then @botbaki feedback ... (or just emojis) to tell it whether the review was any good. There's a backend process to incorporate the feedback into a revised review prompt.

The prompting currently is very simplistic, but I think it would be a great project to improve it.

[Sébastien Gouëzel]

Kim Morrison said:

Oh, and we have this too! See https://github.com/kim-em/botbaki. You can actually use it today on mathlib, try @botbaki review on a PR to request a review, and then @botbaki feedback ... (or just emojis) to tell it whether the review was any good. There's a backend process to incorporate the feedback into a revised review prompt.

Are you saying it's currently active on Mathlib? I've just tried to trigger it on #34559 out of curiosity, but it doesn't look like anything is happening.

[Joseph Myers]

Now that botbaki has reviewed #34559, I see it's suggesting omega (to be avoided nowadays) and changing a terminal simp (for a subgoal) to simp only (also typically discouraged).

[Kim Morrison]

Sébastien Gouëzel said:

Kim Morrison said:

Oh, and we have this too! See https://github.com/kim-em/botbaki. You can actually use it today on mathlib, try @botbaki review on a PR to request a review, and then @botbaki feedback ... (or just emojis) to tell it whether the review was any good. There's a backend process to incorporate the feedback into a revised review prompt.

Are you saying it's currently active on Mathlib? I've just tried to trigger it on #34559 out of curiosity, but it doesn't look like anything is happening.

I restarted the listener and it has now responded.

[Kim Morrison]

Joseph Myers said:

Now that botbaki has reviewed #34559, I see it's suggesting omega (to be avoided nowadays) and changing a terminal simp (for a subgoal) to simp only (also typically discouraged).

@Joseph Myers, maybe you would like to reply to those comments with @botbaki feedback ..., and I will then see what prompting updates we get.

Or just giving +1 / -1 emoji reactions to its comments should work as well.

[Sébastien Gouëzel]

The result is quite nice: it caught two real mistakes (repeated scope opening, misnamed lemma) and gave two bad suggestions (unhappy with a grind [StrictMonoOn] proof, wanted to turn a terminal simp into a simp only). Will it improve if we train it on a few PRs and give feedback? If so, I think it's definitely worth investigating.