3 ms·

A seemingly obvious approach would be to try to get GPT-X to generate candidate proofs and then get a tool like Lean to validate them. Which presumably doesn't

by janekm 6y ago

A seemingly obvious approach would be to try to get GPT-X to generate candidate proofs and then get a tool like Lean to validate them. Which presumably doesn't work or else I suppose the article would have been about that...

iandanforth 6y ago
For reference here's a GPT-3 output for the sample question: Solution: Suppose the given set of n points is A = (a 1 , a 2 , …, a n ). Between any two points we will draw a line segment connecting them, and let the distance from a 1 to the line segment be d(a 1 ,a 2 ) and d(a 1 ,a 3 ) be the distance from a 1 to the line segment connecting a 2 and a 3. Since any two of the points determine a line segment connecting them, there are n–2 segments connecting the n–1 points. Let L be the common perpendicular bisector of two of these segments. So, d(a 1 ,a 2 ) = d(a 1 , L) and d(a 1 ,a 3 ) = d(a 1 , L). Now, we consider the triangle formed by the points (a 1 , a 2 ) and (a 1 , a 3 ). If we are given the points a 1 , a 2 and a 3 , we can easily find the sides of the triangle. Since d(a 1 ,a 2 ) + d(a 1 ,a 3 ) = d(a 1 , L) + d(a 1 , L) = 2d(a 1 , L), the triangle formed is right angled and therefore non-degenerate. We can easily calculate the rational area of such a triangle and the side lengths. Let us consider the simplest case when n = 3. We have three points (a 1 , a 2 , a 3 ) such that each of a 1 , a 2 and a 3 are different. Therefore, we can form a triangle by connecting a 1 , a 2
- pmiller2 6y ago
  This is great. It looks like the confused ramblings of a student who has no clue.
  - singhrac 6y ago
    Always fun to grade these kinds of proofs with a bottle of wine at 2am. I never faulted anyone for doing this, but I sometimes wondered why they bothered. Throwing stuff to a wall to see what sticks doesn't give you points.
    - Jtsummers 6y ago
      One of my math professors had a "BS" stamp for things like this. If it were worth X points, you'd lose X-5 when it was so obviously a rambling mess. He'd rather you just say "I don't know" than waste both your time and his. Perhaps that's just an advantage of tenure, though.
gwern 6y ago
OA has done that, as 'GPT-f': https://arxiv.org/abs/2009.03393#openai https://arxiv.org/abs/2009.03393#openai They also have ambitions of IMO: https://twitter.com/spolu/status/1303693595833237504 https://twitter.com/spolu/status/1303693595833237504 I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this Lean-using team.

by janekm 6y ago

iandanforth 6y ago

For reference here's a GPT-3 output for the sample question: Solution: Suppose the given set of n points is A = (a 1 , a 2 , …, a n ). Between any two points we will draw a line segment connecting them, and let the distance from a 1 to the line segment be d(a 1 ,a 2 ) and d(a 1 ,a 3 ) be the distance from a 1 to the line segment connecting a 2 and a 3. Since any two of the points determine a line segment connecting them, there are n–2 segments connecting the n–1 points. Let L be the common perpendicular bisector of two of these segments. So, d(a 1 ,a 2 ) = d(a 1 , L) and d(a 1 ,a 3 ) = d(a 1 , L). Now, we consider the triangle formed by the points (a 1 , a 2 ) and (a 1 , a 3 ). If we are given the points a 1 , a 2 and a 3 , we can easily find the sides of the triangle. Since d(a 1 ,a 2 ) + d(a 1 ,a 3 ) = d(a 1 , L) + d(a 1 , L) = 2d(a 1 , L), the triangle formed is right angled and therefore non-degenerate. We can easily calculate the rational area of such a triangle and the side lengths. Let us consider the simplest case when n = 3. We have three points (a 1 , a 2 , a 3 ) such that each of a 1 , a 2 and a 3 are different. Therefore, we can form a triangle by connecting a 1 , a 2

pmiller2 6y ago
This is great. It looks like the confused ramblings of a student who has no clue.
- singhrac 6y ago
  Always fun to grade these kinds of proofs with a bottle of wine at 2am. I never faulted anyone for doing this, but I sometimes wondered why they bothered. Throwing stuff to a wall to see what sticks doesn't give you points.
  - Jtsummers 6y ago
    One of my math professors had a "BS" stamp for things like this. If it were worth X points, you'd lose X-5 when it was so obviously a rambling mess. He'd rather you just say "I don't know" than waste both your time and his. Perhaps that's just an advantage of tenure, though.

gwern 6y ago

OA has done that, as 'GPT-f': https://arxiv.org/abs/2009.03393#openai https://arxiv.org/abs/2009.03393#openai They also have ambitions of IMO: https://twitter.com/spolu/status/1303693595833237504 https://twitter.com/spolu/status/1303693595833237504 I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this Lean-using team.