4 ms·

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

21 points by LightMachine 2y ago

gingfreecss 2y ago
Freaking incredible
10mateus311 2y ago
this is so dope omg
greatgib 2y ago
Youtube tells me that the video is not available :( Would someone be able to do a tldr of what this is about? Looks interesting but the title doesn't give me a clue about what it is... Llm, audio,...?
calebh 2y ago
The video was originally posted on X, and can still be viewed here: https://x.com/VictorTaelin/status/1881392823246729640 https://x.com/VictorTaelin/status/1881392823246729640 It's about the use of interaction nets, which gives an optimal evaluation strategy for the lambda calculus. I'm not an expert on it, but from my understanding it allows extensive sharing of computation across different instances of an enumerative search. 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. 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.
- worldsayshi 2y ago
  Here's a bsky link: https://bsky.app/profile/victortaelin.bsky.social/post/3lg72urscyk2a https://bsky.app/profile/victortaelin.bsky.social/post/3lg72...
tluyben2 2y ago
I think this was the video? https://youtu.be/GddkKIhDE2c https://youtu.be/GddkKIhDE2c
tecore 2y ago
That’s really awesome
flvsff 2y ago
[flagged]
flvsff 2y ago
[flagged]
tough 2y ago
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. Some key points from the presentation include: * 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. 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.
- tough 2y ago
  Table of Contents 01:53 Proving the Ruma Hypothesis - https://youtu.be/GddkKIhDE2c?t=113 https://youtu.be/GddkKIhDE2c?t=113 05:13 Restricting Word Types to Exactly Two Bits Set - https://youtu.be/GddkKIhDE2c?t=313 05:18 First-Class Enumerations for Computation - https://youtu.be/GddkKIhDE2c?t=318 06:35 Enumerations Interoperability - https://youtu.be/GddkKIhDE2c?t=395 06:44 Narrowed List of Functions with Restrictions - https://youtu.be/GddkKIhDE2c?t=404 07:50 New Definition Emerges - https://youtu.be/GddkKIhDE2c?t=470 08:18 Section Title: Wrong Function Example - https://youtu.be/GddkKIhDE2c?t=498 08:24 Most Overfit Functions, But First One Stands Out - https://youtu.be/GddkKIhDE2c?t=504 09:40 General Addition Implementation Tested - https://youtu.be/GddkKIhDE2c?t=580 09:49 Finding Unique Functions - https://youtu.be/GddkKIhDE2c?t=589 10:36 Examining Functions with a Simple Loop - https://youtu.be/GddkKIhDE2c?t=636 10:38 First Argument Relationship - https://youtu.be/GddkKIhDE2c?t=638 10:48 PubShadow Literature Finds Problem in 0.06 Sec - https://youtu.be/GddkKIhDE2c?t=648 11:37 Complexity Hides in Simple Tasks - https://youtu.be/GddkKIhDE2c?t=697 12:11 Fast Loading Due to Under-the-Hood Optimizations - https://youtu.be/GddkKIhDE2c?t=731 13:33 Function Finder in 4.5 Sec - https://youtu.be/GddkKIhDE2c?t=813 13:41 Accelerating the Process - https://youtu.be/GddkKIhDE2c?t=821 14:37 Speedups via Cluster Parallelization - https://youtu.be/GddkKIhDE2c?t=877 14:45 Boolean, Natural Number, Words of Fixed Length, Lists, Funct - https://youtu.be/GddkKIhDE2c?t=885 https://youtu.be/GddkKIhDE2c?t=885 16:23 Proving a Theorem by Defining an Empty Body - https://youtu.be/GddkKIhDE2c?t=983 16:30 Recipient Receives First Bit of List - https://youtu.be/GddkKIhDE2c?t=990 17:06 New Goal: Proving Equation for Pairs - https://youtu.be/GddkKIhDE2c?t=1026 17:40 Section Title: Boolean List Conversion - https://youtu.be/GddkKIhDE2c?t=1060 18:23 Constructing Equates in a Function - https://youtu.be/GddkKIhDE2c?t=1103 19:07 True Case Match: Convert Not True to True - https://youtu.be/GddkKIhDE2c?t=1147 19:21 Proof Complete: No More Obligations - https://youtu.be/GddkKIhDE2c?t=1161 19:31 Proving Self-Computation with Auxiliary Function - https://youtu.be/GddkKIhDE2c?t=1171 19:59 Proving List's Tail - https://youtu.be/GddkKIhDE2c?t=1199 20:39 Inductive Hypothesis Applied to Rest of List - https://youtu.be/GddkKIhDE2c?t=1239 21:29 Proof of Empty Pattern Match - https://youtu.be/GddkKIhDE2c?t=1289 21:32 Section Title: Synthesizer's Turn - https://youtu.be/GddkKIhDE2c?t=1292 22:01 Demonstrating a Key Theorem - https://youtu.be/GddkKIhDE2c?t=1321 https://youtu.be/GddkKIhDE2c?t=1321 23:05 Instant Search Proof - https://youtu.be/GddkKIhDE2c?t=1385 24:01 Enumerating the Proof Space - https://youtu.be/GddkKIhDE2c?t=1441 https://youtu.be/GddkKIhDE2c?t=1441 26:06 Integrating with Theorem Provers - https://youtu.be/GddkKIhDE2c?t=1566 https://youtu.be/GddkKIhDE2c?t=1566 27:20 Closing Notes: Simplistic Tool for Fast Solutions - https://youtu.be/GddkKIhDE2c?t=1640 https://youtu.be/GddkKIhDE2c?t=1640 28:08 Ready to Paralize with Cluster of Matchminis - https://youtu.be/GddkKIhDE2c?t=1688 https://youtu.be/GddkKIhDE2c?t=1688 28:18 Predicting Next Token - https://youtu.be/GddkKIhDE2c?t=1698 29:18 Predicting Next Tokens with Symbolic Transforms - https://youtu.be/GddkKIhDE2c?t=1758 https://youtu.be/GddkKIhDE2c?t=1758 29:33 Synthesizing Token Predictions from Lists - https://youtu.be/GddkKIhDE2c?t=1773

21 points by LightMachine 2y ago

gingfreecss 2y ago

Freaking incredible

10mateus311 2y ago

this is so dope omg

greatgib 2y ago

Youtube tells me that the video is not available :( Would someone be able to do a tldr of what this is about? Looks interesting but the title doesn't give me a clue about what it is... Llm, audio,...?

calebh 2y ago

The video was originally posted on X, and can still be viewed here: https://x.com/VictorTaelin/status/1881392823246729640 https://x.com/VictorTaelin/status/1881392823246729640 It's about the use of interaction nets, which gives an optimal evaluation strategy for the lambda calculus. I'm not an expert on it, but from my understanding it allows extensive sharing of computation across different instances of an enumerative search. 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. 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.

worldsayshi 2y ago
Here's a bsky link: https://bsky.app/profile/victortaelin.bsky.social/post/3lg72urscyk2a https://bsky.app/profile/victortaelin.bsky.social/post/3lg72...

tluyben2 2y ago

I think this was the video? https://youtu.be/GddkKIhDE2c https://youtu.be/GddkKIhDE2c

tecore 2y ago

That’s really awesome

flvsff 2y ago

[flagged]

flvsff 2y ago

[flagged]

tough 2y ago

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. Some key points from the presentation include: * 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. 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.

tough 2y ago
Table of Contents 01:53 Proving the Ruma Hypothesis - https://youtu.be/GddkKIhDE2c?t=113 https://youtu.be/GddkKIhDE2c?t=113 05:13 Restricting Word Types to Exactly Two Bits Set - https://youtu.be/GddkKIhDE2c?t=313 05:18 First-Class Enumerations for Computation - https://youtu.be/GddkKIhDE2c?t=318 06:35 Enumerations Interoperability - https://youtu.be/GddkKIhDE2c?t=395 06:44 Narrowed List of Functions with Restrictions - https://youtu.be/GddkKIhDE2c?t=404 07:50 New Definition Emerges - https://youtu.be/GddkKIhDE2c?t=470 08:18 Section Title: Wrong Function Example - https://youtu.be/GddkKIhDE2c?t=498 08:24 Most Overfit Functions, But First One Stands Out - https://youtu.be/GddkKIhDE2c?t=504 09:40 General Addition Implementation Tested - https://youtu.be/GddkKIhDE2c?t=580 09:49 Finding Unique Functions - https://youtu.be/GddkKIhDE2c?t=589 10:36 Examining Functions with a Simple Loop - https://youtu.be/GddkKIhDE2c?t=636 10:38 First Argument Relationship - https://youtu.be/GddkKIhDE2c?t=638 10:48 PubShadow Literature Finds Problem in 0.06 Sec - https://youtu.be/GddkKIhDE2c?t=648 11:37 Complexity Hides in Simple Tasks - https://youtu.be/GddkKIhDE2c?t=697 12:11 Fast Loading Due to Under-the-Hood Optimizations - https://youtu.be/GddkKIhDE2c?t=731 13:33 Function Finder in 4.5 Sec - https://youtu.be/GddkKIhDE2c?t=813 13:41 Accelerating the Process - https://youtu.be/GddkKIhDE2c?t=821 14:37 Speedups via Cluster Parallelization - https://youtu.be/GddkKIhDE2c?t=877 14:45 Boolean, Natural Number, Words of Fixed Length, Lists, Funct - https://youtu.be/GddkKIhDE2c?t=885 https://youtu.be/GddkKIhDE2c?t=885 16:23 Proving a Theorem by Defining an Empty Body - https://youtu.be/GddkKIhDE2c?t=983 16:30 Recipient Receives First Bit of List - https://youtu.be/GddkKIhDE2c?t=990 17:06 New Goal: Proving Equation for Pairs - https://youtu.be/GddkKIhDE2c?t=1026 17:40 Section Title: Boolean List Conversion - https://youtu.be/GddkKIhDE2c?t=1060 18:23 Constructing Equates in a Function - https://youtu.be/GddkKIhDE2c?t=1103 19:07 True Case Match: Convert Not True to True - https://youtu.be/GddkKIhDE2c?t=1147 19:21 Proof Complete: No More Obligations - https://youtu.be/GddkKIhDE2c?t=1161 19:31 Proving Self-Computation with Auxiliary Function - https://youtu.be/GddkKIhDE2c?t=1171 19:59 Proving List's Tail - https://youtu.be/GddkKIhDE2c?t=1199 20:39 Inductive Hypothesis Applied to Rest of List - https://youtu.be/GddkKIhDE2c?t=1239 21:29 Proof of Empty Pattern Match - https://youtu.be/GddkKIhDE2c?t=1289 21:32 Section Title: Synthesizer's Turn - https://youtu.be/GddkKIhDE2c?t=1292 22:01 Demonstrating a Key Theorem - https://youtu.be/GddkKIhDE2c?t=1321 https://youtu.be/GddkKIhDE2c?t=1321 23:05 Instant Search Proof - https://youtu.be/GddkKIhDE2c?t=1385 24:01 Enumerating the Proof Space - https://youtu.be/GddkKIhDE2c?t=1441 https://youtu.be/GddkKIhDE2c?t=1441 26:06 Integrating with Theorem Provers - https://youtu.be/GddkKIhDE2c?t=1566 https://youtu.be/GddkKIhDE2c?t=1566 27:20 Closing Notes: Simplistic Tool for Fast Solutions - https://youtu.be/GddkKIhDE2c?t=1640 https://youtu.be/GddkKIhDE2c?t=1640 28:08 Ready to Paralize with Cluster of Matchminis - https://youtu.be/GddkKIhDE2c?t=1688 https://youtu.be/GddkKIhDE2c?t=1688 28:18 Predicting Next Token - https://youtu.be/GddkKIhDE2c?t=1698 29:18 Predicting Next Tokens with Symbolic Transforms - https://youtu.be/GddkKIhDE2c?t=1758 https://youtu.be/GddkKIhDE2c?t=1758 29:33 Synthesizing Token Predictions from Lists - https://youtu.be/GddkKIhDE2c?t=1773