LLM能编程么？OpenAI的最新研究

[hci]

OpenAI自己的文章："are still unable to solve the majority" of coding tasks.

https://arxiv.org/pdf/2502.12115

[forecasting]

OpenAI自己的文章："are still unable to solve the majority" of coding tasks.

https://arxiv.org/pdf/2502.12115

这帮做deepLearning的人理论修养真差，这还需要写论文吗？几年前我老就告诉那些瞎吹的，不可能，几个月前就在这newmitbbs说过，仔细看

别人炒股不喜欢做FA（financial analysis或者fundemental analysis），我一个建议是，把报表等等喂给chatGPT让它先分析，看看效果如何，学会如何利用chatGPT做辅助。

在STEM版提问或回答问题之前也让chatGPT做一下评价，很有益处，至少很有趣！

chatGPT做不了数学证明或者编程，但搜集知识并加以提炼并比较还是有一些意思。这段话在计算机上对应着什么，什么是提炼？压缩，但不是无损压缩。比较，就是匹配并判断异同。判断不同而确定不同之处谁对谁错，就是不错的能力了，我自己想，它是以大多数材料相同的地方来否定个别相异的看法。事实上，它判断不了话语是否一致，至少是所有话语是否一致。

viewtopic.php?p=4319562&hilit=%E8%AF%81 ... B#p4319562

[Caravel]

OpenAI自己的文章："are still unable to solve the majority" of coding tasks.

https://arxiv.org/pdf/2502.12115

LLM写一些短的的code没什么问题，长context的任务还比较困难。但是原理上，我不觉得有什么不肯能的

[wass]

就是一个放大镜，2x或者3x

x就是你的能力

[Caravel]

这帮做deepLearning的人理论修养真差，这还需要写论文吗？几年前我老就告诉那些瞎吹的，不可能，几个月前就在这newmitbbs说过，仔细看


viewtopic.php?p=4319562&hilit=%E8%AF%81 ... B#p4319562

做数学证明没有问题，已经有无数的例子。

[forecasting]

做数学证明没有问题，已经有无数的例子。

'



你能独立做完做对作业，有个家伙拿去抄了一遍，你老师能糊涂到说他也会做作业吗？转引我过去说的关于程序和证明的话：

有几个定理是关于机器学习的，就是机器能学到什么，什么不可能学到。最初有用形式语言理论表述的，
https://en.wikipedia.org/wiki/E._Mark_Gold
https://en.wikipedia.org/wiki/Language_ ... _the_limit
后来有所谓VC维数， https://en.wikipedia.org/wiki/Vapnik%E2 ... _dimension
​
​机器数学证明是另外一个问题，就是靠人的智能编程实现的机器证明。先说个有关而不不是数学定理机器证明的有Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry%E2% ... espondence
再说数学定理机器证明的几个结果：数理逻辑里的量词消去法和与之相关的Tarski–Seidenberg theorem（https://en.wikipedia.org/wiki/Tarski%E2 ... rg_theorem），还有源自代数几何的希尔伯特零点定理的Buchberger算法（https://en.wikipedia.org/wiki/Buchberger%27s_algorithm）。这些有很多已经超出了机器可学习的上限。但是是机器能证明的。把这些嵌入AI里面，能扩展DNN机器证明的能力，可这些不是机器学到的。嵌入DNN，比如设计接口以解决DNN和形式化的机器证明的交互问题，即自然语言和所嵌入机器正证明所用形式化语言（数理逻辑表达式或程序语言）的互译问题。
​
数学定理的机器证明和机器可学得（learnability）本不是一回事。机器可学得（learnability）的数学定理的证明最好的结果是机器可学得（learnability）的语言的子集（证明等价于语法分析）。所以证明如果超出了机器可学得（learnability），即不可能学得，那么就只能嵌入，即从外界引入，或者搜索匹配。

​与机器证明，直觉逻辑/构造逻辑，Curry-Howard对应有关的或者进一步的发展的一个纲领是univalent foundations https://www.ias.edu/ideas/2014/voevodsky-origins
https://www.ias.edu/math/sp/univalent/goals
https://www.ias.edu/idea-tags/univalent-foundations
Fields奖得主Vladimir Voevodsky 开创或者倡议的。
与univalent fiundation相关的计算项目：https://ncatlab.org/nlab/show/univalent ... athematics

算术就是数论的意思，高斯那本书好像就叫作算术研究。几何其实指代数几何，就是代数几何思想和技术应用于数论。算术几何就是研究Diophantine equations的整数解，因为马季亚谢维奇定理（由他提供的完成证明的关键步骤）和MRDP定理（即尤里·马季亚谢维奇（Yuri Matiyasevich），朱莉娅·罗宾逊（Julia Robinson），马丁·戴维斯（Martin Davis）和希拉里·普特南（Hilary Putnam））否定了希尔伯特第十问题。分类丢番图方程并研究其整数解，就自然成了代数几何和数论交叉的地带。

证明就是计算，计算就是证明。我说了好几次Curry-Howard定理，https://en.wikipedia.org/wiki/Curry%E2% ... espondence 。大家可能都觉得是闲聊，就随意浏览一下。

Post，Godel，Herbrand，Turing，Church，Curry and Howard，Chomsky，Markov等人的工作有一个等价关系的证明：Post system = Computable function=Turing Machine=algorithm（program）=proof= c.e.language= Markov algorithm. 等号是表示在计算的意义上等价。普林斯顿高等研究院那个univalent项目部分地也是基于这个思想 https://www.math.princeton.edu/events/u ... -28t163003 。

转：《算术研究》（Disquisitiones Arithmeticae）是德国数学家卡尔·弗里德里希·高斯于1798年写成的一本数论教材，在1801年他24岁时首次出版

四元玉鉴。Knuth也在TAO里说过。往大处说，就是Buchburger's algorithm或者Hilbert Nullstellenstullsatz的思想，这样就联系上代数几何了。所以代数几何尤其算术几何里很多问题或其证明是现成的算法，Curry-Howard定理早就提示了证明（严格说，形式化的证明就是一个程序，这就是princeton高研院那个项目的主要思想之一）和算法等价，https://en.wikipedia.org/wiki/Curry%E2% ... espondence。
另外一个思路就是，Diophantine equation 无算法解（希尔伯特第十问题），研究其解，即算术代数几何，就是在 Matiyasevich's theorem or the MRDP theorem 定理之下用代数几何方法研究方程的解集。https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem。
那几个无知的家伙在撒泼打滚，不仅没学问，也没人品，我不屑于跟他们啰嗦。谁有兴趣，可以教给他们一些基本知识，他们学的不是computer science and technology，是信息工程，没基本的知识，丢死人了。谁敢亮出是哪个老师的学生，小心自己老师知道了真实水平开了他，那可就给华人丢脸了。 我啥时候也民族主义了？

Von Neumann和Godel很早就把证明和程序（算法）等价：https://rjlipton.com/the-gdel-letter/

[wdong]

OpenAI自己的文章："are still unable to solve the majority" of coding tasks.

https://arxiv.org/pdf/2502.12115

我终于意识到交流障碍在哪里了。当我兴奋地说AI能编程的时候，我脑子里想的是: AI有可能能编程，别人还差一点没实现，这个方向可以做。

完全不可能，和已经实现了都没什么意思。差一点的时候最有意思。

[Caravel]

'



你能独立做完做对作业，有个家伙拿去抄了一遍，你老师能糊涂到说他也会做作业吗？转引我过去说的关于程序和证明的话：

你没有意识到人类做数学证明题8，9成都是照猫画虎

自己独创的也就一点点

今天的ai做证明题已经不是简单的抄答案

至少是简单的变化，混合运用也可以handle

我认为和人做证明没有本质的区别

alpha geometry这种混合系统也是一种办法

3，5年内，估计AI就可以证明出来人类证明不了的问题

[Caravel]

我终于意识到交流障碍在哪里了。当我兴奋地说AI能编程的时候，我脑子里想的是: AI有可能能编程，别人还差一点没实现，这个方向可以做。

完全不可能，和已经实现了都没什么意思。差一点的时候最有意思。

是的，还缺什么，也许deepseek把长context搞定，这问题就迎刃而解了，也需要还需要其他big idea

[Spike123]

LLM是一种工具，提高马工的工作效率。以前马工上stack overflow找答案，现在问AI/LLM。
AI抄来的作业可能有问题，未必完全合适，需要调试修改。

[forecasting]

LLM是一种工具，提高马工的工作效率。以前马工上stack overflow找答案，现在问AI/LLM。
AI抄来的作业可能有问题，未必完全合适，需要调试修改。

这才是正解。可以考虑一下如何更好地用它们做辅助，节省人力。

[forecasting]

你没有意识到人类做数学证明题8，9成都是照猫画虎

自己独创的也就一点点

今天的ai做证明题已经不是简单的抄答案

至少是简单的变化，混合运用也可以handle

我认为和人做证明没有本质的区别

alpha geometry这种混合系统也是一种办法

3，5年内，估计AI就可以证明出来人类证明不了的问题

觉得你说的强关联系统（量子）有点意思，如果有机会可以多注意一下。至于指望LLM或者AI做出啥人类做不出或者难做出的证明来，我们就当作美好的理想或者科幻乐一下就好。