超超 LV
发表于 2025-4-8 12:09:39
感谢大佬的关注 @Eternity, 作为一个研一的科研新手实在是受宠若惊! 其实之前有点懒了不想更了，现在也回国继续读研二了在隔离，暂时忙完一堆事后终于可以来说说感受吧。随便传播一下neural theorem proving这个比较小众的方向~
先讲讲实习内容。进的组是一个很小的组，用语言模型(Language Model)来做形式化的数学证明。具体来说，就是让AI自己学会怎么做数学证明题。在给定数学题目下，给出这个题目的证明。这个证明是形式化的也就是可以被验证，主要是在一些形式化系统中(Lean, Metamath, Isabelle...)。
组内的氛围很轻松，大家大部分都远程所以一般就用Slack来交流了。但是节奏感觉很快，而且大家都很有激情(推动AI在数学上的能力，比如能让它做IMO数学题)。我猜可能因为这个主题就很理想主义，不像什么GPT-3，Copilot可以拿来赚钱。因为这个组的主题是数学的缘故，需要和Metamath和Lean的社区里的数学家有很多交流，(比如我就在Lean的Zulip chat里经常看到大佬 @mcwu 出没，以及没事就看看Kevine Buzzard或者Peter Scholze的发言记录)。
让我印象深刻的一点是，Slack里有一个频道叫research。像我这种实习生没什么权限看其他频道的内容，所以当时我只是听说了过几个月要发布Copilot但是对研究细节完全不知情。但是research这个频道是几乎所有人都能看到的。每天都会有不同人的分享ArXiv文章，或者其他机构的推特。然后就可以近距离观看头牌大佬例如Ilya Sutskever的对不同的文章的评论和发言。往往他们的一两句话就能说到重点，特别是一些经验性的claim，对研究直觉和品味的形成是很宝贵的财富。(可惜我实习的时候没好好看，现在也看不到了，难过)。
能进组的原因大概也是我的技能树比较特殊？前一段实习是做Rust开发。刚开始实习的时候，组里说要把所有Python的内核用Rust重写一遍(因为Rust快啊，内存效率高，Rust牛逼)。他们一看我简历说原来你写过Rust啊，拉我过去帮忙。结果靠另一位大佬花了一星期就都大部分搞定了。我只能负责边边角角的部分。这也导致了这几个月写的代码都是Rust：一开始写原型用Python，然后再用Rust重写一遍。至于其他语言，最后共花了一周学习Lean，Metamath就开始上手干活了。
之前在X读书的时候，在Inria(就是那个写了sklearn包的机构)也做过一段时间的实习，搞知识图谱。一周见一次导师，十分佛系(可能也因为他们对我没什么期待)，最后说欸有可能发一篇paper结果到现在不了了之。在这里有问题随时发个消息过去问导师一般答复都很快。也算是一种对比吧。
最后给我的工作打一下小广告：openai/miniF2F. 嘿嘿
------------------------------------------------------------
过几天去OpenAI毕业实习了，先mark一下过几个月再答(逃 |
|
