TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

Show HN: SupGen, an model-free program synthesizer by examples / dependent types

21 点作者 LightMachine4 个月前

7 条评论

tough4 个月前
The speaker is presenting a new AI tool that can synthesize proofs of mathematical theorems. The tool uses a combination of numerators and primitives to prove theorems exponentially fast, even on a single core. The speaker notes that the tool has limitations, such as only recursing on row numbers and not being able to learn or predict the next token in a symbolic transform. However, they believe that the tool will be useful for programming and solving big problems, such as the Riemann Hypothesis or making a whole game from scratch. The speaker plans to release a playground soon, allowing users to experiment with the tool and have fun using it.<p>Some key points from the presentation include:<p>* The tool can prove mathematical theorems exponentially fast, even on a single core. * It uses a combination of numerators and primitives to prove theorems. * It has limitations, such as only recursing on row numbers and not being able to learn or predict the next token in a symbolic transform. * The tool will be useful for programming and solving big problems. * A playground will be released soon, allowing users to experiment with the tool and have fun using it.<p>Overall, the speaker is excited about the potential of the tool and believes it could be a valuable addition to the field of AI research and development.
评论 #42775591 未加载
calebh4 个月前
The video was originally posted on X, and can still be viewed here: <a href="https:&#x2F;&#x2F;x.com&#x2F;VictorTaelin&#x2F;status&#x2F;1881392823246729640" rel="nofollow">https:&#x2F;&#x2F;x.com&#x2F;VictorTaelin&#x2F;status&#x2F;1881392823246729640</a><p>It&#x27;s about the use of interaction nets, which gives an optimal evaluation strategy for the lambda calculus. I&#x27;m not an expert on it, but from my understanding it allows extensive sharing of computation across different instances of an enumerative search.<p>Parallelism of the computation is another big selling point, except modern hardware design is not well suited for the calculus. The author of the video recently tried to get the system to work well on GPUs and ran into issues with thread divergence. I think their current plan is to build some sort of cluster of Mac Minis due the good performance of the CPUs on that platform.<p>If this computation paradigm advances far enough and shows enough promise, I would expect to see companies start to prototype processors tailor made for interaction nets.
评论 #42799601 未加载
tluyben24 个月前
I think this was the video?<p><a href="https:&#x2F;&#x2F;youtu.be&#x2F;GddkKIhDE2c" rel="nofollow">https:&#x2F;&#x2F;youtu.be&#x2F;GddkKIhDE2c</a>
tecore4 个月前
That’s really awesome
gingfreecss4 个月前
Freaking incredible
greatgib4 个月前
Youtube tells me that the video is not available :(<p>Would someone be able to do a tldr of what this is about? Looks interesting but the title doesn&#x27;t give me a clue about what it is... Llm, audio,...?
10mateus3114 个月前
this is so dope omg